From bcdba61431ead40a18a6ac04285cd6513d491287 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 10 Jul 2012 14:33:06 +0000 Subject: [PATCH] commit by user mkmluser --- weblib/cicm2012/part2.ma | 24 ++++++++++++------------ weblib/commit_test2.ma | 6 +++++- 2 files changed, 17 insertions(+), 13 deletions(-) diff --git a/weblib/cicm2012/part2.ma b/weblib/cicm2012/part2.ma index ad8f06a4f..9abb511cf 100644 --- a/weblib/cicm2012/part2.ma +++ b/weblib/cicm2012/part2.ma @@ -185,7 +185,7 @@ notation "\b H" non associative with precedence 90 statement asserts that we can reflect a proof that eqb a b is false into a proof of the proposition a ≠ b. *) -img class="anchor" src="icons/tick.png" id="eqb_false"lemma eqb_false: ∀S:a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"DeqSet/a.∀a,b:S. +lemma eqb_false: ∀S:a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"DeqSet/a.∀a,b:S. (a href="cic:/matita/cicm2012/part2/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. #S #a #b % (* same tactic on two goals *) @@ -208,7 +208,7 @@ notation "\bf H" non associative with precedence 90 (* The following statement proves that propositional equality in a DeqSet is decidable in the traditional sense, namely either a=b or a≠b *) - img class="anchor" src="icons/tick.png" id="dec_eq"lemma dec_eq: ∀S:a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"DeqSet/a.∀a,b:S. a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b a title="logical or" href="cic:/fakeuri.def(1)"∨/a a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a b. + lemma dec_eq: ∀S:a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"DeqSet/a.∀a,b:S. a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b a title="logical or" href="cic:/fakeuri.def(1)"∨/a a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a b. #S #a #b cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/cicm2012/part2/eqb.fix(0,0,3)"eqb/a ? a b)) #H [%1 @(\P H) | %2 @(\Pf H)] qed. @@ -220,15 +220,15 @@ the boolean equality beqb, then prove that beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by instantiating the DeqSet record with the previous information *) -img class="anchor" src="icons/tick.png" id="beqb"definition beqb ≝ λb1,b2. +definition beqb ≝ λb1,b2. match b1 with [ true ⇒ b2 | false ⇒ a href="cic:/matita/basics/bool/notb.def(1)"notb/a b2]. notation < "a == b" non associative with precedence 45 for @{beqb $a $b }. -img class="anchor" src="icons/tick.png" id="beqb_true"lemma beqb_true: ∀b1,b2. a href="cic:/matita/cicm2012/part2/beqb.def(2)"beqb/a b1 b2 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 b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b2. +lemma beqb_true: ∀b1,b2. a href="cic:/matita/cicm2012/part2/beqb.def(2)"beqb/a b1 b2 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 b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b2. #b1 #b2 cases b1 cases b2 normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed. -img class="anchor" src="icons/tick.png" id="DeqBool"definition DeqBool ≝ a href="cic:/matita/cicm2012/part2/DeqSet.con(0,1,0)"mk_DeqSet/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/cicm2012/part2/beqb.def(2)"beqb/a a href="cic:/matita/cicm2012/part2/beqb_true.def(4)"beqb_true/a. +definition DeqBool ≝ a href="cic:/matita/cicm2012/part2/DeqSet.con(0,1,0)"mk_DeqSet/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/cicm2012/part2/beqb.def(2)"beqb/a a href="cic:/matita/cicm2012/part2/beqb_true.def(4)"beqb_true/a. (* At this point, we would expect to be able to prove things like the following: for any boolean b, if b==false is true then b=false. @@ -236,7 +236,7 @@ Unfortunately, this would not work, unless we declare b of type DeqBool (change the type in the following statement and see what happens). *) -img class="anchor" src="icons/tick.png" id="exhint"example exhint: ∀b:a href="cic:/matita/cicm2012/part2/DeqBool.def(5)"DeqBool/a. (b=a title="eqb" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → ba title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. +example exhint: ∀b:a href="cic:/matita/cicm2012/part2/DeqBool.def(5)"DeqBool/a. (b=a title="eqb" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → ba title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. #b #H @(\P H) qed. @@ -269,7 +269,7 @@ unification hint 0 a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"≔/a (* After having provided the previous hints, we may rewrite example exhint declaring b of type bool. *) -img class="anchor" src="icons/tick.png" id="exhint1"example exhint1: ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. (b =a title="eqb" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/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. +example exhint1: ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. (b =a title="eqb" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/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. #b #H @(\P H) qed. @@ -277,10 +277,10 @@ qed. this, we must as usual define the boolen equality function, and prove it correctly reflects propositional equality. *) -img class="anchor" src="icons/tick.png" id="eq_pairs"definition eq_pairs ≝ +definition eq_pairs ≝ λA,B:a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"DeqSet/a.λp1,p2:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB.(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p1 =a title="eqb" href="cic:/fakeuri.def(1)"=/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p2) a title="boolean and" href="cic:/fakeuri.def(1)"∧/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p1 =a title="eqb" href="cic:/fakeuri.def(1)"=/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p2). -img class="anchor" src="icons/tick.png" id="eq_pairs_true"lemma eq_pairs_true: ∀A,B:a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"DeqSet/a.∀p1,p2:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB. +lemma eq_pairs_true: ∀A,B:a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"DeqSet/a.∀p1,p2:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB. a href="cic:/matita/cicm2012/part2/eq_pairs.def(4)"eq_pairs/a A B p1 p2 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 p1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a p2. #A #B * #a1 #b1 * #a2 #b2 % [#H cases (a href="cic:/matita/basics/bool/andb_true.def(5)"andb_true/a …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) // @@ -288,7 +288,7 @@ it correctly reflects propositional equality. *) ] qed. -img class="anchor" src="icons/tick.png" id="DeqProd"definition DeqProd ≝ λA,B:a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"DeqSet/a. +definition DeqProd ≝ λA,B:a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"DeqSet/a. a href="cic:/matita/cicm2012/part2/DeqSet.con(0,1,0)"mk_DeqSet/a (Aa title="Product" href="cic:/fakeuri.def(1)"×/aB) (a href="cic:/matita/cicm2012/part2/eq_pairs.def(4)"eq_pairs/a A B) (a href="cic:/matita/cicm2012/part2/eq_pairs_true.def(6)"eq_pairs_true/a A B). (* Having a unification problem of the kind T1×T2 = carr X, what kind @@ -308,7 +308,7 @@ unification hint 0 a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"≔/a (* ---------------------------------------- *) ⊢ a href="cic:/matita/cicm2012/part2/eq_pairs.def(4)"eq_pairs/a T1 T2 p1 p2 ≡ a href="cic:/matita/cicm2012/part2/eqb.fix(0,0,3)"eqb/a X p1 p2. -img class="anchor" src="icons/tick.png" id="hint2"example hint2: ∀b1,b2. +example hint2: ∀b1,b2. 〈b1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a=a title="eqb" href="cic:/fakeuri.def(1)"=/a〈a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,b2a title="Pair construction" href="cic:/fakeuri.def(1)"〉/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 〈b1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a〈a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,b2a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. #b1 #b2 #H @(\P H) -qed. +qed. \ No newline at end of file diff --git a/weblib/commit_test2.ma b/weblib/commit_test2.ma index 51bd8abb1..786ee682f 100644 --- a/weblib/commit_test2.ma +++ b/weblib/commit_test2.ma @@ -1,3 +1,7 @@ -(* test2 *) +(* test2 + +foo + + *) axiom pluto : Prop. \ No newline at end of file -- 2.39.2