From f848433620419e71cd19ec0b4f58c717ac50f85e Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 28 Feb 2012 08:23:11 +0000 Subject: [PATCH] commit by user andrea --- weblib/basics/logic.ma | 180 ++++++++++++++++++------------------ weblib/tutorial/chapter2.ma | 5 +- weblib/tutorial/chapter4.ma | 108 +++++++++++++--------- 3 files changed, 155 insertions(+), 138 deletions(-) diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma index 8f981d469..b9dfed28c 100644 --- a/weblib/basics/logic.ma +++ b/weblib/basics/logic.ma @@ -21,58 +21,58 @@ 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:eq ? x a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → P x p. + ∀A.∀a,x.∀p:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a.∀P: ∀x:A. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a → Type[3]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a 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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a → Prop. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) → ∀x.∀p:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a.P x p. + #A #a #P #p #x0 #p0; @(a href="cic:/matita/basics/logic/eq_rect_r.def(1)"eq_rect_r/a ? ? ? 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. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a → Type[0]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) → ∀x.∀p:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? 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. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a → Type[1]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) → ∀x.∀p:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? 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. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a → Type[2]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) → ∀x.∀p:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? 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. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a → Type[3]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) → ∀x.∀p:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? 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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y → y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x. +#A #x #y #Heq @(a href="cic:/matita/basics/logic/rewrite_l.def(1)"rewrite_l/a A x (λz.za title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax)) // 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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x → P y. +#A #x #P #Hx #y #Heq (cases (a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a ? ? ? Heq)); //; qed. -theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B. +theorem eq_coerc: ∀A,B:Type[0].A→(Aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aB)→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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y → y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a z → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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. xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay → f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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. x1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax2 → y1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay2 → f x1 y1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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. x1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax2 → y1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay2 → z1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/az2 → f x1 y1 z1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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 @@ -97,26 +97,26 @@ inductive False: Prop ≝ . λA. A → False. *) inductive Not (A:Prop): Prop ≝ -nmk: (A → False) → Not A. +nmk: (A → a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a) → 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 → a title="logical not" href="cic:/fakeuri.def(1)"¬/aA → a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. +#A #H #Hn (elim Hn); /span class="autotactic"2span class="autotrace" trace /span/span/; 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) → a title="logical not" href="cic:/fakeuri.def(1)"¬/aB →a title="logical not" href="cic:/fakeuri.def(1)"¬/aA. +/span class="autotactic"4span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a, a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/; 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 a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y → y a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a x. +/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a, a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/; qed. (* and *) inductive And (A,B:Prop) : Prop ≝ @@ -124,10 +124,10 @@ 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 a title="logical and" href="cic:/fakeuri.def(1)"∧/a B → A. #A #B #AB (elim AB) //; qed. -theorem proj2: ∀ A,B:Prop. A ∧ B → B. +theorem proj2: ∀ A,B:Prop. A a title="logical and" href="cic:/fakeuri.def(1)"∧/a B → B. #A #B #AB (elim AB) //; qed. (* or *) @@ -138,7 +138,7 @@ inductive Or (A,B:Prop) : Prop ≝ interpretation "logical or" 'or x y = (Or x y). definition decidable : Prop → Prop ≝ -λ A:Prop. A ∨ ¬ A. +λ A:Prop. A a title="logical or" href="cic:/fakeuri.def(1)"∨/a a title="logical not" href="cic:/fakeuri.def(1)"¬/a A. (* exists *) inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝ @@ -151,122 +151,122 @@ inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝ (* iff *) definition iff := - λ A,B. (A → B) ∧ (B → A). + λ A,B. (A → B) a title="logical and" href="cic:/fakeuri.def(1)"∧/a (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 a title="iff" href="cic:/fakeuri.def(1)"↔/a B → B a title="iff" href="cic:/fakeuri.def(1)"↔/a A. +#A #B * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ 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 a title="iff" href="cic:/fakeuri.def(1)"↔/a B → B a title="iff" href="cic:/fakeuri.def(1)"↔/a C → A a title="iff" href="cic:/fakeuri.def(1)"↔/a C. +#A #B #C * #H1 #H2 * #H3 #H4 % /span class="autotactic"3span class="autotrace" trace /span/span/ qed. -lemma iff_not: ∀A,B. A ↔ B → ¬A ↔ ¬B. -#A #B * #H1 #H2 % /3/ qed. +lemma iff_not: ∀A,B. A a title="iff" href="cic:/fakeuri.def(1)"↔/a B → a title="logical not" href="cic:/fakeuri.def(1)"¬/aA a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="logical not" href="cic:/fakeuri.def(1)"¬/aB. +#A #B * #H1 #H2 % /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/ 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 a title="iff" href="cic:/fakeuri.def(1)"↔/a B → C a title="logical and" href="cic:/fakeuri.def(1)"∧/a A a title="iff" href="cic:/fakeuri.def(1)"↔/a C a title="logical and" href="cic:/fakeuri.def(1)"∧/a B. +#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ 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 a title="iff" href="cic:/fakeuri.def(1)"↔/a B → A a title="logical and" href="cic:/fakeuri.def(1)"∧/a C a title="iff" href="cic:/fakeuri.def(1)"↔/a B a title="logical and" href="cic:/fakeuri.def(1)"∧/a C. +#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ 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 a title="iff" href="cic:/fakeuri.def(1)"↔/a B → C a title="logical or" href="cic:/fakeuri.def(1)"∨/a A a title="iff" href="cic:/fakeuri.def(1)"↔/a C a title="logical or" href="cic:/fakeuri.def(1)"∨/a B. +#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ 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 a title="iff" href="cic:/fakeuri.def(1)"↔/a B → A a title="logical or" href="cic:/fakeuri.def(1)"∨/a C a title="iff" href="cic:/fakeuri.def(1)"↔/a B a title="logical or" href="cic:/fakeuri.def(1)"∨/a C. +#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ qed. (* cose per destruct: da rivedere *) definition R0 ≝ λT:Type[0].λt:T.t. -definition R1 ≝ eq_rect_Type0. +definition R1 ≝ a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a. (* 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. a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0 → Type[0]. + ∀a1:T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0). + ∀T2:∀x0:T0. ∀p0:a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0. ∀x1:T1 x0 p0. a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? p0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x1 → Type[0]. + ∀a2:T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a1). ∀b0:T0. - ∀e0:a0 = b0. + ∀e0:a0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b0. ∀b1: T1 b0 e0. - ∀e1:R1 ?? T1 a1 ? e0 = b1. + ∀e1:a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? e0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b1. T2 b0 e0 b1 e1. #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1 -@(eq_rect_Type0 ????? e1) -@(R1 ?? ? ?? e0) +@(a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a ????? e1) +@(a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? ? ?? 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. a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0 → Type[0]. + ∀a1:T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0). + ∀T2:∀x0:T0. ∀p0:a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0. ∀x1:T1 x0 p0. a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? p0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x1 → Type[0]. + ∀a2:T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a1). + ∀T3:∀x0:T0. ∀p0:a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0. ∀x1:T1 x0 p0.∀p1:a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? p0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x1. + ∀x2:T2 x0 p0 x1 p1.a href="cic:/matita/basics/logic/R2.def(3)"R2/a ???? T2 a2 x0 p0 ? p1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x2 → Type[0]. + ∀a3:T3 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a1) a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a2). ∀b0:T0. - ∀e0:a0 = b0. + ∀e0:a0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b0. ∀b1: T1 b0 e0. - ∀e1:R1 ?? T1 a1 ? e0 = b1. + ∀e1:a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? e0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b1. ∀b2: T2 b0 e0 b1 e1. - ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2. + ∀e2:a href="cic:/matita/basics/logic/R2.def(3)"R2/a ???? T2 a2 b0 e0 ? e1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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) +@(a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a ????? e2) +@(a href="cic:/matita/basics/logic/R2.def(3)"R2/a ?? ? ???? 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. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a T0 a0 x0 → Type[0]. + ∀a1:T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0). + ∀T2:∀x0:T0. ∀p0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 …) a0 x0. ∀x1:T1 x0 p0.a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 …) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a T0 a0 T1 a1 x0 p0) x1 → Type[0]. + ∀a2:T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1). + ∀T3:∀x0:T0. ∀p0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 …) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a T0 a0 T1 a1 x0 p0) x1. + ∀x2:T2 x0 p0 x1 p1.a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T2 …) (a href="cic:/matita/basics/logic/R2.def(3)"R2/a T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0]. + ∀a3:T3 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1) + a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)) a2). + ∀T4:∀x0:T0. ∀p0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 …) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a T0 a0 T1 a1 x0 p0) x1. + ∀x2:T2 x0 p0 x1 p1.∀p2:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T2 …) (a href="cic:/matita/basics/logic/R2.def(3)"R2/a T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2. + ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T3 …) (a href="cic:/matita/basics/logic/R3.def(4)"R3/a 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 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1) + a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)) a2) + a3 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T3 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1) + a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)) a2)) a3). ∀b0:T0. - ∀e0:eq (T0 …) a0 b0. + ∀e0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 …) a0 b0. ∀b1: T1 b0 e0. - ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1. + ∀e1:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 …) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a 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:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T2 …) (a href="cic:/matita/basics/logic/R2.def(3)"R2/a 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:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T3 …) (a href="cic:/matita/basics/logic/R3.def(4)"R3/a 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) +@(a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a ????? e3) +@(a href="cic:/matita/basics/logic/R3.def(4)"R3/a ????????? e0 ? e1 ? e2) @a4 qed. -definition eqProp ≝ λA:Prop.eq A. +definition eqProp ≝ λA:Prop.a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a 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:xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax. a href="cic:/matita/basics/logic/eqProp.def(1)"eqProp/a ? h (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A x). +#A #x #h @(a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? h: a href="cic:/matita/basics/logic/eqProp.def(1)"eqProp/a ? ? ?). 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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a t → Type[3].P (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? t) → ∀p.P p. + #T #t #P #H #p >(a href="cic:/matita/basics/logic/lemmaK.def(2)"lemmaK/a T t p) @H +qed. \ No newline at end of file diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index 804ba58ba..ab758c124 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -217,7 +217,7 @@ lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)" |#a #Hind #q #r cut (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a), a href="cic:/matita/basics/types/snd.def(1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a)〉) [//] cases (a href="cic:/matita/basics/types/snd.def(1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a)) - [#H >(a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"div2S1/a … H) #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(Hind … H) + [#H >(a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"div2S1/a … H) #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a whd in ⊢ (???%); <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(Hind … H) |#H >(a href="cic:/matita/tutorial/chapter2/div2SO.def(3)"div2SO/a … H) #H1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @(Hind … H) ] qed. @@ -259,7 +259,8 @@ definition div2Pagain : ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0, |#a * #p #qrspec cut (p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p, a href="cic:/matita/basics/types/snd.def(1)"snd/a … p〉) [//] cases (a href="cic:/matita/basics/types/snd.def(1)"snd/a … p) - [#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉) whd #q #r #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(qrspec … H) + [#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉) whd #q #r #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a + whd in ⊢ (???%); <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(qrspec … H) |#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉) whd #q #r #H1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @(qrspec … H) ] qed. diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 8457aa484..1be877197 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -1,5 +1,5 @@ (* In this Chapter we shall develop a naif theory of sets represented as characteristic -predicates over some universe codeA/code, that is as objects of type A→Prop *) +predicates over some universe codeA/code, that is as objects of type A→Prop. *) include "basics/logic.ma". @@ -16,7 +16,9 @@ definition singleton ≝ λA.λx,a:A.xa title="leibnitz's equality" href="cic:/ (* 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 *) @@ -46,88 +48,102 @@ notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}. 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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 B → B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A. -#U #A #B #eqAB #a @iff_sym @eqAB qed. +#U #A #B #eqAB #a @a href="cic:/matita/basics/logic/iff_sym.def(2)"iff_sym/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 B → B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C. +#U #A #B #C #eqAB #eqBC #a @a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a // 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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="union" href="cic:/fakeuri.def(1)"∪/a B. +#U #A #B #C #eqAB #a @a href="cic:/matita/basics/logic/iff_or_r.def(2)"iff_or_r/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="union" href="cic:/fakeuri.def(1)"∪/a C. +#U #A #B #C #eqBC #a @a href="cic:/matita/basics/logic/iff_or_l.def(2)"iff_or_l/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="intersection" href="cic:/fakeuri.def(1)"∩/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="intersection" href="cic:/fakeuri.def(1)"∩/a B. +#U #A #B #C #eqAB #a @a href="cic:/matita/basics/logic/iff_and_r.def(2)"iff_and_r/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="intersection" href="cic:/fakeuri.def(1)"∩/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="intersection" href="cic:/fakeuri.def(1)"∩/a C. +#U #A #B #C #eqBC #a @a href="cic:/matita/basics/logic/iff_and_l.def(2)"iff_and_l/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="substraction" href="cic:/fakeuri.def(1)"-/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="substraction" href="cic:/fakeuri.def(1)"-/a B. +#U #A #B #C #eqAB #a @a href="cic:/matita/basics/logic/iff_and_r.def(2)"iff_and_r/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="substraction" href="cic:/fakeuri.def(1)"-/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="substraction" href="cic:/fakeuri.def(1)"-/a C. +#U #A #B #C #eqBC #a @a href="cic:/matita/basics/logic/iff_and_l.def(2)"iff_and_l/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/iff_not.def(4)"iff_not/a/span/span/ 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 a title="union" href="cic:/fakeuri.def(1)"∪/a a title="empty set" href="cic:/fakeuri.def(1)"∅/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A. +#U #A #w % [* // normalize #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace /span/span/ | /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/] qed. lemma union_comm : ∀U.∀A,B:U →Prop. - A ∪ B =1 B ∪ A. -#U #A #B #a % * /2/ qed. + A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 B a title="union" href="cic:/fakeuri.def(1)"∪/a A. +#U #A #B #a % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ 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 a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="union" href="cic:/fakeuri.def(1)"∪/a C a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="union" href="cic:/fakeuri.def(1)"∪/a (B a title="union" href="cic:/fakeuri.def(1)"∪/a C). +#S #A #B #C #w % [* [* /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/] | * [/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ | * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/] 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 a title="intersection" href="cic:/fakeuri.def(1)"∩/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 B a title="intersection" href="cic:/fakeuri.def(1)"∩/a A. +#U #A #B #a % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed. + +lemma cap_assoc: ∀U.∀A,B,C:U→Prop. + A a title="intersection" href="cic:/fakeuri.def(1)"∩/a (B a title="intersection" href="cic:/fakeuri.def(1)"∩/a C) a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 (A a title="intersection" href="cic:/fakeuri.def(1)"∩/a B) a title="intersection" href="cic:/fakeuri.def(1)"∩/a C. +#U #A #B #C #w % [ * #Aw * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ span class="autotactic"span class="autotrace"/span/span| * * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ ] +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 a title="union" href="cic:/fakeuri.def(1)"∪/a A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A. +#U #A #a % [* // | /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/] qed. lemma cap_idemp: ∀U.∀A:U →Prop. - A ∩ A =1 A. -#U #A #a % [* // | /2/] qed. + A a title="intersection" href="cic:/fakeuri.def(1)"∩/a A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A. +#U #A #a % [* // | /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/] 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 a title="union" href="cic:/fakeuri.def(1)"∪/a B) a title="intersection" href="cic:/fakeuri.def(1)"∩/a C a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 (A a title="intersection" href="cic:/fakeuri.def(1)"∩/a C) a title="union" href="cic:/fakeuri.def(1)"∪/a (B a title="intersection" href="cic:/fakeuri.def(1)"∩/a C). +#U #A #B #C #w % [* * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ | * * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/] 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 a title="union" href="cic:/fakeuri.def(1)"∪/a B) a title="substraction" href="cic:/fakeuri.def(1)"-/a C a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 (A a title="substraction" href="cic:/fakeuri.def(1)"-/a C) a title="union" href="cic:/fakeuri.def(1)"∪/a (B a title="substraction" href="cic:/fakeuri.def(1)"-/a C). +#U #A #B #C #w % [* * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ | * * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/] 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. Aa title="substraction" href="cic:/fakeuri.def(1)"-/aB a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="intersection" href="cic:/fakeuri.def(1)"∩/a a title="complement" href="cic:/fakeuri.def(1)"¬/aB. +#U #A #B #w normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed. -include "basics/types.ma". -include "basics/bool.ma". - (****** DeqSet: a set with a decidbale equality ******) record DeqSet : Type[1] ≝ { carr :> Type[0]; @@ -168,7 +184,7 @@ definition beqb ≝ λb1,b2. 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 /span class="autotactic"2span class="autotrace" trace conj/span/span/ qed. definition DeqBool ≝ mk_DeqSet bool beqb beqb_true. @@ -194,7 +210,7 @@ definition eq_pairs ≝ 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. -- 2.39.2