]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/common/option_lemmas.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / ng_assembly / common / option_lemmas.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/option.ma".
24 include "num/bool_lemmas.ma".
25
26 (* ****** *)
27 (* OPTION *)
28 (* ****** *)
29
30 nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
31  #T; #x1; #x2; #H;
32  nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
33  nrewrite < H;
34  nnormalize;
35  napply refl_eq.
36 nqed.
37
38 (* !!! da togliere *)
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 (* !!! da togliere *)
48 nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
49  #T; #x; #H;
50  nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
51  nrewrite < H;
52  nnormalize;
53  napply I.
54 nqed.
55
56 nlemma symmetric_eqoption :
57 ∀T:Type.∀f:T → T → bool.
58  (symmetricT T bool f) →
59  (∀op1,op2:option T.
60   (eq_option T f op1 op2 = eq_option T f op2 op1)).
61  #T; #f; #H;
62  #op1; #op2; nelim op1; nelim op2;
63  nnormalize;
64  ##[ ##1: napply refl_eq
65  ##| ##2,3: #H; napply refl_eq
66  ##| ##4: #a; #a0;
67           nrewrite > (H a0 a);
68           napply refl_eq
69  ##]
70 nqed.
71
72 nlemma eq_to_eqoption :
73 ∀T.∀f:T → T → bool.
74  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
75  (∀op1,op2:option T.
76   (op1 = op2 → eq_option T f op1 op2 = true)).
77  #T; #f; #H;
78  #op1; #op2; nelim op1; nelim op2;
79  nnormalize;
80  ##[ ##1: #H1; napply refl_eq
81  ##| ##2: #a; #H1;
82          (* !!! ndestruct: assert false *)
83          nelim (option_destruct_none_some ?? H1)
84  ##| ##3: #a; #H1;
85           (* !!! ndestruct: assert false *)
86           nelim (option_destruct_some_none ?? H1)
87  ##| ##4: #a; #a0; #H1;
88           nrewrite > (H … (option_destruct_some_some … H1));
89           napply refl_eq
90  ##]
91 nqed.
92
93 nlemma eqoption_to_eq :
94 ∀T.∀f:T → T → bool.
95  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
96  (∀op1,op2:option T.
97   (eq_option T f op1 op2 = true → op1 = op2)).
98  #T; #f; #H;
99  #op1; #op2; nelim op1; nelim op2;
100  nnormalize;
101  ##[ ##1: #H1; napply refl_eq
102  ##| ##2,3: #a; #H1; ndestruct (*napply (bool_destruct … H1)*)
103  ##| ##4: #a; #a0; #H1;
104           nrewrite > (H … H1);
105           napply refl_eq
106  ##]
107 nqed.
108
109 nlemma decidable_option :
110 ∀T.(Πx,y:T.decidable (x = y)) →
111    (∀x,y:option T.decidable (x = y)).
112  #T; #H; #x; nelim x;
113  ##[ ##1: #y; ncases y;
114           ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
115           ##| ##2: #yy; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
116                    nnormalize; #H1;
117                    (* !!! ndestruct: assert false *)
118                    napply (option_destruct_none_some T … H1)
119           ##]
120  ##| ##2: #xx; #y; ncases y;
121           ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
122                    nnormalize; #H2;
123                    (* !!! ndestruct: assert false *)
124                    napply (option_destruct_some_none T … H2)
125           ##| ##2: #yy; nnormalize; napply (or2_elim (xx = yy) (xx ≠ yy) ? (H …));
126                    ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
127                             nnormalize; #H2;
128                             napply (H1 (option_destruct_some_some T … H2))
129                    ##| ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
130                             nrewrite > H1; napply refl_eq
131                    ##]
132           ##]
133  ##]
134 nqed.
135
136 nlemma neq_to_neqoption :
137 ∀T.∀f:T → T → bool.
138  (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
139  (∀op1,op2:option T.
140   (op1 ≠ op2 → eq_option T f op1 op2 = false)).
141  #T; #f; #H; #op1; nelim op1;
142  ##[ ##1: #op2; ncases op2;
143           ##[ ##1: nnormalize; #H1; nelim (H1 (refl_eq …))
144           ##| ##2: #yy; nnormalize; #H1; napply refl_eq
145           ##]
146  ##| ##2: #xx; #op2; ncases op2;
147           ##[ ##1: nnormalize; #H1; napply refl_eq
148           ##| ##2: #yy; nnormalize; #H1; napply (H xx yy …);
149                    nnormalize; #H2; nrewrite > H2 in H1:(%); #H1;
150                    napply (H1 (refl_eq …))
151           ##]
152  ##]
153 nqed.
154
155 nlemma neqoption_to_neq :
156 ∀T.∀f:T → T → bool.
157  (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
158  (∀op1,op2:option T.
159   (eq_option T f op1 op2 = false → op1 ≠ op2)).
160  #T; #f; #H; #op1; nelim op1;
161  ##[ ##1: #op2; ncases op2;
162           ##[ ##1: nnormalize; #H1;
163                    ndestruct (*napply (bool_destruct … H1)*)
164           ##| ##2: #yy; nnormalize; #H1; #H2;
165                    (* !!! ndestruct: assert false *)
166                    napply (option_destruct_none_some T … H2)
167           ##]
168  ##| ##2: #xx; #op2; ncases op2;
169           ##[ ##1: nnormalize; #H1; #H2;
170                    (* !!! ndestruct: assert false *)
171                    napply (option_destruct_some_none T … H2)
172           ##| ##2: #yy; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
173                    napply (option_destruct_some_some T … H2)
174           ##]
175  ##]
176 nqed.