From b59bfafcea1d2b429be753fd762b53b231b58dad Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 26 Oct 2008 13:41:07 +0000
Subject: [PATCH] almost done, just needs to be prforated

---
 .../matita/contribs/didactic/duality.ma       | 144 ++++++++++++++----
 1 file changed, 115 insertions(+), 29 deletions(-)

diff --git a/helm/software/matita/contribs/didactic/duality.ma b/helm/software/matita/contribs/didactic/duality.ma
index 44b7880fa..4eaa9c7e3 100644
--- a/helm/software/matita/contribs/didactic/duality.ma
+++ b/helm/software/matita/contribs/didactic/duality.ma
@@ -25,6 +25,39 @@
      usare l'editor gedit che offre la funzionalità di stampa
 *)
 
+(*DOCBEGIN
+
+Il teorema di dualità
+=====================
+
+Il teorema di dualizzazione dice che date due formule `F1` ed `F2`,
+se le due formule sono equivalenti (`F1 ≡ F2`) allora anche le 
+loro dualizzate lo sono (`dualize F1 ≡ dualize F2`).
+
+L'ingrediente principale è la funzione di dualizzazione di una formula `F`:
+   
+   * Scambia FTop con FBot e viceversa
+   
+   * Scambia il connettivo FAnd con FOr e viceversa
+   
+   * Sostituisce il connettivo FImpl con FAnd e nega la
+     prima sottoformula.
+   
+   Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in
+   `¬A ∧ (B ∨ ⊤)`.
+
+Per dimostrare il teorema di dualizzazione in modo agevole è necessario
+definire altre nozioni:
+
+* La funzione `negate` che presa una formula `F` ne nega gli atomi.
+  Ad esempio la formula `(A ∨ (⊤ → B))` deve diventare `¬A ∨ (⊤ → ¬B)`.
+   
+* La funzione `invert` permette di invertire un mondo `v`.
+  Ovvero, per ogni indice di atomo `i`, se `v i` restituisce
+  `1` allora `(invert v) i` restituisce `0` e viceversa.
+   
+DOCEND*)
+
 (* ATTENZIONE
    ==========
    
@@ -61,6 +94,9 @@ inductive Formula : Type ≝
    esercitazione in modo che valga solo 0 oppure 1 nel caso degli
    atomi, anche nel caso 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.
 *) 
 let rec sem (v: nat → nat) (F: Formula) on F ≝
  match F with
@@ -98,34 +134,32 @@ definition v20 ≝ λx.
 *)    
 eval normalize on [[For (FAtom 0) (FAtom 2)]]_v20. 
 
+(*DOCBEGIN
+
+La libreria di Matita
+=====================
+
+Gli strumenti per la dimostrazione assistita sono corredati da
+librerie di teoremi già dimostrati. Per portare a termine l'esercitazione
+sono necessari i seguenti lemmi:
+
+* lemma `sem_bool` : `∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1`
+* lemma `min_bool` : `∀n. min n 1 = 0 ∨ min n 1 = 1`
+* lemma `min_max` : `∀F,G,v.min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v`
+* lemma `max_min` : `∀F,G,v.max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v`
+* lemma `equiv_rewrite` : `∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3`
+
+DOCEND*)
 
 (* ATTENZIONE
    ==========
    
    Non modificare quanto segue.
 *)
-lemma sem_bool : ∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1.
-intros; elim F; simplify;
-[left;reflexivity;
-|right;reflexivity;
-|cases (v n);[left;|cases n1;right;]reflexivity;
-|4,5,6: cases H; cases H1; rewrite > H2; rewrite > H3; simplify;
-   first [ left;reflexivity | right; reflexivity ].
-|cases H; rewrite > H1; simplify;[right|left]reflexivity;]
-qed.
-lemma min_bool : ∀n. min n 1 = 0 ∨ min n 1 = 1.
-intros; cases n; [left;reflexivity] cases n1; right; reflexivity;
-qed.  
-lemma min_max : ∀F,G,v.
-  min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v.
-intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1;
-simplify; reflexivity;
-qed.
-lemma max_min : ∀F,G,v.
-  max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v.
-intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1;
-simplify; reflexivity;
-qed.
+lemma sem_bool : ∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1.  intros; elim F; simplify; [left;reflexivity; |right;reflexivity; |cases (v n);[left;|cases n1;right;]reflexivity; |4,5,6: cases H; cases H1; rewrite > H2; rewrite > H3; simplify; first [ left;reflexivity | right; reflexivity ].  |cases H; rewrite > H1; simplify;[right|left]reflexivity;] qed.
+lemma min_bool : ∀n. min n 1 = 0 ∨ min n 1 = 1.  intros; cases n; [left;reflexivity] cases n1; right; reflexivity; qed.  
+lemma min_max : ∀F,G,v.  min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v.  intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed.
+lemma max_min : ∀F,G,v.  max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v.  intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed.
 
 (* Esercizio 2
    ===========
@@ -174,7 +208,7 @@ lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros
    Definire per ricorsione strutturale la funzione di
    dualizzazione di una formula `F`. Tale funzione:
    
-   * Sambia FTop con FBot e viceversa
+   * Scambia FTop con FBot e viceversa
    
    * Scambia il connettivo FAnd con FOr e viceversa
    
@@ -186,13 +220,13 @@ lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros
 *)  
 let rec dualize (F : Formula) on F : Formula ≝
   match F with
