(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
nelim (H1 H);
nqed.
-nlemma 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;
napply (H1 H).
nqed.
-ninductive And (A,B:Prop) : Prop ≝
- conj : A → B → (And A B).
+ninductive And2 (A,B:Prop) : Prop ≝
+ conj2 : A → B → (And2 A B).
-interpretation "logical and" 'and x y = (And x y).
+interpretation "logical and" 'and x y = (And2 x y).
-nlemma proj1: ∀A,B:Prop.A ∧ B → A.
+nlemma proj2_1: ∀A,B:Prop.A ∧ B → A.
#A; #B; #H;
- (* \ldots al posto di ??? *)
- napply (And_ind A B … H);
+ napply (And2_ind A B … H);
#H1; #H2;
napply H1.
nqed.
-nlemma proj2: ∀A,B:Prop.A ∧ B → B.
+nlemma proj2_2: ∀A,B:Prop.A ∧ B → B.
#A; #B; #H;
- napply (And_ind A B … H);
+ napply (And2_ind A B … H);
#H1; #H2;
napply H2.
nqed.
-ninductive Or (A,B:Prop) : Prop ≝
- or_introl : A → (Or A B)
-| or_intror : B → (Or A B).
+ninductive And3 (A,B,C:Prop) : Prop ≝
+ conj3 : A → B → C → (And3 A B C).
-interpretation "logical or" 'or x y = (Or x y).
+nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A.
+ #A; #B; #C; #H;
+ napply (And3_ind A B C … H);
+ #H1; #H2; #H3;
+ napply H1.
+nqed.
+
+nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B.
+ #A; #B; #C; #H;
+ napply (And3_ind A B C … H);
+ #H1; #H2; #H3;
+ napply H2.
+nqed.
+
+nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C.
+ #A; #B; #C; #H;
+ napply (And3_ind A B C … H);
+ #H1; #H2; #H3;
+ napply H3.
+nqed.
+
+ninductive And4 (A,B,C,D:Prop) : Prop ≝
+ conj4 : A → B → C → D → (And4 A B C D).
+
+nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H1.
+nqed.
+
+nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H2.
+nqed.
+
+nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H3.
+nqed.
+
+nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H4.
+nqed.
+
+ninductive And5 (A,B,C,D,E:Prop) : Prop ≝
+ conj5 : A → B → C → D → E → (And5 A B C D E).
+
+nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H1.
+nqed.
+
+nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H2.
+nqed.
+
+nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H3.
+nqed.
+
+nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H4.
+nqed.
+
+nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H5.
+nqed.
+
+ninductive Or2 (A,B:Prop) : Prop ≝
+ or2_intro1 : A → (Or2 A B)
+| or2_intro2 : B → (Or2 A B).
+
+interpretation "logical or" 'or x y = (Or2 x y).
ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
-nlemma or_elim : ∀P,Q,G:Prop.Or P Q → ∀fp:P → G.∀fq:Q → G.G.
- #P; #Q; #G; #H; #H1; #H2;
- napply (Or_ind P Q ? H1 H2 ?);
+nlemma or2_elim
+ : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
+ #P1; #P2; #Q; #H; #f1; #f2;
+ napply (Or2_ind P1 P2 ? f1 f2 ?);
+ napply H.
+nqed.
+
+nlemma symmetric_or2 : ∀P1,P2.Or2 P1 P2 → Or2 P2 P1.
+ #P1; #P2; #H;
+ napply (or2_elim P1 P2 ? H);
+ ##[ ##1: #H1; napply (or2_intro2 P2 P1 H1)
+ ##| ##2: #H1; napply (or2_intro1 P2 P1 H1)
+ ##]
+nqed.
+
+ninductive Or3 (A,B,C:Prop) : Prop ≝
+ or3_intro1 : A → (Or3 A B C)
+| or3_intro2 : B → (Or3 A B C)
+| or3_intro3 : C → (Or3 A B C).
+
+nlemma or3_elim
+ : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q.
+ #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3;
+ napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?);
+ napply H.
+nqed.
+
+nlemma symmetric_or3_12 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P2 P1 P3.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro2 P2 P1 P3 H1)
+ ##| ##2: #H1; napply (or3_intro1 P2 P1 P3 H1)
+ ##| ##3: #H1; napply (or3_intro3 P2 P1 P3 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or3_13 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P3 P2 P1.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro3 P3 P2 P1 H1)
+ ##| ##2: #H1; napply (or3_intro2 P3 P2 P1 H1)
+ ##| ##3: #H1; napply (or3_intro1 P3 P2 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or3_23 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P1 P3 P2.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro1 P1 P3 P2 H1)
+ ##| ##2: #H1; napply (or3_intro3 P1 P3 P2 H1)
+ ##| ##3: #H1; napply (or3_intro2 P1 P3 P2 H1)
+ ##]
+nqed.
+
+ninductive Or4 (A,B,C,D:Prop) : Prop ≝
+ or4_intro1 : A → (Or4 A B C D)
+| or4_intro2 : B → (Or4 A B C D)
+| or4_intro3 : C → (Or4 A B C D)
+| or4_intro4 : D → (Or4 A B C D).
+
+nlemma or4_elim
+ : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q.
+ ∀f3:P3 → Q.∀f4:P4 → Q.Q.
+ #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4;
+ napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?);
napply H.
nqed.
+nlemma symmetric_or4_12 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P2 P1 P3 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro2 P2 P1 P3 P4 H1)
+ ##| ##2: #H1; napply (or4_intro1 P2 P1 P3 P4 H1)
+ ##| ##3: #H1; napply (or4_intro3 P2 P1 P3 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P2 P1 P3 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_13 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P3 P2 P1 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro3 P3 P2 P1 P4 H1)
+ ##| ##2: #H1; napply (or4_intro2 P3 P2 P1 P4 H1)
+ ##| ##3: #H1; napply (or4_intro1 P3 P2 P1 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P3 P2 P1 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_14 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P4 P2 P3 P1.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro4 P4 P2 P3 P1 H1)
+ ##| ##2: #H1; napply (or4_intro2 P4 P2 P3 P1 H1)
+ ##| ##3: #H1; napply (or4_intro3 P4 P2 P3 P1 H1)
+ ##| ##4: #H1; napply (or4_intro1 P4 P2 P3 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_23 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P3 P2 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P3 P2 P4 H1)
+ ##| ##2: #H1; napply (or4_intro3 P1 P3 P2 P4 H1)
+ ##| ##3: #H1; napply (or4_intro2 P1 P3 P2 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P1 P3 P2 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_24 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P4 P3 P2.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P4 P3 P2 H1)
+ ##| ##2: #H1; napply (or4_intro4 P1 P4 P3 P2 H1)
+ ##| ##3: #H1; napply (or4_intro3 P1 P4 P3 P2 H1)
+ ##| ##4: #H1; napply (or4_intro2 P1 P4 P3 P2 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_34 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P2 P4 P3.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P2 P4 P3 H1)
+ ##| ##2: #H1; napply (or4_intro2 P1 P2 P4 P3 H1)
+ ##| ##3: #H1; napply (or4_intro4 P1 P2 P4 P3 H1)
+ ##| ##4: #H1; napply (or4_intro3 P1 P2 P4 P3 H1)
+ ##]
+nqed.
+
+ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
+ or5_intro1 : A → (Or5 A B C D E)
+| or5_intro2 : B → (Or5 A B C D E)
+| or5_intro3 : C → (Or5 A B C D E)
+| or5_intro4 : D → (Or5 A B C D E)
+| or5_intro5 : E → (Or5 A B C D E).
+
+nlemma or5_elim
+ : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
+ ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
+ #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
+ napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
+ napply H.
+nqed.
+
+nlemma symmetric_or5_12 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P2 P1 P3 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro2 P2 P1 P3 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro1 P2 P1 P3 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P2 P1 P3 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P2 P1 P3 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P2 P1 P3 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_13 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P3 P2 P1 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro3 P3 P2 P1 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P3 P2 P1 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro1 P3 P2 P1 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P3 P2 P1 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P3 P2 P1 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_14 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P4 P2 P3 P1 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro4 P4 P2 P3 P1 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P4 P2 P3 P1 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P4 P2 P3 P1 P5 H1)
+ ##| ##4: #H1; napply (or5_intro1 P4 P2 P3 P1 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P4 P2 P3 P1 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_15 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P5 P2 P3 P4 P1.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro5 P5 P2 P3 P4 P1 H1)
+ ##| ##2: #H1; napply (or5_intro2 P5 P2 P3 P4 P1 H1)
+ ##| ##3: #H1; napply (or5_intro3 P5 P2 P3 P4 P1 H1)
+ ##| ##4: #H1; napply (or5_intro4 P5 P2 P3 P4 P1 H1)
+ ##| ##5: #H1; napply (or5_intro1 P5 P2 P3 P4 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_23 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P3 P2 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P3 P2 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro3 P1 P3 P2 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro2 P1 P3 P2 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P3 P2 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P3 P2 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_24 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P4 P3 P2 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P4 P3 P2 P5 H1)
+ ##| ##2: #H1; napply (or5_intro4 P1 P4 P3 P2 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P4 P3 P2 P5 H1)
+ ##| ##4: #H1; napply (or5_intro2 P1 P4 P3 P2 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P4 P3 P2 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_25 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P5 P3 P4 P2.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P5 P3 P4 P2 H1)
+ ##| ##2: #H1; napply (or5_intro5 P1 P5 P3 P4 P2 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P5 P3 P4 P2 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P5 P3 P4 P2 H1)
+ ##| ##5: #H1; napply (or5_intro2 P1 P5 P3 P4 P2 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_34 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P4 P3 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P4 P3 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P4 P3 P5 H1)
+ ##| ##3: #H1; napply (or5_intro4 P1 P2 P4 P3 P5 H1)
+ ##| ##4: #H1; napply (or5_intro3 P1 P2 P4 P3 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P2 P4 P3 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_35 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P5 P4 P3.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P5 P4 P3 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P5 P4 P3 H1)
+ ##| ##3: #H1; napply (or5_intro5 P1 P2 P5 P4 P3 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P2 P5 P4 P3 H1)
+ ##| ##5: #H1; napply (or5_intro3 P1 P2 P5 P4 P3 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_45 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P3 P5 P4.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P3 P5 P4 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P3 P5 P4 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P2 P3 P5 P4 H1)
+ ##| ##4: #H1; napply (or5_intro5 P1 P2 P3 P5 P4 H1)
+ ##| ##5: #H1; napply (or5_intro4 P1 P2 P3 P5 P4 H1)
+ ##]
+nqed.
+
ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
ex_intro: ∀x:A.Q x → ex A Q.
napply refl_eq.
nqed.
-nlemma eq_elim_r: ∀A:Type.∀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.
+nlemma symmetric_neq : ∀T.∀x,y:T.x ≠ y → y ≠ x.
+ #T; #x; #y;
+ nnormalize;
+ #H; #H1;
+ nrewrite > H1 in H:(%); #H;
+ napply (H (refl_eq …)).
+nqed.
+
ndefinition relationT : Type → Type → Type ≝
λA,T:Type.A → A → T.
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