X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Ftheory.ma;h=b6a84d6af9dcff803e6da3e03206505ed634446d;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=bab796daa3b732a1714d2a50909eba646dc263aa;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index bab796daa..b6a84d6af 100644
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -16,14 +16,13 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
 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 *)
@@ -45,7 +44,7 @@ nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  #A; #C; #H;
  nnormalize;
  #H1;
- nelim (H1 H).
+ nelim (H1 H);
 nqed.
 
 nlemma not_to_not : ∀A,B:Prop. (A → B) → ((¬B) → (¬A)).
@@ -178,7 +177,7 @@ ninductive Or2 (A,B:Prop) : Prop ≝
 
 interpretation "logical or" 'or x y = (Or2 x y).
 
-ndefinition decidable ≝ λA:Prop.A ∨ (¬A).
+ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
 
 nlemma or2_elim
  : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
@@ -441,10 +440,13 @@ 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.
 
+ndefinition iff ≝
+λA,B.(A → B) ∧ (B → A).
+
 (* higher_order_defs/relations *)
 
 ndefinition relation : Type → Type ≝
-λA.A → A → Prop. 
+λA:Type.A → A → Prop. 
 
 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x:A.R x x.
@@ -472,8 +474,6 @@ ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 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)).
@@ -505,93 +505,13 @@ nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  napply refl_eq.
 nqed.
 
-nlemma eq_ind_r: ∀A:Type[0].∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
+nlemma eq_ind_r: ∀A:Type.∀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.
+nlemma symmetric_neq : ∀T.∀x,y:T.x ≠ y → y ≠ x.
  #T; #x; #y;
  nnormalize;
  #H; #H1;
@@ -607,3 +527,36 @@ 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).
+
+(* aggiunta per bypassare i punti in cui le dimostrazioni sono equivalenti *)
+(*
+ninductive peqv (A:Prop) (x:A) : A → Prop ≝
+ prefl_eqv : peqv A x x.
+
+interpretation "prop equivalence" 'preqv t x y = (peqv t x y).
+*)
+(* \equiv *)
+(*
+notation > "hvbox(a break ≡ b)" 
+  non associative with precedence 45
+for @{ 'preqv ? $a $b }.
+
+nlemma symmetric_peqv: ∀A:Prop. symmetric A (peqv A).
+ #A;
+ nnormalize;
+ #x; #y; #H;
+ napply (peqv_ind A x (λ_.?) ? y H);
+ napply prefl_eqv.
+nqed.
+
+nlemma peqv_ind_r: ∀A:Prop.∀x:A.∀P:A → Prop.P x → ∀y:A.y ≡ x → P y.
+ #A; #x; #P; #H; #y; #H1;
+ napply (peqv_ind A x (λ_.?) H y (symmetric_peqv … H1)).
+nqed.
+
+naxiom peqv_ax : ∀P:Prop.∀Q,R:P.Q ≡ R.
+*)
+(* uso P x → P y, H e' P x
+   nrewrite > cioe' napply (peqv_ind ? x (λ_.?) H y (dimostrazione di x ≡ y));
+   nrewrite < cioe' napply (peqv_ind_r ? x ? H y (dimostrazione y ≡ x)));
+*)