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: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/pts.ma".
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 ninductive And (A,B:Prop) : Prop ≝
56 conj : A → B → (And A B).
58 interpretation "logical and" 'and x y = (And x y).
60 nlemma proj1: ∀A,B:Prop.A ∧ B → A.
62 napply (And_ind A B ?? H);
67 nlemma proj2: ∀A,B:Prop.A ∧ B → B.
69 napply (And_ind A B ?? H);
74 ninductive Or (A,B:Prop) : Prop ≝
75 or_introl : A → (Or A B)
76 | or_intror : B → (Or A B).
78 interpretation "logical or" 'or x y = (Or x y).
80 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
82 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
83 ex_intro: ∀x:A.Q x → ex A Q.
85 interpretation "exists" 'exists x = (ex ? x).
87 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
88 ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
91 λA,B.(A -> B) ∧ (B -> A).
93 (* higher_order_defs/relations *)
95 ndefinition relation : Type → Type ≝
98 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
101 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
102 λA.λR.∀x,y:A.R x y → R y x.
104 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
105 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
107 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
108 λA.λR.∀x:A.¬ (R x x).
110 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
111 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
113 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
114 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
116 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
117 λA.λR.∀x,y:A.R x y → ¬ (R y x).
119 (* logic/equality.ma *)
121 ninductive eq (A:Type) (x:A) : A → Prop ≝
124 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
126 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
128 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
136 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
137 #A; #x; #P; #H; #y; #H1;
138 nrewrite < (symmetric_eq ??? H1);
142 ndefinition relationT : Type → Type → Type ≝
145 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
146 λA,T.λR.∀x,y:A.R x y = R y x.
148 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
149 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
153 ninductive list (A:Type) : Type ≝
155 | cons: A -> list A -> list A.
157 nlet rec append A (l1: list A) l2 on l1 ≝
160 | (cons hd tl) => cons A hd (append A tl l2) ].
162 notation "hvbox(hd break :: tl)"
163 right associative with precedence 47
164 for @{'cons $hd $tl}.
166 notation "[ list0 x sep ; ]"
167 non associative with precedence 90
168 for ${fold right @'nil rec acc @{'cons $x $acc}}.
170 notation "hvbox(l1 break @ l2)"
171 right associative with precedence 47
172 for @{'append $l1 $l2 }.
174 interpretation "nil" 'nil = (nil ?).
175 interpretation "cons" 'cons hd tl = (cons ? hd tl).
176 interpretation "append" 'append l1 l2 = (append ? l1 l2).
178 nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → x1 = x2.
179 #T; #x1; #x2; #y1; #y2; #H;
180 nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
186 nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
187 #T; #x1; #x2; #y1; #y2; #H;
188 nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
194 nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
196 nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
202 nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
204 nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
210 nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
214 ##[ ##1: napply (refl_eq ??)
221 nlemma associative_list : ∀T.associative (list T) (append T).
225 ##[ ##1: napply (refl_eq ??)
232 nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
238 nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
240 nrewrite > (associative_list T l [a] l1);