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 And (A,B:Prop) : Prop ≝
61 conj : A → B → (And A B).
63 interpretation "logical and" 'and x y = (And x y).
65 nlemma proj1: ∀A,B:Prop.A ∧ B → A.
67 (* \ldots al posto di ??? *)
68 napply (And_ind A B … H);
73 nlemma proj2: ∀A,B:Prop.A ∧ B → B.
75 napply (And_ind A B … H);
80 ninductive Or (A,B:Prop) : Prop ≝
81 or_introl : A → (Or A B)
82 | or_intror : B → (Or A B).
84 interpretation "logical or" 'or x y = (Or x y).
86 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
88 nlemma or_elim : ∀P,Q,G:Prop.Or P Q → ∀fp:P → G.∀fq:Q → G.G.
89 #P; #Q; #G; #H; #H1; #H2;
90 napply (Or_ind P Q ? H1 H2 ?);
94 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
95 ex_intro: ∀x:A.Q x → ex A Q.
97 interpretation "exists" 'exists x = (ex ? x).
99 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
100 ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
103 λA,B.(A → B) ∧ (B → A).
105 (* higher_order_defs/relations *)
107 ndefinition relation : Type → Type ≝
108 λA:Type.A → A → Prop.
110 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
113 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
114 λA.λR.∀x,y:A.R x y → R y x.
116 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
117 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
119 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
120 λA.λR.∀x:A.¬ (R x x).
122 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
123 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
125 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
126 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
128 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
129 λA.λR.∀x,y:A.R x y → ¬ (R y x).
131 (* logic/equality.ma *)
133 ninductive eq (A:Type) (x:A) : A → Prop ≝
136 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
138 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
140 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
141 #T1; #T2; #x; #y; #f; #H;
146 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.
147 #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2;
153 nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y.
154 #T1; #T2; #x; #y; #f;
156 napply (H (eq_f … H1)).
159 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
167 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
168 #A; #x; #P; #H; #y; #H1;
169 nrewrite < (symmetric_eq … H1);
173 ndefinition relationT : Type → Type → Type ≝
176 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
177 λA,T.λR.∀x,y:A.R x y = R y x.
179 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
180 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).