(no commit message)

[helm.git] / helm / software / matita / contribs / ng_assembly / common / theory.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index f963517755208101971ec44ab47ff9b87f8b4549..bab796daa3b732a1714d2a50909eba646dc263aa 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -16,13 +16,14 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
 universe constraint Type[0] < Type[1].
 universe constraint Type[1] < Type[2].
 universe constraint Type[2] < Type[3].
+universe constraint Type[3] < Type[4].
 
 (* ********************************** *)
 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
@@ -40,7 +41,6 @@ ndefinition Not: Prop → Prop ≝
 
 interpretation "logical not" 'not x = (Not x).
 
-(*
 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  #A; #C; #H;
  nnormalize;
@@ -178,6 +178,8 @@ ninductive Or2 (A,B:Prop) : Prop ≝
 
 interpretation "logical or" 'or x y = (Or2 x y).
 
+ndefinition decidable ≝ λA:Prop.A ∨ (¬A).
+
 nlemma or2_elim
  : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
  #P1; #P2; #Q; #H; #f1; #f2;
@@ -438,22 +440,18 @@ interpretation "exists" 'exists x = (ex ? x).
 
 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
-*)
 
 (* higher_order_defs/relations *)
 
 ndefinition relation : Type → Type ≝
-λA:Type.A → A → Prop. 
+λA.A → A → Prop. 
 
-(*
 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x:A.R x x.
-*)
 
 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x,y:A.R x y → R y x.
 
-(*
 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 
@@ -468,18 +466,18 @@ ndefinition tight_apart : ∀A:Type.∀eq,ap:relation 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.
 
+ndefinition refl ≝ refl_eq.
+
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 
-(*
 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
  #T1; #T2; #x; #y; #f; #H;
  nrewrite < H;
@@ -498,7 +496,6 @@ nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) 
  nnormalize; #H; #H1;
  napply (H (eq_f … H1)).
 nqed.
-*)
 
 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  #A;
@@ -508,13 +505,92 @@ nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  napply refl_eq.
 nqed.
 
-nlemma eq_ind_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
+nlemma eq_ind_r: ∀A:Type[0].∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
  #A; #x; #P; #H; #y; #H1;
  nrewrite < (symmetric_eq … H1);
  napply H.
 nqed.
 
-(*
+ndefinition R0 ≝ λT:Type[0].λt:T.t.
+
+ndefinition R1 ≝ eq_rect_Type0.
+
+ndefinition R2 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl_eq ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
+  T2 b0 e0 b1 e1.
+ #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
+ napply (eq_rect_Type0 ????? e1);
+ napply (R1 ?? ? ?? e0);
+ napply a2;
+nqed.
+
+ndefinition R3 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl_eq ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
+  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
+      ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
+  ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
+  ∀b2: T2 b0 e0 b1 e1.
+  ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
+  T3 b0 e0 b1 e1 b2 e2.
+ #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
+ napply (eq_rect_Type0 ????? e2);
+ napply (R2 ?? ? ???? e0 ? e1);
+ napply a3;
+nqed.
+
+ndefinition R4 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
+  ∀a1:T1 a0 (refl_eq T0 a0).
+  ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+  ∀a2:T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1).
+  ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+  ∀a3:T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
+      a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2). 
+  ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+      ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. 
+      Type[0].
+  ∀a4:T4 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
+      a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2) 
+      a3 (refl_eq (T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
+                   a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2))
+                   a3).
+  ∀b0:T0.
+  ∀e0:eq (T0 …) a0 b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
+  ∀b2: T2 b0 e0 b1 e1.
+  ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
+  ∀b3: T3 b0 e0 b1 e1 b2 e2.
+  ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
+  T4 b0 e0 b1 e1 b2 e2 b3 e3.
+ #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
+ napply (eq_rect_Type0 ????? e3);
+ napply (R3 ????????? e0 ? e1 ? e2);
+ napply a4;
+nqed.
+
 nlemma symmetric_neq : ∀T:Type.∀x,y:T.x ≠ y → y ≠ x.
  #T; #x; #y;
  nnormalize;
@@ -531,12 +607,3 @@ ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 
 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).
-*)
-
-ninductive bool : Type ≝
- true : bool |
- false : bool.
-
-nlemma pippo : (true = false) → (false = true).
- #H; ndestruct.
-nqed.