]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/didactic/exercises/duality.ma
dca98ddc7652616d5e2f9a63977e28f061bd3e19
[helm.git] / helm / software / matita / library / didactic / exercises / duality.ma
1 (* Esercizio 0
2    ===========
3
4    Compilare i seguenti campi:
5
6    Nome1: ...
7    Cognome1: ...
8    Matricola1: ...
9    Account1: ...
10
11    Nome2: ...
12    Cognome2: ...
13    Matricola2: ...
14    Account2: ...
15
16    Prima di abbandonare la postazione:
17
18    * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella)
19      /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui
20      account è mrossi, deve salvare il file in /public/linguaggi_mrossi.ma
21
22    * mandatevi via email o stampate il file. Per stampare potete usare
23      usare l'editor gedit che offre la funzionalità di stampa
24 *)
25
26 (*DOCBEGIN
27
28 Il teorema di dualità
29 =====================
30
31 Il teorema di dualizzazione dice che date due formule `F1` ed `F2`,
32 se le due formule sono equivalenti (`F1 ≡ F2`) allora anche le 
33 loro dualizzate lo sono (`dualize F1 ≡ dualize F2`).
34
35 L'ingrediente principale è la funzione di dualizzazione di una formula `F`:
36    
37    * Scambia FTop con FBot e viceversa
38    
39    * Scambia il connettivo FAnd con FOr e viceversa
40    
41    * Sostituisce il connettivo FImpl con FAnd e nega la
42      prima sottoformula.
43    
44    Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in
45    `¬A ∧ (B ∨ ⊤)`.
46
47 Per dimostrare il teorema di dualizzazione in modo agevole è necessario
48 definire altre nozioni:
49
50 * La funzione `negate` che presa una formula `F` ne nega gli atomi.
51   Ad esempio la formula `(A ∨ (⊤ → B))` deve diventare `¬A ∨ (⊤ → ¬B)`.
52    
53 * La funzione `invert` permette di invertire un mondo `v`.
54   Ovvero, per ogni indice di atomo `i`, se `v i` restituisce
55   `1` allora `(invert v) i` restituisce `0` e viceversa.
56    
57 DOCEND*)
58
59 (* ATTENZIONE
60    ==========
61    
62    Non modificare quanto segue 
63 *)
64 include "nat/minus.ma".
65 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
66 notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
67 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
68 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
69 definition max ≝ λn,m. if eqb (n - m) 0 then m else n. 
70 definition min ≝ λn,m. if eqb (n - m) 0 then n else m. 
71
72 (* Ripasso
73    =======
74    
75    Il linguaggio delle formule, dove gli atomi sono
76    rapperesentati da un numero naturale
77 *)
78 inductive Formula : Type ≝
79 | FBot: Formula
80 | FTop: Formula
81 | FAtom: nat → Formula
82 | FAnd: Formula → Formula → Formula
83 | FOr: Formula → Formula → Formula
84 | FImpl: Formula → Formula → Formula
85 | FNot: Formula → Formula
86 .
87
88 (* Esercizio 1
89    ===========
90    
91    Modificare la funzione `sem` scritta nella precedente
92    esercitazione in modo che valga solo 0 oppure 1 nel caso degli
93    atomi, anche nel caso in cui il mondo `v` restituisca un numero
94    maggiore di 1.
95    
96    Suggerimento: non è necessario usare il costrutto if_then_else
97    e tantomento il predicato di maggiore o uguale. È invece possibile
98    usare la funzione `min`.
99 *) 
100 let rec sem (v: nat → nat) (F: Formula) on F : nat ≝
101  match F with
102   [ FBot ⇒ 0
103   | FTop ⇒ 1
104   | FAtom n ⇒ (*BEGIN*)min (v n) 1(*END*)
105   | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2)
106   | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
107   | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
108   | FNot F1 ⇒ 1 - (sem v F1)
109   ]
110 .
111
112 (* ATTENZIONE
113    ==========
114    
115    Non modificare quanto segue.
116 *)
117 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
118 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
119 notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
120 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
121
122 definition v20 ≝ λx.
123        if eqb x 0 then 2
124   else if eqb x 1 then 1
125   else                 0.
126   
127 (* Test 1
128    ======
129    
130    La semantica della formula `(A ∨ C)` nel mondo `v20` in cui 
131    `A` vale `2` e `C` vale `0` deve valere `1`.
132    
133    Decommenta ed esegui.
134 *)    
135
136 (* eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. *) 
137
138 (*DOCBEGIN
139
140 La libreria di Matita
141 =====================
142
143 Gli strumenti per la dimostrazione assistita sono corredati da
144 librerie di teoremi già dimostrati. Per portare a termine l'esercitazione
145 sono necessari i seguenti lemmi:
146
147 * lemma `sem_le_1` : `∀F,v. [[ F ]]_v ≤ 1`
148 * lemma `min_1_1` : `∀x. x ≤ 1 → 1 - (1 - x) = x`
149 * lemma `min_bool` : `∀n. min n 1 = 0 ∨ min n 1 = 1`
150 * lemma `min_max` : `∀F,G,v.min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v`
151 * lemma `max_min` : `∀F,G,v.max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v`
152 * lemma `equiv_rewrite` : `∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3`
153
154 DOCEND*)
155
156 (* ATTENZIONE
157    ==========
158    
159    Non modificare quanto segue.
160 *)
161 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.
162 lemma min_bool : ∀n. min n 1 = 0 ∨ min n 1 = 1.  intros; cases n; [left;reflexivity] cases n1; right; reflexivity; qed.  
163 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.
164 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.
165 lemma min_1_1 : ∀x.x ≤ 1 → 1 - (1 - x) = x. intros; inversion H; intros; destruct; [reflexivity;] rewrite < (le_n_O_to_eq ? H1); reflexivity;qed.
166 lemma sem_le_1 : ∀F,v.[[F]]_v ≤ 1. intros; cases (sem_bool F v); rewrite > H; [apply le_O_n|apply le_n]qed.
167
168 (* Esercizio 2
169    ===========
170    
171    Definire per ricorsione strutturale la funzione `negate`
172    che presa una formula `F` ne nega gli atomi.
173    
174    Ad esempio la formula `(A ∨ (⊤ → B))` deve diventare
175    `¬A ∨ (⊤ → ¬B)`.
176 *)
177 let rec negate (F: Formula) on F : Formula ≝
178  match F with
179   [ (*BEGIN*)FBot ⇒ FBot
180   | FTop ⇒ FTop
181   | FAtom n ⇒ FNot (FAtom n)
182   | FAnd F1 F2 ⇒ FAnd (negate F1) (negate F2)
183   | FOr F1 F2 ⇒ FOr (negate F1) (negate F2)
184   | FImpl F1 F2 ⇒ FImpl (negate F1) (negate F2)
185   | FNot F ⇒ FNot (negate F)(*END*)
186   ].
187
188 (* Test 2
189    ======
190   
191    Testare la funzione `negate`. Il risultato atteso è:
192    
193        FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1)))
194        
195    Decommenta ed esegui 
196 *)
197
198 (* eval normalize on (negate (FOr (FAtom 0) (FImpl FTop (FAtom 1)))). *)
199
200 (* ATTENZIONE
201    ==========
202    
203    Non modificare quanto segue
204 *)
205 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
206 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
207 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
208 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
209 lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; autobatch. qed.
210
211 (* Esercizio 3
212    ===========
213    
214    Definire per ricorsione strutturale la funzione di
215    dualizzazione di una formula `F`. Tale funzione:
216    
217    * Scambia FTop con FBot e viceversa
218    
219    * Scambia il connettivo FAnd con FOr e viceversa
220    
221    * Sostituisce il connettivo FImpl con FAnd e nega la
222      prima sottoformula. Il razionale è che `FImpl A B`
223      è semanticamente equivalente a `FOr (FNot A) B` il
224      cui duale è `FAnd (FNot A) B`.
225    
226    Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in
227    `¬A ∧ (B ∨ ⊤)`. 
228 *)  
229 let rec dualize (F : Formula) on F : Formula ≝
230   match F with
231   [ (*BEGIN*)FBot ⇒ FTop
232   | FTop ⇒ FBot
233   | FAtom n ⇒ FAtom n
234   | FAnd F1 F2 ⇒ FOr (dualize F1) (dualize F2)
235   | FOr F1 F2 ⇒ FAnd (dualize F1) (dualize F2)
236   | FImpl F1 F2 ⇒ FAnd (FNot (dualize F1)) (dualize F2)
237   | FNot F ⇒ FNot (dualize F)(*END*)
238   ].
239
240 (* Test 3
241    ======
242    
243    Testare la funzione `dualize`. Il risultato atteso è:
244    
245        FAnd (FNot (FAtom O)) (FOr (FAtom 1) FTop) 
246        
247    Decommenta ed esegui.
248 *)
249
250 (* eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))). *)
251
252 (* Spiegazione
253    ===========
254    
255    La funzione `invert` permette di invertire un mondo `v`.
256    Ovvero, per ogni indice di atomo `i`, se `v i` restituisce
257    `1` allora `(invert v) i` restituisce `0` e viceversa.
258    
259 *)
260 definition invert ≝
261  λv:ℕ → ℕ. λx. if eqb (min (v x) 1) 0 then 1 else 0.
262  
263 interpretation "Inversione del mondo" 'invert v = (invert v).
264  
265 (*DOCBEGIN
266
267 Il linguaggio di dimostrazione di Matita
268 ========================================
269
270 Per dimostrare il lemma `negate_invert` in modo agevole è necessario 
271 utilizzare il seguente comando:
272
273 * by H1, H2 we proved P (H)
274
275   Il comando `by ... we proved` visto nella scorsa esercitazione
276   permette di utilizzare più ipotesi o lemmi alla volta
277   separandoli con una virgola.
278
279 DOCEND*)
280
281 (* Esercizio 4
282    ===========
283    
284    Dimostrare il lemma `negate_invert` che asserisce che
285    la semantica in un mondo `v` associato alla formula
286    negata di `F` e uguale alla semantica associata
287    a `F` in un mondo invertito.
288 *) 
289 lemma negate_invert:
290   ∀F:Formula.∀v:ℕ→ℕ.[[ negate F ]]_v=[[ F ]]_(invert v).
291 assume F:Formula.
292 assume v:(ℕ→ℕ).
293 we proceed by induction on F to prove ([[ negate F ]]_v=[[ F ]]_(invert v)).
294   case FBot.
295     (*BEGIN*)
296     the thesis becomes ([[ negate FBot ]]_v=[[ FBot ]]_(invert v)).
297     (*END*)
298   done.
299   case FTop.
300     (*BEGIN*)
301     the thesis becomes ([[ negate FTop ]]_v=[[ FTop ]]_(invert v)).
302     (*END*)
303   done.
304   case FAtom.
305     assume n : ℕ.
306     the thesis becomes ((*BEGIN*)[[ negate (FAtom n) ]]_v=[[ FAtom n ]]_(invert v)(*END*)).
307     the thesis becomes ((*BEGIN*)1 - (min (v n) 1)= min (invert v n) 1(*END*)).
308     the thesis becomes (1 - (min (v n) 1)= min (if eqb (min (v n) 1) 0 then 1 else 0) 1).
309     by min_bool we proved (min (v n) 1 = 0 ∨ min (v n) 1 = 1) (H1);
310     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).
311       case Left.
312         conclude 
313             (1 - (min (v n) 1)) 
314           = (1 - 0) by H.
315           = 1.
316           = (min 1 1).
317           = (min (if true then 1 else O) 1).
318           = (min (if eqb 0 0 then 1 else O) 1).
319           = (min (if eqb (min (v n) 1) O then 1 else O) 1) by H.
320       done.
321       case Right.
322         (*BEGIN*)
323         conclude 
324             (1 - (min (v n) 1)) 
325           = (1 - 1) by H.
326           = 0.
327           = (min 0 1).
328           = (min (if eqb 1 0 then 1 else O) 1).
329           = (min (if eqb (min (v n) 1) O then 1 else O) 1) by H.
330         (*END*)
331       done.
332   case FAnd.
333     assume f : Formula.
334     by induction hypothesis we know
335       ((*BEGIN*)[[ negate f ]]_v=[[ f ]]_(invert v)(*END*)) (H).
336     assume f1 : Formula.
337     by induction hypothesis we know
338      ((*BEGIN*)[[ negate f1 ]]_v=[[ f1 ]]_(invert v)(*END*)) (H1).
339     the thesis becomes
340      ([[ negate (FAnd f f1) ]]_v=[[ FAnd f f1 ]]_(invert v)).
341     the thesis becomes
342      (min [[ negate f ]]_v [[ negate f1]]_v = [[ FAnd f f1 ]]_(invert v)).
343     conclude 
344         (min [[ negate f ]]_v [[ negate f1]]_v)
345       = (min [[ f ]]_(invert v) [[ negate f1]]_v) by (*BEGIN*)H(*END*).
346       = (min [[ f ]]_(invert v) [[ f1]]_(invert v)) by (*BEGIN*)H1(*END*).
347   done.
348   case FOr.
349     (*BEGIN*)
350     assume f : Formula.
351     by induction hypothesis we know
352       ([[ negate f ]]_v=[[ f ]]_(invert v)) (H).
353     assume f1 : Formula.
354     by induction hypothesis we know
355      ([[ negate f1 ]]_v=[[ f1 ]]_(invert v)) (H1).
356     the thesis becomes
357      ([[ negate (FOr f f1) ]]_v=[[ FOr f f1 ]]_(invert v)).
358     the thesis becomes
359      (max [[ negate f ]]_v [[ negate f1]]_v = [[ FOr f f1 ]]_(invert v)).
360     conclude 
361         (max [[ negate f ]]_v [[ negate f1]]_v)
362       = (max [[ f ]]_(invert v) [[ negate f1]]_v) by H.
363       = (max [[ f ]]_(invert v) [[ f1]]_(invert v)) by H1.
364     (*END*)
365   done.
366   case FImpl.
367     (*BEGIN*)
368     assume f : Formula.
369     by induction hypothesis we know
370       ([[ negate f ]]_v=[[ f ]]_(invert v)) (H).
371     assume f1 : Formula.
372     by induction hypothesis we know
373      ([[ negate f1 ]]_v=[[ f1 ]]_(invert v)) (H1).
374     the thesis becomes
375      ([[ negate (FImpl f f1) ]]_v=[[ FImpl f f1 ]]_(invert v)).
376     the thesis becomes
377      (max (1 - [[ negate f ]]_v) [[ negate f1]]_v = [[ FImpl f f1 ]]_(invert v)).
378     conclude 
379         (max (1 - [[ negate f ]]_v) [[ negate f1]]_v)
380       = (max (1 - [[ f ]]_(invert v)) [[ negate f1]]_v) by H.
381       = (max (1 - [[ f ]]_(invert v)) [[ f1]]_(invert v)) by H1.
382     (*END*)
383   done.
384   case FNot.
385     (*BEGIN*)
386     assume f : Formula.
387     by induction hypothesis we know
388       ([[ negate f ]]_v=[[ f ]]_(invert v)) (H).
389     the thesis becomes
390       ([[ negate (FNot f) ]]_v=[[ FNot f ]]_(invert v)).
391     the thesis becomes
392       (1 - [[ negate f ]]_v=[[ FNot f ]]_(invert v)).
393     conclude (1 - [[ negate f ]]_v) = (1 - [[f]]_(invert v)) by H.
394     (*END*)
395   done.  
396 qed.   
397
398 (* Esercizio 5
399    ===========
400    
401    Dimostrare che la funzione negate rispetta l'equivalenza.
402 *)
403 lemma negate_fun:
404  ∀F:Formula.∀G:Formula.F ≡ G → negate F ≡ negate G.
405  assume (*BEGIN*)F:Formula(*END*).
406  assume (*BEGIN*)G:Formula(*END*).
407  suppose (*BEGIN*)(F ≡ G) (H)(*END*).
408  the thesis becomes (*BEGIN*)(negate F ≡ negate G)(*END*).
409  the thesis becomes (*BEGIN*)(∀v:ℕ→ℕ.[[ negate F ]]_v=[[ negate G ]]_v)(*END*).
410  assume v:(ℕ→ℕ).
411  conclude 
412      [[ negate F ]]_v
413    = [[ F ]]_(invert v) by (*BEGIN*)negate_invert(*END*).
414    = [[ G ]]_((*BEGIN*)invert v(*BEGIN*)) by (*BEGIN*)H(*BEGIN*).
415    = [[ negate G ]]_(*BEGIN*)v(*BEGIN*) by (*BEGIN*)negate_invert(*END*).
416  done.  
417 qed.
418
419 (* Esercizio 6
420    ===========
421    
422    Dimostrare che per ogni formula `F`, `(negate F)` equivale a 
423    dualizzarla e negarla.
424 *)
425 lemma not_dualize_eq_negate:
426  ∀F:Formula.negate F ≡ FNot (dualize F).
427  (*BEGIN*)
428  assume F:Formula.
429  the thesis becomes (∀v:ℕ→ℕ.[[negate F]]_v=[[FNot (dualize F)]]_v).
430  (*END*)
431  assume v:(ℕ→ℕ).
432  we proceed by induction on F to prove ([[negate F]]_v=[[FNot (dualize F)]]_v).
433  case FBot.
434    (*BEGIN*)
435    the thesis becomes ([[ negate FBot ]]_v=[[ FNot (dualize FBot) ]]_v).
436    (*END*)
437  done.
438  case FTop.
439    (*BEGIN*)
440    the thesis becomes ([[ negate FTop ]]_v=[[ FNot (dualize FTop) ]]_v).
441    (*END*)
442  done.
443  case FAtom.
444    (*BEGIN*)
445    assume n : ℕ.
446    the thesis becomes ([[ negate (FAtom n) ]]_v=[[ FNot (dualize (FAtom n)) ]]_v).
447    (*END*)
448  done.
449  case FAnd.
450    assume f : Formula.
451    by induction hypothesis we know
452      ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H).
453    assume f1 : Formula.
454    by induction hypothesis we know
455     ([[ negate f1 ]]_v=[[ FNot (dualize f1) ]]_v) (H1).
456    the thesis becomes
457     ([[ negate (FAnd f f1) ]]_v=[[ FNot (dualize (FAnd f f1)) ]]_v).
458    the thesis becomes
459     (min [[ negate f ]]_v [[ negate f1 ]]_v=[[ FNot (dualize (FAnd f f1)) ]]_v).
460    conclude 
461        (min (*BEGIN*)[[ negate f ]]_v(*END*) (*BEGIN*)[[ negate f1 ]]_v(*END*))
462      = (min (*BEGIN*)[[ FNot (dualize f) ]]_v(*END*) (*BEGIN*)[[ negate f1 ]]_v(*END*)) by H.    
463      = (min (*BEGIN*)[[ FNot (dualize f) ]]_v(*END*) (*BEGIN*)[[ FNot (dualize f1) ]]_v(*END*)) by H1.
464      = (min (1 - [[ dualize f ]]_v) (1 - [[ dualize f1 ]]_v)).
465      = (1 - (max [[ dualize f ]]_v [[ dualize f1 ]]_v)) by min_max.
466  done.
467  case FOr.
468    (*BEGIN*)
469    assume f : Formula.
470    by induction hypothesis we know
471      ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H).
472    assume f1 : Formula.
473    by induction hypothesis we know
474     ([[ negate f1 ]]_v=[[ FNot (dualize f1) ]]_v) (H1).
475    the thesis becomes
476     ([[ negate (FOr f f1) ]]_v=[[ FNot (dualize (FOr f f1)) ]]_v).
477    the thesis becomes
478     (max [[ negate f ]]_v [[ negate f1 ]]_v=[[ FNot (dualize (FOr f f1)) ]]_v).
479    conclude 
480        (max [[ negate f ]]_v [[ negate f1 ]]_v)
481      = (max [[ FNot (dualize f) ]]_v [[ negate f1 ]]_v) by H.    
482      = (max [[ FNot (dualize f) ]]_v [[ FNot (dualize f1) ]]_v) by H1.
483      = (max (1 - [[ dualize f ]]_v) (1 - [[ dualize f1 ]]_v)).
484      = (1 - (min [[ dualize f ]]_v [[ dualize f1 ]]_v)) by max_min.
485    (*END*)
486  done.
487  case FImpl.
488    (*BEGIN*)
489    assume f : Formula.
490    by induction hypothesis we know
491      ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H).
492    assume f1 : Formula.
493    by induction hypothesis we know
494     ([[ negate f1 ]]_v=[[ FNot (dualize f1) ]]_v) (H1).
495    the thesis becomes
496     ([[ negate (FImpl f f1) ]]_v=[[ FNot (dualize (FImpl f f1)) ]]_v).
497    the thesis becomes
498     (max (1 - [[ negate f ]]_v) [[ negate f1 ]]_v=[[ FNot (dualize (FImpl f f1)) ]]_v).
499    conclude 
500        (max (1-[[ negate f ]]_v) [[ negate f1 ]]_v)
501      = (max (1-[[ FNot (dualize f) ]]_v) [[ negate f1 ]]_v) by H.    
502      = (max (1-[[ FNot (dualize f) ]]_v) [[ FNot (dualize f1) ]]_v) by H1.
503      = (max (1 - [[ FNot (dualize f) ]]_v) (1 - [[ dualize f1 ]]_v)).
504      = (1 - (min [[ FNot (dualize f) ]]_v [[ dualize f1 ]]_v)) by max_min.
505    (*END*)
506  done.
507  case FNot.
508    (*BEGIN*) 
509    assume f : Formula.
510    by induction hypothesis we know
511      ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H).
512    the thesis becomes
513       ([[ negate (FNot f) ]]_v=[[ FNot (dualize (FNot f)) ]]_v).
514    the thesis becomes
515       (1 - [[ negate f ]]_v=[[ FNot (dualize (FNot f)) ]]_v).
516    conclude (1 - [[ negate f ]]_v) = (1 - [[ FNot (dualize f) ]]_v) by H.
517    (*END*)
518  done.
519 qed.
520
521 (* Esercizio 7
522    ===========
523    
524    Dimostrare che la negazione è iniettiva
525 *)
526 theorem not_inj:
527  ∀F,G:Formula.FNot F ≡ FNot G→F ≡ G.
528  (*BEGIN*)
529  assume F:Formula.
530  assume G:Formula.
531  suppose (FNot F ≡ FNot G) (H).
532  the thesis becomes (F ≡ G).
533  the thesis becomes (∀v:ℕ→ℕ.[[ F ]]_v=[[ G ]]_v).
534  (*END*)
535  assume v:(ℕ→ℕ).
536  by sem_le_1 we proved ([[F]]_v ≤ 1) (H1).
537  by (*BEGIN*)sem_le_1(*END*) we proved ([[G]]_v ≤ 1) (H2).
538  by min_1_1, H1 we proved (1 - (1 - [[F]]_v) = [[F]]_v) (H3).
539  by (*BEGIN*)min_1_1, H2(*END*) we proved ((*BEGIN*)1 - (1 - [[G]]_v)(*END*) = [[G]]_v) (H4).
540  conclude 
541      ([[F]]_v)
542    = (1 - (1 - [[F]]_v)) by (*BEGIN*)H3(*END*).
543    = (1 - [[(*BEGIN*)FNot F(*END*)]]_v).
544    = (1 - [[ FNot G]]_v) by H.
545    = (1 - (*BEGIN*)(1 - [[G]]_v)(*END*)).
546    = [[G]]_v by (*BEGIN*)H4(*END*).
547  done.
548 qed.
549
550 (*DOCBEGIN
551
552 La prova del teorema di dualità
553 ===============================
554
555 Il teorema di dualità accennato a lezione dice che se due formule 
556 `F1` ed `F2` sono equivalenti, allora anche le formule duali lo sono.
557         
558     ∀F1,F2:Formula. F1 ≡ F2 → dualize F1 ≡ dualize F2.
559         
560 Per dimostrare tale teorema è bene suddividere la prova in lemmi intermedi
561
562 1. lemma `negate_invert`, dimostrato per induzione su F, utilizzando
563    `min_bool`
564    
565         ∀F:Formula.∀v:ℕ→ℕ.[[ negate F ]]_v=[[ F ]]_(invert v).
566
567 2. lemma `negate_fun`, conseguenza di `negate_invert`
568
569         ∀F,G:Formula. F ≡ G → negate F ≡ negate G.
570         
571 2. lemma `not_dualize_eq_negate`, dimostrato per induzione su F,
572    utilizzando `max_min` e `min_max`
573
574         ∀F:Formula. negate F ≡ FNot (dualize F)
575         
576 4. lemma `not_inj`, conseguenza di `sem_bool`
577  
578         ∀F,G:Formula. FNot F ≡ FNot G → F ≡ G
579
580 Una volta dimostrati tali lemmi la prova del teorema di dualità 
581 procede come di seguito:
582
583 1. Assume l'ipotesi  
584
585         F1 ≡ F2
586
587 2. Utilizza `negate_fun` per ottenere 
588
589         negate F1 ≡ negate F2
590
591 3. Utilizzando due volte il lemma `not_dualize_eq_negate` e il lemma
592    `equiv_rewrite` ottiene 
593
594         FNot (dualize F1) ≡ FNot (dualize F2)
595
596 4. Conclude utilizzando il lemma `not_inj` per ottenere la tesi 
597
598         dualize F1 ≡ dualize F2
599
600 DOCEND*)
601
602 (* Esercizio 8
603    ===========
604    
605    Dimostrare il teorema di dualità
606 *)
607 theorem duality: ∀F1,F2:Formula.F1 ≡ F2 → dualize F1 ≡ dualize F2.
608  assume F1:Formula.
609  assume F2:Formula.
610  suppose (F1 ≡ F2) (H).
611  the thesis becomes (dualize F1 ≡ dualize F2).
612  by (*BEGIN*)negate_fun(*END*), H we proved (negate F1 ≡ negate F2) (H1).
613  by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H1 we proved (FNot (dualize F1) ≡ negate F2) (H2).
614  by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H2 we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3).
615  by (*BEGIN*)not_inj(*END*), H3 we proved (dualize F1 ≡ dualize F2) (H4).
616  by H4 done.
617 qed.