(* 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 *)
#A; #C; #H;
nnormalize;
#H1;
- nelim (H1 H);
+ nelim (H1 H).
nqed.
nlemma not_to_not : ∀A,B:Prop. (A → B) → ((¬B) → (¬A)).
interpretation "logical or" 'or x y = (Or2 x y).
-ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
+ndefinition decidable ≝ λA:Prop.A ∨ (¬A).
nlemma or2_elim
: ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
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:Type.A → A → Prop.
+λA.A → A → Prop.
ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
λA.λR.∀x:A.R x x.
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)).
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.
-nlemma symmetric_neq : ∀T.∀x,y:T.x ≠ y → y ≠ x.
+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;
#H; #H1;
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)));
-*)
projects / helm.git / blobdiff