]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/freescale/theory.ma
freescale porting, work in progress
[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / theory.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "freescale/pts.ma".
24
25 (* ********************************** *)
26 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
27 (* ********************************** *)
28
29 (* logic/connectives.ma *)
30
31 ninductive True: Prop ≝
32  I : True.
33
34 ninductive False: Prop ≝.
35
36 ndefinition Not: Prop → Prop ≝
37 λA.(A → False).
38
39 interpretation "logical not" 'not x = (Not x).
40
41 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
42  #A; #C; #H;
43  nnormalize;
44  #H1;
45  nelim (H1 H);
46 nqed.
47
48 nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
49  #A; #B; #H;
50  nnormalize;
51  #H1; #H2;
52  nelim (H1 (H H2)).
53 nqed.
54
55 ninductive And (A,B:Prop) : Prop ≝
56  conj : A → B → (And A B).
57
58 interpretation "logical and" 'and x y = (And x y).
59
60 nlemma proj1: ∀A,B:Prop.A ∧ B → A.
61  #A; #B; #H;
62  (* \ldots al posto di ??? *)
63  napply (And_ind A B … H);
64  #H1; #H2;
65  napply H1.
66 nqed.
67
68 nlemma proj2: ∀A,B:Prop.A ∧ B → B.
69  #A; #B; #H;
70  napply (And_ind A B … H);
71  #H1; #H2;
72  napply H2.
73 nqed.
74
75 ninductive Or (A,B:Prop) : Prop ≝
76   or_introl : A → (Or A B)
77 | or_intror : B → (Or A B).
78
79 interpretation "logical or" 'or x y = (Or x y).
80
81 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
82
83 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
84  ex_intro: ∀x:A.Q x → ex A Q.
85
86 interpretation "exists" 'exists x = (ex ? x).
87
88 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
89  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
90
91 ndefinition iff ≝
92 λA,B.(A → B) ∧ (B → A).
93
94 (* higher_order_defs/relations *)
95
96 ndefinition relation : Type → Type ≝
97 λA:Type.A → A → Prop. 
98
99 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
100 λA.λR.∀x:A.R x x.
101
102 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
103 λA.λR.∀x,y:A.R x y → R y x.
104
105 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
106 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
107
108 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
109 λA.λR.∀x:A.¬ (R x x).
110
111 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
112 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
113
114 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
115 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
116
117 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
118 λA.λR.∀x,y:A.R x y → ¬ (R y x).
119
120 (* logic/equality.ma *)
121
122 ninductive eq (A:Type) (x:A) : A → Prop ≝
123  refl_eq : eq A x x.
124
125 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
126
127 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
128
129 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
130  #A;
131  nnormalize;
132  #x; #y; #H;
133  nrewrite < H;
134  napply refl_eq.
135 nqed.
136
137 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
138  #A; #x; #P; #H; #y; #H1;
139  nrewrite < (symmetric_eq … H1);
140  napply H.
141 nqed.
142
143 ndefinition relationT : Type → Type → Type ≝
144 λA,T:Type.A → A → T.
145
146 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
147 λA,T.λR.∀x,y:A.R x y = R y x.
148
149 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
150 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
151
152 (* list/list.ma *)
153
154 ninductive list (A:Type) : Type ≝
155   nil: list A
156 | cons: A → list A → list A.
157
158 nlet rec append A (l1: list A) l2 on l1 ≝
159  match l1 with
160   [ nil ⇒ l2
161   | (cons hd tl) ⇒ cons A hd (append A tl l2) ].
162
163 notation "hvbox(hd break :: tl)"
164   right associative with precedence 47
165   for @{'cons $hd $tl}.
166
167 notation "[ list0 x sep ; ]"
168   non associative with precedence 90
169   for ${fold right @'nil rec acc @{'cons $x $acc}}.
170
171 notation "hvbox(l1 break @ l2)"
172   right associative with precedence 47
173   for @{'append $l1 $l2 }.
174
175 interpretation "nil" 'nil = (nil ?).
176 interpretation "cons" 'cons hd tl = (cons ? hd tl).
177 interpretation "append" 'append l1 l2 = (append ? l1 l2).
178
179 nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → x1 = x2.
180  #T; #x1; #x2; #y1; #y2; #H;
181  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
182  nrewrite < H;
183  nnormalize;
184  napply refl_eq.
185 nqed.
186
187 nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
188  #T; #x1; #x2; #y1; #y2; #H;
189  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
190  nrewrite < H;
191  nnormalize;
192  napply refl_eq.
193 nqed.
194
195 nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
196  #T; #x; #y; #H;
197  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
198  nrewrite > H;
199  nnormalize;
200  napply I.
201 nqed.
202
203 nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
204  #T; #x; #y; #H;
205  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
206  nrewrite < H;
207  nnormalize;
208  napply I.
209 nqed.
210
211 nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
212  #T; #l;
213  nelim l;
214  nnormalize;
215  ##[ ##1: napply refl_eq
216  ##| ##2: #x; #y; #H;
217           nrewrite > H;
218           napply refl_eq
219  ##]
220 nqed.
221
222 nlemma associative_list : ∀T.associative (list T) (append T).
223  #T; #x; #y; #z;
224  nelim x;
225  nnormalize;
226  ##[ ##1: napply refl_eq
227  ##| ##2: #a; #b; #H;
228           nrewrite > H;
229           napply refl_eq
230  ##]
231 nqed.
232
233 nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
234  #T; #l1; #l2; #a;
235  nnormalize;
236  napply refl_eq.
237 nqed.
238
239 nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
240  #T; #a; #l; #l1;
241  nrewrite > (associative_list T l [a] l1);
242  nnormalize;
243  napply refl_eq.
244 nqed.