From: Enrico Tassi Date: Tue, 11 Nov 2008 19:33:11 +0000 (+0000) Subject: last fixes X-Git-Tag: make_still_working~4573 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f9480e116110345956ef873c88dba78f73fa225b;p=helm.git last fixes --- diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma index cb42e8198..f708c19ba 100644 --- a/helm/software/matita/contribs/didactic/shannon.ma +++ b/helm/software/matita/contribs/didactic/shannon.ma @@ -130,6 +130,7 @@ La libreria di Matita Per portare a termine l'esercitazione sono necessari i seguenti lemmi: * lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y` +* lemma `sem_bool` : `∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1` * lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false` * lemma `eq_to_eqb_true` : `∀x,y.x = y → eqb x y = true` * lemma `min_1_sem` : `∀F,v.min 1 [[ F ]]_v = [[ F ]]_v` @@ -138,7 +139,7 @@ Per portare a termine l'esercitazione sono necessari i seguenti lemmi: Nota su `x = y` e `eqb x y` --------------------------- -Se vi siete mai chiasti la differenza tra `x = y` ed `eqb x y` +Se vi siete mai chiesti la differenza tra `x = y` ed `eqb x y` quanto segue prova a chiarirla. Presi due numeri `x` e `y` in ℕ, dire che `x = y` significa i due numeri @@ -190,7 +191,7 @@ Il caso `FAtom` richiede maggiore cura. Assunto l'indice dell'atomo `n`, occorre utilizzare il lemma `decidable_eq_nat` per ottenere l'ipotesi aggiuntiva `n = x ∨ n ≠ x` (dove `x` è l'atomo su cui predica il teorema). Si procede per casi sull'ipotesi appena ottenuta. -In entrambi i casi, usanto i lemmi `eq_to_eqb_true` oppure `not_eq_to_eqb_false` +In entrambi i casi, usando i lemmi `eq_to_eqb_true` oppure `not_eq_to_eqb_false` si ottengolo le ipotesi aggiuntive `(eqb n x = true)` oppure `(eqb n x = false)`. Entrambi i casi si concludono con una catena di uguaglianze.