1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 universe constraint Type[0] < Type[1].
25 (* ********************************** *)
26 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
27 (* ********************************** *)
29 (* logic/connectives.ma *)
31 ninductive True: Prop ≝
34 ninductive False: Prop ≝.
36 ndefinition Not: Prop → Prop ≝
39 interpretation "logical not" 'not x = (Not x).
41 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
48 nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
55 nlemma prop_to_nnprop : ∀P.P → ¬¬P.
56 #P; nnormalize; #H; #H1;
60 ninductive And2 (A,B:Prop) : Prop ≝
61 conj2 : A → B → (And2 A B).
63 interpretation "logical and" 'and x y = (And2 x y).
65 nlemma proj2_1: ∀A,B:Prop.A ∧ B → A.
67 napply (And2_ind A B … H);
72 nlemma proj2_2: ∀A,B:Prop.A ∧ B → B.
74 napply (And2_ind A B … H);
79 ninductive And3 (A,B,C:Prop) : Prop ≝
80 conj3 : A → B → C → (And3 A B C).
82 nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A.
84 napply (And3_ind A B C … H);
89 nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B.
91 napply (And3_ind A B C … H);
96 nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C.
98 napply (And3_ind A B C … H);
103 ninductive And4 (A,B,C,D:Prop) : Prop ≝
104 conj4 : A → B → C → D → (And4 A B C D).
106 nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A.
108 napply (And4_ind A B C D … H);
113 nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B.
115 napply (And4_ind A B C D … H);
120 nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C.
122 napply (And4_ind A B C D … H);
127 nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D.
129 napply (And4_ind A B C D … H);
134 ninductive And5 (A,B,C,D,E:Prop) : Prop ≝
135 conj5 : A → B → C → D → E → (And5 A B C D E).
137 nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A.
138 #A; #B; #C; #D; #E; #H;
139 napply (And5_ind A B C D E … H);
140 #H1; #H2; #H3; #H4; #H5;
144 nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B.
145 #A; #B; #C; #D; #E; #H;
146 napply (And5_ind A B C D E … H);
147 #H1; #H2; #H3; #H4; #H5;
151 nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C.
152 #A; #B; #C; #D; #E; #H;
153 napply (And5_ind A B C D E … H);
154 #H1; #H2; #H3; #H4; #H5;
158 nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D.
159 #A; #B; #C; #D; #E; #H;
160 napply (And5_ind A B C D E … H);
161 #H1; #H2; #H3; #H4; #H5;
165 nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E.
166 #A; #B; #C; #D; #E; #H;
167 napply (And5_ind A B C D E … H);
168 #H1; #H2; #H3; #H4; #H5;
172 ninductive Or2 (A,B:Prop) : Prop ≝
173 or2_intro1 : A → (Or2 A B)
174 | or2_intro2 : B → (Or2 A B).
176 interpretation "logical or" 'or x y = (Or2 x y).
178 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
181 : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
182 #P1; #P2; #Q; #H; #f1; #f2;
183 napply (Or2_ind P1 P2 ? f1 f2 ?);
187 ninductive Or3 (A,B,C:Prop) : Prop ≝
188 or3_intro1 : A → (Or3 A B C)
189 | or3_intro2 : B → (Or3 A B C)
190 | or3_intro3 : C → (Or3 A B C).
193 : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q.
194 #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3;
195 napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?);
199 ninductive Or4 (A,B,C,D:Prop) : Prop ≝
200 or4_intro1 : A → (Or4 A B C D)
201 | or4_intro2 : B → (Or4 A B C D)
202 | or4_intro3 : C → (Or4 A B C D)
203 | or4_intro4 : D → (Or4 A B C D).
206 : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q.
207 ∀f3:P3 → Q.∀f4:P4 → Q.Q.
208 #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4;
209 napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?);
213 ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
214 or5_intro1 : A → (Or5 A B C D E)
215 | or5_intro2 : B → (Or5 A B C D E)
216 | or5_intro3 : C → (Or5 A B C D E)
217 | or5_intro4 : D → (Or5 A B C D E)
218 | or5_intro5 : E → (Or5 A B C D E).
221 : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
222 ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
223 #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
224 napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
228 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
229 ex_intro: ∀x:A.Q x → ex A Q.
231 interpretation "exists" 'exists x = (ex ? x).
233 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
234 ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
237 λA,B.(A → B) ∧ (B → A).
239 (* higher_order_defs/relations *)
241 ndefinition relation : Type → Type ≝
242 λA:Type.A → A → Prop.
244 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
247 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
248 λA.λR.∀x,y:A.R x y → R y x.
250 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
251 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
253 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
254 λA.λR.∀x:A.¬ (R x x).
256 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
257 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
259 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
260 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
262 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
263 λA.λR.∀x,y:A.R x y → ¬ (R y x).
265 (* logic/equality.ma *)
267 ninductive eq (A:Type) (x:A) : A → Prop ≝
270 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
272 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
274 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
275 #T1; #T2; #x; #y; #f; #H;
280 nlemma eq_f2 : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.x1 = y1 → x2 = y2 → f x1 x2 = f y1 y2.
281 #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2;
287 nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y.
288 #T1; #T2; #x; #y; #f;
290 napply (H (eq_f … H1)).
293 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
301 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
302 #A; #x; #P; #H; #y; #H1;
303 nrewrite < (symmetric_eq … H1);
307 ndefinition relationT : Type → Type → Type ≝
310 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
311 λA,T.λR.∀x,y:A.R x y = R y x.
313 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
314 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).