commit by user mkmluser

diff --git a/weblib/cicm2012/part2.ma b/weblib/cicm2012/part2.ma
index ad8f06a4f41ac499b22fe6c7beb807823e51eb49..9abb511cf940765fc63a6a52aba111b05ab94674 100644 (file)
--- 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. *)
 
-\ 5img class="anchor" src="icons/tick.png" id="eqb_false"\ 6lemma eqb_false: ∀S:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a,b:S. 
+lemma eqb_false: ∀S:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a,b:S. 
   (\ 5a href="cic:/matita/cicm2012/part2/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 ? a b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 a \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 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 *)
 
- \ 5img class="anchor" src="icons/tick.png" id="dec_eq"\ 6lemma dec_eq: ∀S:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a,b:S. a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 a \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 b.
+ lemma dec_eq: ∀S:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a,b:S. a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 a \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 b.
 #S #a #b cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/cicm2012/part2/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 ? 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 *)
 
-\ 5img class="anchor" src="icons/tick.png" id="beqb"\ 6definition beqb ≝ λb1,b2.
+definition beqb ≝ λb1,b2.
   match b1 with [ true ⇒ b2 | false ⇒ \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b2].
 
 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
-\ 5img class="anchor" src="icons/tick.png" id="beqb_true"\ 6lemma beqb_true: ∀b1,b2. \ 5a href="cic:/matita/cicm2012/part2/beqb.def(2)"\ 6beqb\ 5/a\ 6 b1 b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b2.
+lemma beqb_true: ∀b1,b2. \ 5a href="cic:/matita/cicm2012/part2/beqb.def(2)"\ 6beqb\ 5/a\ 6 b1 b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b2.
 #b1 #b2 cases b1 cases b2 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. 
 
-\ 5img class="anchor" src="icons/tick.png" id="DeqBool"\ 6definition DeqBool ≝ \ 5a href="cic:/matita/cicm2012/part2/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/cicm2012/part2/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/cicm2012/part2/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6.
+definition DeqBool ≝ \ 5a href="cic:/matita/cicm2012/part2/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/cicm2012/part2/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/cicm2012/part2/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6.
 
 (* 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). *)
 
-\ 5img class="anchor" src="icons/tick.png" id="exhint"\ 6example exhint: ∀b:\ 5a href="cic:/matita/cicm2012/part2/DeqBool.def(5)"\ 6DeqBool\ 5/a\ 6. (b=\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+example exhint: ∀b:\ 5a href="cic:/matita/cicm2012/part2/DeqBool.def(5)"\ 6DeqBool\ 5/a\ 6. (b=\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
 #b #H @(\P H) 
 qed.
 
@@ -269,7 +269,7 @@ unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6≔\ 5/a
 (* After having provided the previous hints, we may rewrite example exhint 
 declaring b of type bool. *)
  
-\ 5img class="anchor" src="icons/tick.png" id="exhint1"\ 6example exhint1: ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. (b =\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6. 
+example exhint1: ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. (b =\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6. 
 #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. *)
 
-\ 5img class="anchor" src="icons/tick.png" id="eq_pairs"\ 6definition eq_pairs ≝
+definition eq_pairs ≝
   λA,B:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λp1,p2:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B.(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p1 =\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p2) \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p1 =\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p2).
 
-\ 5img class="anchor" src="icons/tick.png" id="eq_pairs_true"\ 6lemma eq_pairs_true: ∀A,B:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀p1,p2:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B.
+lemma eq_pairs_true: ∀A,B:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀p1,p2:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B.
   \ 5a href="cic:/matita/cicm2012/part2/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 A B p1 p2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 p1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 p2.
 #A #B * #a1 #b1 * #a2 #b2 %
   [#H cases (\ 5a href="cic:/matita/basics/bool/andb_true.def(5)"\ 6andb_true\ 5/a\ 6 …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
@@ -288,7 +288,7 @@ it correctly reflects propositional equality. *)
   ]
 qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="DeqProd"\ 6definition DeqProd ≝ λA,B:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.
+definition DeqProd ≝ λA,B:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.
   \ 5a href="cic:/matita/cicm2012/part2/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 (A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B) (\ 5a href="cic:/matita/cicm2012/part2/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 A B) (\ 5a href="cic:/matita/cicm2012/part2/eq_pairs_true.def(6)"\ 6eq_pairs_true\ 5/a\ 6 A B).
 
 (* Having a unification problem of the kind T1×T2 = carr X, what kind 
@@ -308,7 +308,7 @@ unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6≔\ 5/a
 (* ---------------------------------------- *) ⊢ 
     \ 5a href="cic:/matita/cicm2012/part2/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 T1 T2 p1 p2 ≡ \ 5a href="cic:/matita/cicm2012/part2/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X p1 p2.
 
-\ 5img class="anchor" src="icons/tick.png" id="hint2"\ 6example hint2: ∀b1,b2. 
+example hint2: ∀b1,b2. 
   〈b1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6=\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6〈\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,b2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 〈b1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6〈\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,b2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6.
 #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 51bd8abb100ee5d9daab7a1646573ae7882d6b32..786ee682f050486daa901aadf7922f009402c0de 100644 (file)
--- 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