From 06c9a9279fa23a314bb74f4fa9ce7163038301f7 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 28 Feb 2012 09:29:28 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter4.ma | 100 ++++++++++++++++++++++++++---------- 1 file changed, 74 insertions(+), 26 deletions(-) diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 1be877197..d2dc7c843 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -1,7 +1,8 @@ (* 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. *) -include "basics/logic.ma". +include "basics/types.ma". +include "basics/bool.ma". (**** For instance the empty set is defined by the always function predicate *) @@ -86,9 +87,9 @@ lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop. 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: *) +(* 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: *) lemma union_empty_r: ∀U.∀A:U→Prop. 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. @@ -104,7 +105,7 @@ lemma union_assoc: ∀U.∀A,B,C:U → Prop. #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 +(* In the same way we prove commutativity and associativity for set interesection *) lemma cap_comm : ∀U.∀A,B:U →Prop. @@ -126,9 +127,8 @@ lemma cap_idemp: ∀U.∀A:U →Prop. 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. -(* We conclude our examples with a couple of distributivity theorems, -and a characterization of substraction in terms of interesection and -complementation. *) +(* 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 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). @@ -144,60 +144,108 @@ lemma substract_def:∀U.∀A,B:U→Prop. Aa title="substraction" href="cic:/fa #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. -(****** DeqSet: a set with a decidbale equality ******) +(* In several situation it is important to assume to have a decidable equality +between elements of a set U, namely a boolean function eqb: U→U→bool such that +for any pair of elements a and b in U, (eqb x y) is true if and only if x=y. +A set equipped with such an equality is called a DeqSet: *) record DeqSet : Type[1] ≝ { carr :> Type[0]; - eqb: carr → carr → bool; - eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y) + eqb: carr → carr → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a; + eqb_true: ∀x,y. (eqb x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) a title="iff" href="cic:/fakeuri.def(1)"↔/a (x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y) }. +(* We use the notation == to denote the decidable equality, to distinguish it +from the propositional equality. In particular, a term of the form a==b is a +boolean, while a=b is a proposition. *) + notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }. interpretation "eqb" 'eqb a b = (eqb ? a b). +(* It is convenient to have a simple way to reflect a proof of the fact +that (eqb a b) is true into a proof of the proposition (a = b); to this aim, +we introduce two operators "\P" and "\b". *) + notation "\P H" non associative with precedence 90 for @{(proj1 … (eqb_true ???) $H)}. notation "\b H" non associative with precedence 90 for @{(proj2 … (eqb_true ???) $H)}. -lemma eqb_false: ∀S:DeqSet.∀a,b:S. - (eqb ? a b) = false ↔ a ≠ b. +(* If H:eqb a b = true, then \P H: a = b, and conversely if h:a = b, then +\b h: eqb a b = true. Let us see an example of their use: the following +statement asserts that we can reflect a proof that eqb a b is false into +a proof of the proposition a ≠ b. *) + +lemma eqb_false: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a,b:S. + (a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"eqb/a ? a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="iff" href="cic:/fakeuri.def(1)"↔/a a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a b. + +(* We start the proof introducing the hypothesis, and then split the "if" and +"only if" cases *) + #S #a #b % #H - [@(not_to_not … not_eq_true_false) #H1