-(*
+ (*
||M|| This file is part of HELM, an Hypertextual, Electronic
||A|| Library of Mathematics, developed at the Computer Science
||T|| Department of the University of Bologna, Italy.
V_______________________________________________________________ *)
include "basics/pts.ma".
-(*include "hints_declaration.ma".*)
+include "hints_declaration.ma".
(* propositional equality *)
-inductive eq (A:Type[1]) (x:A) : A → Prop ≝
+inductive eq (A:Type[2]) (x:A) : A → Prop ≝
refl: eq A x x.
-
+
interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+interpretation "leibniz reflexivity" 'refl = refl.
lemma eq_rect_r:
- ∀A.∀a,x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.∀P:
- ∀x:A. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a → Type[2]. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) → P x p.
+ ∀A.∀a,x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.∀P: ∀x:A. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a → Type[3]. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) → P x p.
#A #a #x #p (cases p) // qed.
lemma eq_ind_r :
- ∀A.∀a.∀P: ∀x:A. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a → Prop. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) →
- ∀x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.P x p.
+ ∀A.∀a.∀P: ∀x:A. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a → Prop. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) → ∀x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.P x p.
#A #a #P #p #x0 #p0; @(\ 5a href="cic:/matita/basics/logic/eq_rect_r.def(1)"\ 6eq_rect_r\ 5/a\ 6 ? ? ? p0) //; qed.
+lemma eq_rect_Type0_r:
+ ∀A.∀a.∀P: ∀x:A. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a → Type[0]. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) → ∀x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
+ cases p; //; qed.
+
+lemma eq_rect_Type1_r:
+ ∀A.∀a.∀P: ∀x:A. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a → Type[1]. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) → ∀x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
+ cases p; //; qed.
+
lemma eq_rect_Type2_r:
- ∀A.∀a.∀P: ∀x:A. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a → Type[2]. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) →
- ∀x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.P x p.
- #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+ ∀A.∀a.∀P: ∀x:A. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a → Type[2]. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) → ∀x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
+ cases p; //; qed.
+
+lemma eq_rect_Type3_r:
+ ∀A.∀a.∀P: ∀x:A. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a → Type[3]. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) → ∀x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
cases p; //; qed.
-theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y → P y.
+theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y → P y.
#A #x #P #Hx #y #Heq (cases Heq); //; qed.
theorem sym_eq: ∀A.∀x,y:A. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y → y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.
-#A #x #y #Heq @(\ 5a href="cic:/matita/basics/logic/rewrite_l.def(1)"\ 6rewrite_l\ 5/a\ 6 A x (λz.z\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x)); //; qed.
+#A #x #y #Heq @(\ 5a href="cic:/matita/basics/logic/rewrite_l.def(1)"\ 6rewrite_l\ 5/a\ 6 A x (λz.z\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x)) // qed.
-theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x → P y.
+theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x → P y.
#A #x #P #Hx #y #Heq (cases (\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 ? ? ? Heq)); //; qed.
theorem eq_coerc: ∀A,B:Type[0].A→(A\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6B)→B.
∀x1,x2:A.∀y1,y2:B. x1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x2 → y1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y2 → f x1 y1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x2 y2.
#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed.
+lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
+∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x2 → y1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y2 → z1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6z2 → f x1 y1 z1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x2 y2 z2.
+#A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
+
(* hint to genereric equality
definition eq_equality: equality ≝
mk_equality eq refl rewrite_l rewrite_r.
inductive Not (A:Prop): Prop ≝
nmk: (A → \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6) → Not A.
-
interpretation "logical not" 'not x = (Not x).
theorem absurd : ∀A:Prop. A → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6A → \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
-#A #H #Hn (elim Hn); /2/; qed.
+#A #H #Hn (elim Hn); /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/; qed.
(*
ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
nqed. *)
theorem not_to_not : ∀A,B:Prop. (A → B) → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6B →\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6A.
-/4/; qed.
+/\ 5span class="autotactic"\ 64\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/; qed.
(* inequality *)
interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
theorem sym_not_eq: ∀A.∀x,y:A. x \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 y → y \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 x.
-/3/; qed.
+/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/; qed.
(* and *)
inductive And (A,B:Prop) : Prop ≝
definition iff :=
λ A,B. (A → B) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 (B → A).
-interpretation "iff" 'iff a b = (iff a b).
+interpretation "iff" 'iff a b = (iff a b).
+
+lemma iff_sym: ∀A,B. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → B \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 A.
+#A #B * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+lemma iff_trans:∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → B \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C → A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C.
+#A #B #C * #H1 #H2 * #H3 #H4 % /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ qed.
+
+lemma iff_not: ∀A,B. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6B.
+#A #B * #H1 #H2 % /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+lemma iff_and_l: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → C \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 B.
+#A #B #C * #H1 #H2 % * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+lemma iff_and_r: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → A \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 C \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 C.
+#A #B #C * #H1 #H2 % * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+lemma iff_or_l: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → C \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 B.
+#A #B #C * #H1 #H2 % * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+lemma iff_or_r: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → A \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 C \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 C.
+#A #B #C * #H1 #H2 % * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
(* cose per destruct: da rivedere *)
definition R1 ≝ \ 5a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"\ 6eq_rect_Type0\ 5/a\ 6.
-(* useless stuff *)
+(* used for lambda-delta *)
definition R2 :
∀T0:Type[0].
∀a0:T0.
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
@(\ 5a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"\ 6eq_rect_Type0\ 5/a\ 6 ????? e3)
-@(\ 5a href="cic:/matita/basics/logic/R3.def(4)"\ 6R3\ 5/a\ 6 ????????? e0 ? e1 ? e2)
+@(\ 5a href="cic:/matita/basics/logic/R3.def(4)"\ 6R3\ 5/a\ 6 ????????? e0 ? e1 ? e2)
@a4
qed.
-(* TODO concrete definition by means of proof irrelevance *)
-axiom streicherK : ∀T:Type[1].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[2].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
+definition eqProp ≝ λA:Prop.\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 A.
+(* Example to avoid indexing and the consequential creation of ill typed
+ terms during paramodulation *)
+example lemmaK : ∀A.∀x:A.∀h:x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x. \ 5a href="cic:/matita/basics/logic/eqProp.def(1)"\ 6eqProp\ 5/a\ 6 ? h (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A x).
+#A #x #h @(\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? h: \ 5a href="cic:/matita/basics/logic/eqProp.def(1)"\ 6eqProp\ 5/a\ 6 ? ? ?).
+qed.
+
+theorem streicherK : ∀T:Type[2].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[3].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
+ #T #t #P #H #p >(\ 5a href="cic:/matita/basics/logic/lemmaK.def(2)"\ 6lemmaK\ 5/a\ 6 T t p) @H
+qed.
projects / helm.git / blobdiff