(* SOTTOINSIEME MINIMALE DELLA TEORIA *)
(* ********************************** *)
+(* logic/connectives.ma *)
+
ninductive True: Prop ≝
I : True.
interpretation "logical not" 'not x = (Not x).
-ntheorem absurd : ∀A,C:Prop.A → ¬A → C.
+nlemma absurd : ∀A,C:Prop.A → ¬A → C.
#A; #C; #H;
nnormalize;
#H1;
nelim (H1 H).
nqed.
-ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
+nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
#A; #B; #H;
nnormalize;
#H1; #H2;
interpretation "logical and" 'and x y = (And x y).
-ntheorem proj1: ∀A,B:Prop.A ∧ B → A.
+nlemma proj1: ∀A,B:Prop.A ∧ B → A.
#A; #B; #H;
napply (And_ind A B ?? H);
#H1; #H2;
napply H1.
nqed.
-ntheorem proj2: ∀A,B:Prop.A ∧ B → B.
+nlemma proj2: ∀A,B:Prop.A ∧ B → B.
#A; #B; #H;
napply (And_ind A B ?? H);
#H1; #H2;
ndefinition iff ≝
λA,B.(A -> B) ∧ (B -> A).
+(* higher_order_defs/relations *)
+
ndefinition relation : Type → Type ≝
λA:Type.A → A → Prop.
ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
λA.λR.∀x,y:A.R x y → ¬ (R y x).
+(* logic/equality.ma *)
+
ninductive eq (A:Type) (x:A) : A → Prop ≝
refl_eq : eq A x x.
interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
-ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
+nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
#A;
nnormalize;
#x; #y; #H;
napply (refl_eq ??).
nqed.
-ntheorem eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
+nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
#A; #x; #P; #H; #y; #H1;
napply (eq_ind ? x ? H y ?);
nrewrite < H1;
napply (refl_eq ??).
nqed.
+
+ndefinition relationT : Type → Type → Type ≝
+λA,T:Type.A → A → T.
+
+ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
+λA,T.λR.∀x,y:A.R x y = R y x.
+
+ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
+λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
+
+(* list/list.ma *)
+
+ninductive list (A:Type) : Type ≝
+ nil: list A
+| cons: A -> list A -> list A.
+
+nlet rec list_ind (A:Type) (P:list A → Prop) (p:P (nil A)) (f:(Πa:A.Πl':list A.P l' → P (cons A a l'))) (l:list A) on l ≝
+ match l with [ nil ⇒ p | cons h t ⇒ f h t (list_ind A P p f t) ].
+
+nlet rec list_rec (A:Type) (P:list A → Set) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
+ match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rec A P p f t) ].
+
+nlet rec list_rect (A:Type) (P:list A → Type) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
+ match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rect A P p f t) ].
+
+nlet rec append A (l1: list A) l2 on l1 ≝
+ match l1 with
+ [ nil => l2
+ | (cons hd tl) => cons A hd (append A tl l2) ].
+
+notation "hvbox(hd break :: tl)"
+ right associative with precedence 47
+ for @{'cons $hd $tl}.
+
+notation "[ list0 x sep ; ]"
+ non associative with precedence 90
+ for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+ right associative with precedence 47
+ for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → x1 = x2.
+ #T; #x1; #x2; #y1; #y2; #H;
+ nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
+ #T; #x1; #x2; #y1; #y2; #H;
+ nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
+ #T; #x; #y; #H;
+ nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
+ nrewrite > H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
+ #T; #x; #y; #H;
+ nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
+ #T; #l;
+ napply (list_ind T ??? l);
+ nnormalize;
+ ##[ ##1: napply (refl_eq ??)
+ ##| ##2: #x; #y; #H;
+ nrewrite > H;
+ napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma associative_list : ∀T.associative (list T) (append T).
+ #T; #x; #y; #z;
+ napply (list_ind T ??? x);
+ nnormalize;
+ ##[ ##1: napply (refl_eq ??)
+ ##| ##2: #a; #b; #H;
+ nrewrite > H;
+ napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
+ #T; #l1; #l2; #a;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
+ #T; #a; #l; #l1;
+ nrewrite > (associative_list T l [a] l1);
+ nnormalize;
+ napply (refl_eq ??).
+nqed.