From be56c1bf3bf2b6821c42ce9911bea7a7e98afa71 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 28 Oct 2008 18:01:39 +0000 Subject: [PATCH] ... --- .../matita/contribs/didactic/duality.ma | 121 +++++++----------- 1 file changed, 46 insertions(+), 75 deletions(-) diff --git a/helm/software/matita/contribs/didactic/duality.ma b/helm/software/matita/contribs/didactic/duality.ma index 7fe9082e1..62087ab4a 100644 --- a/helm/software/matita/contribs/didactic/duality.ma +++ b/helm/software/matita/contribs/didactic/duality.ma @@ -92,11 +92,12 @@ inductive Formula : Type ≝ Modificare la funzione `sem` scritta nella precedente esercitazione in modo che valga solo 0 oppure 1 nel caso degli - atomi, anche nel caso il mondo `v` restituisca un numero + atomi, anche nel caso in cui il mondo `v` restituisca un numero maggiore di 1. Suggerimento: non è necessario usare il costrutto if_then_else - e tantomento il predicato di maggiore o uguale. + e tantomento il predicato di maggiore o uguale. È invece possibile + usare la funzione `min`. *) let rec sem (v: nat → nat) (F: Formula) on F : nat ≝ match F with @@ -132,7 +133,7 @@ definition v20 ≝ λx. `A` vale `2` e `C` vale `0` deve valere `1`. *) -eval normalize on [[For (FAtom 0) (FAtom 2)]]_v20. +eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. (*DOCBEGIN @@ -213,7 +214,9 @@ lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros * Scambia il connettivo FAnd con FOr e viceversa * Sostituisce il connettivo FImpl con FAnd e nega la - prima sottoformula. + prima sottoformula. Il razionale è che `FImpl A B` + è semanticamente equivalente a `FOr (FNot A) B` il + cui duale è `FAnd (FNot A) B`. Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in `¬A ∧ (B ∨ ⊤)`. @@ -248,7 +251,7 @@ eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))). *) definition invert ≝ - λv:ℕ -> ℕ. λx. if eqb (min (v x) 1) 0 then 1 else 0. + λv:ℕ → ℕ. λx. if eqb (min (v x) 1) 0 then 1 else 0. interpretation "Inversione del mondo" 'invert v = (invert v). @@ -260,10 +263,6 @@ Il linguaggio di dimostrazione di Matita Per dimostrare il lemma `negate_invert` in modo agevole è necessario utilizzare il seguente comando: -* `symmetry` - - Quando la conclusuine è `a = b` permette di cambiarla in `b = a`. - * by H1, H2 we proved P (H) Il comando `by ... we proved` visto nella scorsa esercitazione @@ -297,22 +296,20 @@ we proceed by induction on F to prove ([[ negate F ]]_v=[[ F ]]_(invert v)). done. case FAtom. assume n : ℕ. - the thesis becomes ([[ negate (FAtom n) ]]_v=[[ FAtom n ]]_(invert v)). - the thesis becomes (1 - (min (v n) 1)= min (invert v n) 1). + the thesis becomes ((*BEGIN*)[[ negate (FAtom n) ]]_v=[[ FAtom n ]]_(invert v)(*END*)). + the thesis becomes ((*BEGIN*)1 - (min (v n) 1)= min (invert v n) 1(*END*)). the thesis becomes (1 - (min (v n) 1)= min (if eqb (min (v n) 1) 0 then 1 else 0) 1). - by min_bool we proved ((*BEGIN*)min (v n) 1 = 0 ∨ min (v n) 1 = 1(*END*)) (H1); + by min_bool we proved (min (v n) 1 = 0 ∨ min (v n) 1 = 1) (H1); we proceed by cases on (H1) to prove (1 - (min (v n) 1)= min (if eqb (min (v n) 1) 0 then 1 else 0) 1). case Left. conclude (1 - (min (v n) 1)) = (1 - 0) by H. = 1. - symmetry. - conclude - (min (if eqb (min (v n) 1) O then 1 else O) 1) - = (min (if eqb 0 0 then 1 else O) 1) by H. = (min 1 1). - = 1. + = (min (if true then 1 else O) 1). + = (min (if eqb 0 0 then 1 else O) 1). + = (min (if eqb (min (v n) 1) O then 1 else O) 1) by H. done. case Right. (*BEGIN*) @@ -320,28 +317,25 @@ we proceed by induction on F to prove ([[ negate F ]]_v=[[ F ]]_(invert v)). (1 - (min (v n) 1)) = (1 - 1) by H. = 0. - symmetry. - conclude - (min (if eqb (min (v n) 1) O then 1 else O) 1) - = (min (if eqb 1 0 then 1 else O) 1) by H. = (min 0 1). - = 0. + = (min (if eqb 1 0 then 1 else O) 1). + = (min (if eqb (min (v n) 1) O then 1 else O) 1) by H. (*END*) done. case FAnd. assume f : Formula. by induction hypothesis we know - ([[ negate f ]]_v=[[ f ]]_(invert v)) (H). + ((*BEGIN*)[[ negate f ]]_v=[[ f ]]_(invert v)(*END*)) (H). assume f1 : Formula. by induction hypothesis we know - ([[ negate f1 ]]_v=[[ f1 ]]_(invert v)) (H1). + ((*BEGIN*)[[ negate f1 ]]_v=[[ f1 ]]_(invert v)(*END*)) (H1). the thesis becomes ([[ negate (FAnd f f1) ]]_v=[[ FAnd f f1 ]]_(invert v)). the thesis becomes (min [[ negate f ]]_v [[ negate f1]]_v = [[ FAnd f f1 ]]_(invert v)). conclude (min [[ negate f ]]_v [[ negate f1]]_v) - = (min [[ f ]]_(invert v) [[ negate f1]]_v) by H. + = (min [[ f ]]_(invert v) [[ negate f1]]_v) by (*BEGIN*)H(*END*). = (min [[ f ]]_(invert v) [[ f1]]_(invert v)) by (*BEGIN*)H1(*END*). done. case FOr. @@ -400,18 +394,16 @@ qed. Dimostrare che la funzione negate rispetta l'equivalenza. *) lemma negate_fun: - ∀F:Formula.∀G:Formula.F ≡ G→negate F ≡ negate G. - (*BEGIN*) - assume F:Formula. - assume G:Formula. - suppose (F ≡ G) (H). - the thesis becomes (negate F ≡ negate G). - the thesis becomes (∀v:ℕ→ℕ.[[ negate F ]]_v=[[ negate G ]]_v). - (*END*) + ∀F:Formula.∀G:Formula.F ≡ G → negate F ≡ negate G. + assume (*BEGIN*)F:Formula(*END*). + assume (*BEGIN*)G:Formula(*END*). + suppose (*BEGIN*)(F ≡ G) (H)(*END*). + the thesis becomes (*BEGIN*)(negate F ≡ negate G)(*END*). + the thesis becomes (*BEGIN*)(∀v:ℕ→ℕ.[[ negate F ]]_v=[[ negate G ]]_v)(*END*). assume v:(ℕ→ℕ). conclude [[ negate F ]]_v - = [[ F ]]_(invert v) by negate_invert. + = [[ F ]]_(invert v) by (*BEGIN*)negate_invert(*END*). = [[ G ]]_((*BEGIN*)invert v(*BEGIN*)) by (*BEGIN*)H(*BEGIN*). = [[ negate G ]]_(*BEGIN*)v(*BEGIN*) by (*BEGIN*)negate_invert(*END*). done. @@ -420,7 +412,7 @@ qed. (* Esercizio 6 =========== - Dimostrare che per ogni formula `F`, `(negae F)` equivale a + Dimostrare che per ogni formula `F`, `(negate F)` equivale a dualizzarla e negarla. *) lemma not_dualize_eq_negate: @@ -459,9 +451,9 @@ lemma not_dualize_eq_negate: the thesis becomes (min [[ negate f ]]_v [[ negate f1 ]]_v=[[ FNot (dualize (FAnd f f1)) ]]_v). conclude - (min [[ negate f ]]_v [[ negate f1 ]]_v) - = (min [[ FNot (dualize f) ]]_v [[ negate f1 ]]_v) by H. - = (min [[ FNot (dualize f) ]]_v [[ FNot (dualize f1) ]]_v) by H1. + (min (*BEGIN*)[[ negate f ]]_v(*END*) (*BEGIN*)[[ negate f1 ]]_v(*END*)) + = (min (*BEGIN*)[[ FNot (dualize f) ]]_v(*END*) (*BEGIN*)[[ negate f1 ]]_v(*END*)) by H. + = (min (*BEGIN*)[[ FNot (dualize f) ]]_v(*END*) (*BEGIN*)[[ FNot (dualize f1) ]]_v(*END*)) by H1. = (min (1 - [[ dualize f ]]_v) (1 - [[ dualize f1 ]]_v)). = (1 - (max [[ dualize f ]]_v [[ dualize f1 ]]_v)) by min_max. done. @@ -524,6 +516,13 @@ qed. Dimostrare che la negazione è iniettiva *) +lemma minus_injective : ∀x.x≤1 → 1 - (1 - x) = x. +intros; inversion H; intros; destruct; try reflexivity; +rewrite < (le_n_O_to_eq ? H1); reflexivity; +qed. + +lemma sem_le_1 : ∀F,v.[[F]]_v ≤ 1. intros; cases (sem_bool F v); rewrite > H; [2:apply le_n] apply le_O_n;qed. + theorem not_inj: ∀F,G:Formula.FNot F ≡ FNot G→F ≡ G. (*BEGIN*) @@ -534,44 +533,16 @@ theorem not_inj: the thesis becomes (∀v:ℕ→ℕ.[[ F ]]_v=[[ G ]]_v). (*END*) assume v:(ℕ→ℕ). + conclude + ([[F]]_v) + = (1 - (1 - [[F]]_v)) by (minus_injective [[F]]_v (sem_le_1 ??)). + = (1 - + = (1 - (1 - [[G]]_v)) + by H we proved ([[ FNot F ]]_v=[[ FNot G ]]_v) (H1). - by sem_bool we proved ([[ F ]]_v=O ∨ [[ F ]]_v=1) (H2). - by (*BEGIN*)sem_bool(*END*) we proved ([[ G ]]_v=(*BEGIN*)O ∨ [[ G ]]_v=1(*END*)) (H3). - we proceed by cases on H2 to prove ([[ F ]]_v=[[ G ]]_v). - case Left. - we proceed by cases on H3 to prove ([[ F ]]_v=[[ G ]]_v). - case Left. - done. - case Right. - conclude - ([[ F ]]_v) - = 0 by H4; - = (1 - 1). - = (1 - [[G]]_v) by H5. - = [[ FNot G ]]_v. - = [[ FNot F ]]_v by H1. - = (1 - [[F]]_v). - = (1 - 0) by H4. - = 1. - done. - case Right. - (*BEGIN*) - we proceed by cases on H3 to prove ([[ F ]]_v=[[ G ]]_v). - case Left. - conclude - ([[ F ]]_v) - = 1 by H4; - = (1 - 0). - = (1 - [[G]]_v) by H5. - = [[ FNot G ]]_v. - = [[ FNot F ]]_v by H1. - = (1 - [[F]]_v). - = (1 - 1) by H4. - = 0. - done. - case Right. - (*END*) - done. + using H1 we proved (1 - [[ F ]]_v=1 - [[ G ]]_v) (H2). + by minus_injective, sem_le_1 we proved ([[ F ]]_v=[[ G ]]_v) (H3); + done. qed. (*DOCBEGIN -- 2.39.2