]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly2/common/option.ma
arithmetics for λδ
[helm.git] / matita / matita / contribs / ng_assembly2 / common / option.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "common/comp.ma".
24 include "common/option_base.ma".
25 include "num/bool_lemmas.ma".
26
27 (* ****** *)
28 (* OPTION *)
29 (* ****** *)
30
31 nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
32  #T; #x1; #x2; #H;
33  nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
34  nrewrite < H;
35  nnormalize;
36  napply refl_eq.
37 nqed.
38
39 nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
40  #T; #x; #H;
41  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
42  nrewrite > H;
43  nnormalize;
44  napply I.
45 nqed.
46
47 nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
48  #T; #x; #H;
49  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
50  nrewrite < H;
51  nnormalize;
52  napply I.
53 nqed.
54
55 nlemma symmetric_eqoption :
56 ∀T:Type.∀f:T → T → bool.
57  (symmetricT T bool f) →
58  (∀op1,op2:option T.
59   (eq_option T f op1 op2 = eq_option T f op2 op1)).
60  #T; #f; #H;
61  #op1; #op2; nelim op1; nelim op2;
62  nnormalize;
63  ##[ ##1: napply refl_eq
64  ##| ##2,3: #H; napply refl_eq
65  ##| ##4: #a; #a0;
66           nrewrite > (H a0 a);
67           napply refl_eq
68  ##]
69 nqed.
70
71 nlemma eq_to_eqoption :
72 ∀T.∀f:T → T → bool.
73  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
74  (∀op1,op2:option T.
75   (op1 = op2 → eq_option T f op1 op2 = true)).
76  #T; #f; #H;
77  #op1; #op2; nelim op1; nelim op2;
78  nnormalize;
79  ##[ ##1: #H1; napply refl_eq
80  ##| ##2: #a; #H1;
81          (* !!! ndestruct: assert false *)
82          nelim (option_destruct_none_some ?? H1)
83  ##| ##3: #a; #H1;
84           (* !!! ndestruct: assert false *)
85           nelim (option_destruct_some_none ?? H1)
86  ##| ##4: #a; #a0; #H1;
87           nrewrite > (H … (option_destruct_some_some … H1));
88           napply refl_eq
89  ##]
90 nqed.
91
92 nlemma eqoption_to_eq :
93 ∀T.∀f:T → T → bool.
94  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
95  (∀op1,op2:option T.
96   (eq_option T f op1 op2 = true → op1 = op2)).
97  #T; #f; #H;
98  #op1; #op2; nelim op1; nelim op2;
99  nnormalize;
100  ##[ ##1: #H1; napply refl_eq
101  ##| ##2,3: #a; #H1; ndestruct (*napply (bool_destruct … H1)*)
102  ##| ##4: #a; #a0; #H1;
103           nrewrite > (H … H1);
104           napply refl_eq
105  ##]
106 nqed.
107
108 nlemma decidable_option :
109 ∀T.(Πx,y:T.decidable (x = y)) →
110    (∀x,y:option T.decidable (x = y)).
111  #T; #H; #x; nelim x;
112  ##[ ##1: #y; ncases y;
113           ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
114           ##| ##2: #yy; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
115                    nnormalize; #H1;
116                    (* !!! ndestruct: assert false *)
117                    napply (option_destruct_none_some T … H1)
118           ##]
119  ##| ##2: #xx; #y; ncases y;
120           ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
121                    nnormalize; #H2;
122                    (* !!! ndestruct: assert false *)
123                    napply (option_destruct_some_none T … H2)
124           ##| ##2: #yy; nnormalize; napply (or2_elim (xx = yy) (xx ≠ yy) ? (H …));
125                    ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
126                             nnormalize; #H2;
127                             napply (H1 (option_destruct_some_some T … H2))
128                    ##| ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
129                             nrewrite > H1; napply refl_eq
130                    ##]
131           ##]
132  ##]
133 nqed.
134
135 nlemma neq_to_neqoption :
136 ∀T.∀f:T → T → bool.
137  (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
138  (∀op1,op2:option T.
139   (op1 ≠ op2 → eq_option T f op1 op2 = false)).
140  #T; #f; #H; #op1; nelim op1;
141  ##[ ##1: #op2; ncases op2;
142           ##[ ##1: nnormalize; #H1; nelim (H1 (refl_eq …))
143           ##| ##2: #yy; nnormalize; #H1; napply refl_eq
144           ##]
145  ##| ##2: #xx; #op2; ncases op2;
146           ##[ ##1: nnormalize; #H1; napply refl_eq
147           ##| ##2: #yy; nnormalize; #H1; napply (H xx yy …);
148                    nnormalize; #H2; nrewrite > H2 in H1:(%); #H1;
149                    napply (H1 (refl_eq …))
150           ##]
151  ##]
152 nqed.
153
154 nlemma neqoption_to_neq :
155 ∀T.∀f:T → T → bool.
156  (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
157  (∀op1,op2:option T.
158   (eq_option T f op1 op2 = false → op1 ≠ op2)).
159  #T; #f; #H; #op1; nelim op1;
160  ##[ ##1: #op2; ncases op2;
161           ##[ ##1: nnormalize; #H1;
162                    ndestruct (*napply (bool_destruct … H1)*)
163           ##| ##2: #yy; nnormalize; #H1; #H2;
164                    (* !!! ndestruct: assert false *)
165                    napply (option_destruct_none_some T … H2)
166           ##]
167  ##| ##2: #xx; #op2; ncases op2;
168           ##[ ##1: nnormalize; #H1; #H2;
169                    (* !!! ndestruct: assert false *)
170                    napply (option_destruct_some_none T … H2)
171           ##| ##2: #yy; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
172                    napply (option_destruct_some_some T … H2)
173           ##]
174  ##]
175 nqed.
176
177 nlemma option_is_comparable :
178  comparable → comparable.
179  #T; napply (mk_comparable (option T));
180  ##[ napply (None ?)
181  ##| napply (λx.false)
182  ##| napply (eq_option … (eqc T))
183  ##| napply (eqoption_to_eq … (eqc T));
184      napply (eqc_to_eq T)
185  ##| napply (eq_to_eqoption … (eqc T));
186      napply (eq_to_eqc T)
187  ##| napply (neqoption_to_neq … (eqc T));
188      napply (neqc_to_neq T)
189  ##| napply (neq_to_neqoption … (eqc T));
190      napply (neq_to_neqc T)
191  ##| napply decidable_option;
192      napply (decidable_c T)
193  ##| napply symmetric_eqoption;
194      napply (symmetric_eqc T)
195  ##]
196 nqed.
197
198 unification hint 0 ≔ S: comparable;
199          T ≟ (carr S),
200          X ≟ (option_is_comparable S)
201  (*********************************************) ⊢
202          carr X ≡ option T.