interpretation "leibniz reflexivity" 'refl = refl.
lemma eq_rect_r:
- ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl 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 = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
+ ∀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. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ ∀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. eq ? x a → Type[1]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ ∀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. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x 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. eq ? x a → Type[3]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ ∀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[2].∀x.∀P:A → Type[2]. P x → ∀y. x = 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 = y → y = x.
-#A #x #y #Heq @(rewrite_l A x (λz.z=x)) // 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.
-theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y.
-#A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
+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=B)→B.
+theorem eq_coerc: ∀A,B:Type[0].A→(A\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6B)→B.
#A #B #Ha #Heq (elim Heq); //; qed.
-theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
+theorem trans_eq : ∀A.∀x,y,z: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 z → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 z.
#A #x #y #z #H1 #H2 >H1; //; qed.
-theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y.
+theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y → f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y.
#A #B #f #x #y #H >H; //; qed.
(* deleterio per auto? *)
theorem eq_f2: ∀A,B,C.∀f:A→B→C.
-∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
+∀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=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = f x2 y2 z2.
+∀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
λA. A → False. *)
inductive Not (A:Prop): Prop ≝
-nmk: (A → False) → Not A.
+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 → ¬A → False.
-#A #H #Hn (elim Hn); /2/; qed.
+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); /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/; qed.
(*
ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
#A; #C; #H; #Hn; nelim (Hn H).
nqed. *)
-theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
-/4/; qed.
+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.
+/\ 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 ≠ y → y ≠ x.
-/3/; qed.
+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.
+/\ 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 ≝
interpretation "logical and" 'and x y = (And x y).
-theorem proj1: ∀A,B:Prop. A ∧ B → A.
+theorem proj1: ∀A,B:Prop. A \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 B → A.
#A #B #AB (elim AB) //; qed.
-theorem proj2: ∀ A,B:Prop. A ∧ B → B.
+theorem proj2: ∀ A,B:Prop. A \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 B → B.
#A #B #AB (elim AB) //; qed.
(* or *)
interpretation "logical or" 'or x y = (Or x y).
definition decidable : Prop → Prop ≝
-λ A:Prop. A ∨ ¬ A.
+λ A:Prop. A \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A.
(* exists *)
inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
(* iff *)
definition iff :=
- λ A,B. (A → B) ∧ (B → A).
+ λ 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).
-lemma iff_sym: ∀A,B. A ↔ B → B ↔ A.
-#A #B * /3/ qed.
+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 ↔ B → B ↔ C → A ↔ C.
-#A #B #C * #H1 #H2 * #H3 #H4 % /3/ 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 ↔ B → ¬A ↔ ¬B.
-#A #B * #H1 #H2 % /3/ 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 ↔ B → C ∧ A ↔ C ∧ B.
-#A #B #C * #H1 #H2 % * /3/ 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 ↔ B → A ∧ C ↔ B ∧ C.
-#A #B #C * #H1 #H2 % * /3/ 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 ↔ B → C ∨ A ↔ C ∨ B.
-#A #B #C * #H1 #H2 % * /3/ 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 ↔ B → A ∨ C ↔ B ∨ C.
-#A #B #C * #H1 #H2 % * /3/ 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 R0 ≝ λT:Type[0].λt:T.t.
-definition R1 ≝ eq_rect_Type0.
+definition R1 ≝ \ 5a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"\ 6eq_rect_Type0\ 5/a\ 6.
(* used for lambda-delta *)
definition R2 :
∀T0:Type[0].
∀a0:T0.
- ∀T1:∀x0:T0. a0=x0 → Type[0].
- ∀a1:T1 a0 (refl ? a0).
- ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
- ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
+ ∀T1:∀x0:T0. a0\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x0 → Type[0].
+ ∀a1:T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a0).
+ ∀T2:∀x0:T0. ∀p0:a0\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x0. ∀x1:T1 x0 p0. \ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? T1 a1 ? p0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x1 → Type[0].
+ ∀a2:T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a1).
∀b0:T0.
- ∀e0:a0 = b0.
+ ∀e0:a0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b0.
∀b1: T1 b0 e0.
- ∀e1:R1 ?? T1 a1 ? e0 = b1.
+ ∀e1:\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? T1 a1 ? e0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b1.
T2 b0 e0 b1 e1.
#T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
-@(eq_rect_Type0 ????? e1)
-@(R1 ?? ? ?? e0)
+@(\ 5a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"\ 6eq_rect_Type0\ 5/a\ 6 ????? e1)
+@(\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? ? ?? e0)
@a2
qed.
definition R3 :
∀T0:Type[0].
∀a0:T0.
- ∀T1:∀x0:T0. a0=x0 → Type[0].
- ∀a1:T1 a0 (refl ? a0).
- ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
- ∀a2:T2 a0 (refl ? a0) a1 (refl ? 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 ? a0) a1 (refl ? a1) a2 (refl ? a2).
+ ∀T1:∀x0:T0. a0\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x0 → Type[0].
+ ∀a1:T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a0).
+ ∀T2:∀x0:T0. ∀p0:a0\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x0. ∀x1:T1 x0 p0. \ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? T1 a1 ? p0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x1 → Type[0].
+ ∀a2:T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a1).
+ ∀T3:∀x0:T0. ∀p0:a0\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x0. ∀x1:T1 x0 p0.∀p1:\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? T1 a1 ? p0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x1.
+ ∀x2:T2 x0 p0 x1 p1.\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 ???? T2 a2 x0 p0 ? p1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x2 → Type[0].
+ ∀a3:T3 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a1) a2 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a2).
∀b0:T0.
- ∀e0:a0 = b0.
+ ∀e0:a0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b0.
∀b1: T1 b0 e0.
- ∀e1:R1 ?? T1 a1 ? e0 = b1.
+ ∀e1:\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? T1 a1 ? e0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b1.
∀b2: T2 b0 e0 b1 e1.
- ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
+ ∀e2:\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 ???? T2 a2 b0 e0 ? e1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b2.
T3 b0 e0 b1 e1 b2 e2.
#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
-@(eq_rect_Type0 ????? e2)
-@(R2 ?? ? ???? e0 ? e1)
+@(\ 5a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"\ 6eq_rect_Type0\ 5/a\ 6 ????? e2)
+@(\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 ?? ? ???? e0 ? e1)
@a3
qed.
definition R4 :
∀T0:Type[0].
∀a0:T0.
- ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
- ∀a1:T1 a0 (refl 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 T0 a0) a1 (refl (T1 a0 (refl 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 T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
- a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl 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.
+ ∀T1:∀x0:T0. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 T0 a0 x0 → Type[0].
+ ∀a1:T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0).
+ ∀T2:∀x0:T0. ∀p0:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T0 …) a0 x0. ∀x1:T1 x0 p0.\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T1 …) (\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+ ∀a2:T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1).
+ ∀T3:∀x0:T0. ∀p0:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T1 …) (\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T2 …) (\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+ ∀a3:T3 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1)
+ a2 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1)) a2).
+ ∀T4:∀x0:T0. ∀p0:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T1 …) (\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.∀p2:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T2 …) (\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+ ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T3 …) (\ 5a href="cic:/matita/basics/logic/R3.def(4)"\ 6R3\ 5/a\ 6 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
Type[0].
- ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
- a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
- a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
- a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
+ ∀a4:T4 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1)
+ a2 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1)) a2)
+ a3 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T3 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1)
+ a2 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1)) a2))
a3).
∀b0:T0.
- ∀e0:eq (T0 …) a0 b0.
+ ∀e0:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T0 …) a0 b0.
∀b1: T1 b0 e0.
- ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
+ ∀e1:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T1 …) (\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 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.
+ ∀e2:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T2 …) (\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 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.
+ ∀e3:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T3 …) (\ 5a href="cic:/matita/basics/logic/R3.def(4)"\ 6R3\ 5/a\ 6 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
-@(eq_rect_Type0 ????? e3)
-@(R3 ????????? e0 ? e1 ? e2)
+@(\ 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)
@a4
qed.
-definition eqProp ≝ λA:Prop.eq A.
+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=x. eqProp ? h (refl A x).
-#A #x #h @(refl ? h: eqProp ? ? ?).
+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 = t → Type[3].P (refl ? t) → ∀p.P p.
- #T #t #P #H #p >(lemmaK T t p) @H
-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.
\ No newline at end of file
(* In this Chapter we shall develop a naif theory of sets represented as characteristic
-predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type A→Prop *)
+predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type A→Prop. *)
include "basics/logic.ma".
(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
interpretation "singleton" 'singl x = (singleton ? x).
-(* The operations of union, intersection, complement and substraction
+(* The membership relation between an element of type A and a set S:A →Prop is
+simply the predicate resulting from the application of S to a.
+The operations of union, intersection, complement and substraction
are easily defined in terms of the propositional connectives of dijunction,
conjunction and negation *)
interpretation "extensional equality" 'eqP a b = (eqP ? a b).
(* This notion of equality is different from the intensional equality of
-fucntions, hence we have to prove the usual properties: *)
+functions; the fact it defines an equivalence relation must be explicitly
+proved: *)
lemma eqP_sym: ∀U.∀A,B:U →Prop.
A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B → B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
-#U #A #B #eqAB #a @iff_sym @eqAB qed.
+#U #A #B #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @eqAB qed.
lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
- A =1 B → B =1 C → A =1 C.
-#U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
+ A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B → B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C.
+#U #A #B #C #eqAB #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 // qed.
-(* For the same reason, we must also prove that all the operations we have
- lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
- A =1 C → A ∪ B =1 C ∪ B.
-#U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
+(* For the same reason, we must also prove that all the operations behave well
+with respect to eqP: *)
+
+lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
+ A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B.
+#U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_or_r.def(2)"\ 6iff_or_r\ 5/a\ 6 @eqAB qed.
lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
- B =1 C → A ∪ B =1 A ∪ C.
-#U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
+ B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 C.
+#U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_or_l.def(2)"\ 6iff_or_l\ 5/a\ 6 @eqBC qed.
lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
- A =1 C → A ∩ B =1 C ∩ B.
-#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+ A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 B.
+#U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_and_r.def(2)"\ 6iff_and_r\ 5/a\ 6 @eqAB qed.
lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
- B =1 C → A ∩ B =1 A ∩ C.
-#U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
+ B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C.
+#U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_and_l.def(2)"\ 6iff_and_l\ 5/a\ 6 @eqBC qed.
lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
- A =1 C → A - B =1 C - B.
-#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+ A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B.
+#U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_and_r.def(2)"\ 6iff_and_r\ 5/a\ 6 @eqAB qed.
lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
- B =1 C → A - B =1 A - C.
-#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
+ B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C.
+#U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_and_l.def(2)"\ 6iff_and_l\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/iff_not.def(4)"\ 6iff_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+(* We can now prove several properties of the previous set-theoretic
+operations. In particular, union is commutative and associative, and
+the empty set is an identity element: *)
-(* set equalities *)
lemma union_empty_r: ∀U.∀A:U→Prop.
- A ∪ ∅ =1 A.
-#U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
+ A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
+#U #A #w % [* // normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
qed.
lemma union_comm : ∀U.∀A,B:U →Prop.
- A ∪ B =1 B ∪ A.
-#U #A #B #a % * /2/ qed.
+ A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 A.
+#U #A #B #a % * /\ 5span class="autotactic"\ 62\ 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 union_assoc: ∀U.∀A,B,C:U → Prop.
- A ∪ B ∪ C =1 A ∪ (B ∪ C).
-#S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
+ A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 C).
+#S #A #B #C #w % [* [* /\ 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/ | /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] | * [/\ 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\ 5/span\ 6\ 5/span\ 6/ | * /\ 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.
+(* In the same way we prove commutativity and associativity for set
+interesection *)
+
lemma cap_comm : ∀U.∀A,B:U →Prop.
- A ∩ B =1 B ∩ A.
-#U #A #B #a % * /2/ qed.
+ A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 A.
+#U #A #B #a % * /\ 5span class="autotactic"\ 62\ 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 cap_assoc: ∀U.∀A,B,C:U→Prop.
+ A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 (B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C) \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 B) \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C.
+#U #A #B #C #w % [ * #Aw * /\ 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/ \ 5span class="autotactic"\ 6\ 5span class="autotrace"\ 6\ 5/span\ 6\ 5/span\ 6| * * /\ 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.
+
+(* We can also easily prove idempotency for union and intersection *)
lemma union_idemp: ∀U.∀A:U →Prop.
- A ∪ A =1 A.
-#U #A #a % [* // | /2/] qed.
+ A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
+#U #A #a % [* // | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] qed.
lemma cap_idemp: ∀U.∀A:U →Prop.
- A ∩ A =1 A.
-#U #A #a % [* // | /2/] qed.
+ A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
+#U #A #a % [* // | /\ 5span class="autotactic"\ 62\ 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.
-(*distributivities *)
+(* We conclude our examples with a couple of distributivity theorems,
+and a characterization of substraction in terms of interesection and
+complementation. *)
lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
- (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
-#U #A #B #C #w % [* * /3/ | * * /3/]
+ (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B) \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C).
+#U #A #B #C #w % [* * /\ 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, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * * /\ 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, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
qed.
lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
- (A ∪ B) - C =1 (A - C) ∪ (B - C).
-#U #A #B #C #w % [* * /3/ | * * /3/]
+ (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B) \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (B \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C).
+#U #A #B #C #w % [* * /\ 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, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * * /\ 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, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
qed.
-(* substraction *)
-lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
-#U #A #B #w normalize /2/
+lemma substract_def:∀U.∀A,B:U→Prop. A\ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 \ 5a title="complement" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6B.
+#U #A #B #w normalize /\ 5span class="autotactic"\ 62\ 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.
-include "basics/types.ma".
-include "basics/bool.ma".
-
(****** DeqSet: a set with a decidbale equality ******)
record DeqSet : Type[1] ≝ { carr :> Type[0];
notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
-#b1 #b2 cases b1 cases b2 normalize /2/
+#b1 #b2 cases b1 cases b2 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace conj\ 5/span\ 6\ 5/span\ 6/
qed.
definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
eq_pairs A B p1 p2 = true ↔ p1 = p2.
#A #B * #a1 #b1 * #a2 #b2 %
- [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
+ [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
|#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
]
qed.
projects / helm.git / commitdiff