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 *)
(* 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.
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.
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.
(* 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.
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) //
]
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
(* ---------------------------------------- *) ⊢
\ 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