]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/num/comp_num_lemmas.ma
update in binaries for λδ
[helm.git] / matita / matita / contribs / ng_assembly / num / comp_num_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 "num/comp_num.ma".
24 include "num/bool_lemmas.ma".
25
26 (* **** *)
27 (* BYTE *)
28 (* **** *)
29
30 nlemma cn_destruct_1 :
31 ∀T.∀x1,x2,y1,y2:T.
32  mk_comp_num T x1 y1 = mk_comp_num T x2 y2 → x1 = x2.
33  #T; #x1; #x2; #y1; #y2; #H;
34  nchange with (match mk_comp_num ? x2 y2 with [ mk_comp_num a _ ⇒ x1 = a ]);
35  nrewrite < H;
36  nnormalize;
37  napply refl_eq.
38 nqed.
39
40 nlemma cn_destruct_2 :
41 ∀T.∀x1,x2,y1,y2:T.
42  mk_comp_num T x1 y1 = mk_comp_num T x2 y2 → y1 = y2.
43  #T; #x1; #x2; #y1; #y2; #H;
44  nchange with (match mk_comp_num ? x2 y2 with [ mk_comp_num _ b ⇒ y1 = b ]);
45  nrewrite < H;
46  nnormalize;
47  napply refl_eq.
48 nqed.
49
50 nlemma symmetric_eqcn :
51 ∀T.∀feq:T → T → bool.
52  (symmetricT T bool feq) →
53  (symmetricT (comp_num T) bool (eq2_cn T feq)).
54  #T; #feq; #H;
55  #b1; nelim b1; #e1; #e2;
56  #b2; nelim b2; #e3; #e4;
57  nchange with (((feq e1 e3)⊗(feq e2 e4)) = ((feq e3 e1)⊗(feq e4 e2)));
58  nrewrite > (H e1 e3);
59  nrewrite > (H e2 e4);
60  napply refl_eq.
61 nqed.
62
63 nlemma eqcn_to_eq :
64 ∀T.∀feq:T → T → bool.
65  (∀x,y:T.(feq x y = true) → (x = y)) →
66  (∀b1,b2:comp_num T.
67   ((eq2_cn T feq b1 b2 = true) → (b1 = b2))).
68  #T; #feq; #H; #b1; #b2;
69  nelim b1; #e1; #e2;
70  nelim b2; #e3; #e4;
71  nchange in ⊢ (% → ?) with (((feq e1 e3)⊗(feq e2 e4)) = true);
72  #H1;
73  nrewrite < (H … (andb_true_true_l … H1));
74  nrewrite < (H … (andb_true_true_r … H1));
75  napply refl_eq.
76 nqed.
77
78 nlemma eq_to_eqcn :
79 ∀T.∀feq:T → T → bool.
80  (∀x,y:T.(x = y) → (feq x y = true)) →
81  (∀b1,b2:comp_num T.
82   ((b1 = b2) → (eq2_cn T feq b1 b2 = true))).
83  #T; #feq; #H; #b1; #b2;
84  nelim b1; #e1; #e2;
85  nelim b2; #e3; #e4;
86  #H1;
87  nrewrite < (cn_destruct_1 … H1);
88  nrewrite < (cn_destruct_2 … H1);
89  nchange with (((feq e1 e1)⊗(feq e2 e2)) = true);
90  nrewrite > (H e1 e1 (refl_eq …));
91  nrewrite > (H e2 e2 (refl_eq …)); 
92  nnormalize;
93  napply refl_eq.
94 nqed.
95
96 nlemma decidable_cn_aux1 :
97 ∀T.∀e1,e2,e3,e4:T.e1 ≠ e3 → (mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4).
98  #T; #e1; #e2; #e3; #e4;
99  nnormalize; #H; #H1;
100  napply (H (cn_destruct_1 … H1)).
101 nqed.
102
103 nlemma decidable_cn_aux2 :
104 ∀T.∀e1,e2,e3,e4:T.e2 ≠ e4 → (mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4).
105  #T; #e1; #e2; #e3; #e4;
106  nnormalize; #H; #H1;
107  napply (H (cn_destruct_2 … H1)).
108 nqed.
109
110 nlemma decidable_cn :
111 ∀T.(∀x,y:T.decidable (x = y)) →
112    (∀b1,b2:comp_num T.
113     (decidable (b1 = b2))).
114  #T; #H;
115  #b1; nelim b1; #e1; #e2;
116  #b2; nelim b2; #e3; #e4;
117  nnormalize;
118  napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (H e1 e3) …);
119  ##[ ##2: #H1; napply (or2_intro2 … (decidable_cn_aux1 T e1 e2 e3 e4 H1))
120  ##| ##1: #H1; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (H e2 e4) …);
121           ##[ ##2: #H2; napply (or2_intro2 … (decidable_cn_aux2 T e1 e2 e3 e4 H2))
122           ##| ##1: #H2; nrewrite > H1; nrewrite > H2;
123                         napply (or2_intro1 … (refl_eq ? (mk_comp_num T e3 e4)))
124           ##]
125  ##]
126 nqed.
127
128 nlemma neqcn_to_neq :
129 ∀T.∀feq:T → T → bool.
130  (∀x,y:T.(feq x y = false) → (x ≠ y)) →
131  (∀b1,b2:comp_num T.
132   ((eq2_cn T feq b1 b2 = false) → (b1 ≠ b2))).
133  #T; #feq; #H; #b1; #b2;
134  nelim b1; #e1; #e2;
135  nelim b2; #e3; #e4;
136  nchange with ((((feq e1 e3) ⊗ (feq e2 e4)) = false) → ?);
137  #H1;
138  napply (or2_elim ((feq e1 e3) = false) ((feq e2 e4) = false) ? (andb_false2 … H1) …);
139  ##[ ##1: #H2; napply (decidable_cn_aux1 … (H … H2))
140  ##| ##2: #H2; napply (decidable_cn_aux2 … (H … H2))
141  ##]
142 nqed.
143
144 nlemma cn_destruct :
145 ∀T.(∀x,y:T.decidable (x = y)) →
146    (∀e1,e2,e3,e4:T.
147     ((mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4)) →
148     ((e1 ≠ e3) ∨ (e2 ≠ e4))).
149  #T; #H; #e1; #e2; #e3; #e4;
150  nnormalize; #H1;
151  napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (H e1 e3) …);
152  ##[ ##2: #H2; napply (or2_intro1 … H2)
153  ##| ##1: #H2; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (H e2 e4) …);
154           ##[ ##2: #H3; napply (or2_intro2 … H3)
155           ##| ##1: #H3; nrewrite > H2 in H1:(%);
156                    nrewrite > H3;
157                    #H1; nelim (H1 (refl_eq …))
158           ##]
159  ##]
160 nqed.
161
162 nlemma neq_to_neqcn :
163 ∀T.∀feq:T → T → bool.
164  (∀x,y:T.(x ≠ y) → (feq x y = false)) →
165  (∀x,y:T.decidable (x = y)) →
166  (∀b1,b2:comp_num T.
167   ((b1 ≠ b2) → (eq2_cn T feq b1 b2 = false))).
168  #T; #feq; #H; #H1; #b1; #b2;
169  nelim b1; #e1; #e2;
170  nelim b2; #e3; #e4;
171  #H2; nchange with (((feq e1 e3) ⊗ (feq e2 e4)) = false);
172  napply (or2_elim (e1 ≠ e3) (e2 ≠ e4) ? (cn_destruct T H1 e1 e2 e3 e4 … H2) …);
173  ##[ ##1: #H3; nrewrite > (H … H3); nnormalize; napply refl_eq
174  ##| ##2: #H3; nrewrite > (H … H3);
175           nrewrite > (symmetric_andbool (feq e1 e3) false);
176           nnormalize; napply refl_eq
177  ##]
178 nqed.