(* 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 *)
#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 ≝ λ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.
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.
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[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;
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