From: matitaweb Date: Wed, 7 Mar 2012 11:47:26 +0000 (+0000) Subject: more sections X-Git-Tag: make_still_working~1878 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d2da1674173236ccb7902490d283741e6de0dd3a more sections --- diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index b56caaa66..20762a99a 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -147,7 +147,9 @@ 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. -(* In several situation it is important to assume to have a decidable equality +(* +h2 class="section"Bool vs. Prop/h2 +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: *) @@ -164,7 +166,9 @@ 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 +(* +h2 class="section"Small Scale Reflection/h2 +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". *) @@ -237,7 +241,9 @@ qed. definition DeqBool ≝ a href="cic:/matita/tutorial/chapter4/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/tutorial/chapter4/beqb.def(2)"beqb/a a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"beqb_true/a. -(* At this point, we would expect to be able to prove things like the +(* +h2 class="section"Unification Hints/h2 +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. Unfortunately, this would not work, unless we declare b of type DeqBool (change the type in the following statement and see what