-  [ FBot ⇒ FTop
+  [ (*BEGIN*)FBot ⇒ FTop
   | FTop ⇒ FBot
   | FAtom n ⇒ FAtom n
   | FAnd F1 F2 ⇒ FOr (dualize F1) (dualize F2)
   | FOr F1 F2 ⇒ FAnd (dualize F1) (dualize F2)
   | FImpl F1 F2 ⇒ FAnd (FNot (dualize F1)) (dualize F2)
-  | FNot F ⇒ FNot (dualize F)
+  | FNot F ⇒ FNot (dualize F)(*END*)
   ].
 
 (* Test 3
@@ -211,6 +245,7 @@ eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))).
    La funzione `invert` permette di invertire un mondo `v`.
    Ovvero, per ogni indice di atomo `i`, se `v i` restituisce
    `1` allora `(invert v) i` restituisce `0` e viceversa.
+   
 *)
 definition invert ≝
  λv:ℕ -> ℕ. λx. if eqb (min (v x) 1) 0 then 1 else 0.
@@ -456,7 +491,7 @@ qed.
    Dimostrare che la negazione è iniettiva
 *)
 theorem not_inj:
- ∀F:Formula.∀G:Formula.FNot F ≡ FNot G→F ≡ G.
+ ∀F,G:Formula.FNot F ≡ FNot G→F ≡ G.
  assume F:Formula.
  assume G:Formula.
  suppose (FNot F ≡ FNot G) (H).
@@ -501,13 +536,64 @@ theorem not_inj:
    done.
 qed.
 
+(*DOCBEGIN
+
+La prova del teorema di dualità
+===============================
+
+Il teorema di dualità accennato a lezione dice che se due formule 
+`F1` ed `F2` sono equivalenti, allora anche le formule duali lo sono.
+        
+    ∀F1,F2:Formula. F1 ≡ F2 → dualize F1 ≡ dualize F2.
+        
+Per dimostrare tale teorema è bene suddividere la prova in lemmi intermedi
+
+1. lemma `negate_invert`, dimostrato per induzione su F, utilizzando
+   `min_bool`
+   
+        ∀F:Formula.∀v:ℕ→ℕ.[[ negate F ]]_v=[[ F ]]_(invert v).
+
+2. lemma `negate_fun`, conseguenza di `negate_invert`
+
+        ∀F,G:Formula. F ≡ G → negate F ≡ negate G.
+        
+2. lemma `not_dualize_eq_negate`, dimostrato per induzione su F,
+   utilizzando `max_min` e `min_max`
+
+        ∀F:Formula. negate F ≡ FNot (dualize F)
+        
+4. lemma `not_inj`, conseguenza di `sem_bool`
+ 
+        ∀F,G:Formula. FNot F ≡ FNot G → F ≡ G
+
+Una volta dimostrati tali lemmi la prova del teorema di dualità 
+procede come di seguito:
+
+1. Assume l'ipotesi  
+
+        F1 ≡ F2
+
+2. Utilizza `negate_fun` per ottenere 
+
+        negate F1 ≡ negate F2
+
+3. Utilizzando due volte il lemma `not_dualize_eq_negate` e il lemma
+   `equiv_rewrite` ottiene 
+
+        FNot (dualize F1) ≡ FNot (dualize F2)
+
+4. Conclude utilizzando il lemma `not_inj` per ottenere la tesi 
+
+        dualize F1 ≡ dualize F2
+
+DOCEND*)
+
 (* Esercizio 8
    ===========
    
    Dimostrare il teorema di dualità
 *)
-theorem duality:
- ∀F1:Formula.∀F2:Formula.F1 ≡ F2 → dualize F1 ≡ dualize F2.
+theorem duality: ∀F1,F2:Formula.F1 ≡ F2 → dualize F1 ≡ dualize F2.
  assume F1:Formula.
  assume F2:Formula.
  suppose (F1 ≡ F2) (H).
@@ -517,4 +603,4 @@ theorem duality:
  by not_dualize_eq_negate, equiv_rewrite we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3).
  by not_inj we proved (dualize F1 ≡ dualize F2) (H4).
  done.
-qed.
\ No newline at end of file
+qed.
-- 
2.39.2