]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/didactic/exercises/substitution.ma
updating the structures for sorts
[helm.git] / helm / software / matita / library / didactic / exercises / substitution.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* Esercizio 0 
16    ===========
17    
18    Compilare i seguenti campi:
19    
20    Nome1: ...
21    Cognome1: ...
22    Matricola1: ...
23    Account1: ...
24    
25    Nome2: ...
26    Cognome2: ...
27    Matricola2: ...
28    Account2: ...
29
30    Prima di abbandonare la postazione:
31
32    * compilare il questionario in fondo al file
33    
34    * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella)
35      /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui
36      account è mrossi, deve salvare il file in /public/linguaggi_mrossi.ma
37
38    * mandatevi via email o stampate il file. Per stampare potete usare
39      usare l'editor gedit che offre la funzionalità di stampa
40 *)
41
42 (*DOCBEGIN
43
44 Come scrivere i simboli
45 =======================
46
47 Per inserire i simboli matematici è necessario digitare il loro nome
48 e poi premere ALT-L. In generale i nomi dei simboli sono della forma
49 `\nome`, ad esempio `\equiv`. Alcuni simboli molto frequenti hanno
50 dei sinonimi più comodi da digitare, per esemio `⇒` ha sia il nome
51 `\Rightarrow` sia `=>`.
52
53 Segue un elenco dei simboli più comuni e i loro nomi separati da virgola,
54 Se sono necessari dei simboli non riportati di seguito si può visualizzare
55 l'intera lista dal menù a tendina `View ▹ TeX/UTF8 table`.
56  
57 * `→` : `\to`, `->`
58 * `⇒` : `\Rightarrow`, `=>`
59 * `ℕ` : `\naturals`
60 * `≝` : `\def`, `:=`
61 * `≡` : `\equiv`
62 * `∀` : `\forall`
63
64 La sintassi `∀x.P` significa "per tutti gli `x` vale `P`".
65
66 La sintassi `F → G` dove `F` e `G` sono proposizioni nel metalinguaggio
67 significa "`F` implica `G`". Attenzione, il simbolo `⇒` (usato a lezione)
68 non ha lo stesso significato in Matita.
69
70 La sintassi `ℕ → ℕ` è il tipo delle funzioni che preso un numero naturale
71 restituiscono un numero naturale. 
72
73 La sintassi di Matita
74 =====================
75
76 Il linguaggio di Matita si basa sul λ-calcolo CIC, la cui sintassi si 
77 differenzia in vari aspetti da quella che solitamente viene utilizzata
78 per fare matematica, e ricorda quella di Scheme che state vedendo nel corso
79 di programmazione. 
80
81 * applicazione
82
83   Se `f` è una funzione che si aspetta due argomenti, l'applucazione di `f`
84   agli argomenti `x` e `y` si scrive `(f x y)` e non `f(x,y)`. Le parentesi
85   possono essere omesse se il senso è chiaro dal contesto. In particolare
86   vengono omesse quando l'applicazione è argomento di un operatore binario.
87   Esempio: `f x y + f y x` si legge `(f x y) + (f y x)`.  
88  
89 * minimo e massimo
90
91   Le funzioni `min` e `max` non fanno eccezione, per calcolare il 
92   massimo tra `x` e `y` si scrive `(max x y)` e non `max{x,y}`
93
94 * Le funzioni definite per ricorsione strutturale utilizzano il costrutto 
95   `let rec` (ricorsione) e il costrutto `match` (analisi per casi).
96
97   Ad esempio la funzione count definita a lezione come
98   
99         count ⊤ ≝ 1
100         count (F1 ∧ F2) ≝ 1 + count F1 + count F2 
101         ...
102      
103   la si esprime come
104   
105         let rec count F on F ≝ 
106           match F with 
107           [ ⊤ ⇒ 1 
108           | F1 ∧ F2 ⇒ 1 + count F1 + count F2 
109           ...
110           ].
111        
112 * Per dare la definizione ricorsiva (di un linguaggio) si usa una sintassi 
113   simile a BNF. Per esempio per definire 
114   
115         <A> ::= <A> "+" <A> | <A> "*" <A> | "0" | "1"
116     
117   si usa il seguente comando
118   
119         inductive A : Type ≝
120         | Plus : A → A → A    
121         | Times : A → A → A   
122         | Zero : A
123         | One : A
124         .
125      
126 La ratio è che `Plus` prende due argomenti di tipo `A` per darmi un `A`,
127 mentre `Zero` non prende nessun argomento per darmi un `A`. Al posto di usare
128 operatori infissi `(0 + 0)` la definizione crea operatori prefissi (funzioni).
129 Quindi `(0+0)` si scriverà come `(Plus Zero Zero)`.
130
131 DOCEND*)
132
133 (* ATTENZIONE
134    ==========
135    
136    Non modificare le seguenti tre righe 
137 *)
138 include "nat/minus.ma".
139 definition max : nat → nat → nat ≝ λa,b:nat.let rec max n m on n ≝ match n with [ O ⇒ b | S n ⇒ match m with [ O ⇒ a | S m ⇒ max n m]] in max a b.
140 definition min : nat → nat → nat ≝ λa,b:nat.let rec min n m on n ≝ match n with [ O ⇒ a | S n ⇒ match m with [ O ⇒ b | S m ⇒ min n m]] in min a b.
141
142
143 (* Esercizio 1 
144    ===========
145    
146    Definire il linguaggio delle formule riempiendo gli spazi 
147 *)
148 inductive Formula : Type ≝
149 | FBot: Formula
150 | FTop: (*BEGIN*)Formula(*END*)
151 | FAtom: nat → Formula (* usiamo i naturali al posto delle lettere *)
152 | FAnd: Formula → Formula → Formula
153 | FOr: (*BEGIN*)Formula → Formula → Formula(*END*)
154 | FImpl: (*BEGIN*)Formula → Formula → Formula(*END*)
155 | FNot: (*BEGIN*)Formula → Formula(*END*)
156 .
157
158
159 (* Esercizio 2 
160    ===========
161
162    Data la funzione di valutazione per gli atomi `v`, definire la 
163    funzione `sem` per una generica formula `F` che vi associa la semantica
164    (o denotazione) 
165 *)
166 let rec sem (v: nat → nat) (F: Formula) on F ≝
167  match F with
168   [ FBot ⇒ 0
169   | FTop ⇒ (*BEGIN*)1(*END*)
170   (*BEGIN*)
171   | FAtom n ⇒ v n
172   (*END*)
173   | FAnd F1 F2 ⇒ (*BEGIN*)min (sem v F1) (sem v F2)(*END*)
174   (*BEGIN*)
175   | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
176   | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
177   (*END*)
178   | FNot F1 ⇒ 1 - (sem v F1)
179   ]
180 .
181
182 (* NOTA
183    ====
184    
185    I comandi che seguono definiscono la seguente notazione:
186
187    if e then risultato1 else risultato2
188    
189    Questa notazione permette di valutare l'espressione `e`. Se questa
190    è vera restituisce `risultato1`, altrimenti restituisce `risultato2`.
191    
192    Un esempio di espressione è `eqb n m`, che confronta i due numeri naturali
193    `n` ed `m`. 
194    
195    * [[ formula ]]v
196    
197    Questa notazione utilizza la funzione `sem` precedentemente definita, in 
198    particolare `[[ f ]]v` è una abbreviazione per `sem v f`.
199
200
201    ATTENZIONE
202    ==========
203    
204    Non modificare le linee seguenti 
205 *)
206 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
207 notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
208 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
209 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
210 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
211 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
212 notation > "[[ term 19 a ]] term 90 v" non associative with precedence 90 for @{ sem $v $a }.
213 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
214
215
216 (* Test 1
217    ======
218    
219    Viene fornita una funzione di valutazione di esempio chiamata `v1101`. 
220    Tale funzione associa agli atomi 0, 1 e 3 un valore pari a 1,
221    invece a 2,4,5,6... un valore pari a 0. 
222    
223    Viene fornita una formula di esempio chiamata `esempio1` che rappresenta
224    la formula 
225     
226        D => (C ∨ (B ∧ A))
227        
228    Dove A è rappresentato con l'atomo 0, B con l'atomo 1, ...
229    
230    Tale formula è valida per la funzione di valutazione `v1101`. 
231    
232    Il comando `eval normalize [[ esempio1 ]]v1101` permette di calcolare
233    la funzione `sem` che avete appena definito. Tale funzione deve 
234    computare a 1 (verrà mostrata una finestra col risultato).
235    Se così non fosse significa che avete commesso un errore nella 
236    definizione di `sem` e prima di continuare è necessario che la sistemiate.   
237 *)
238 definition v1101 ≝ λx.
239       if eqb x 0 then 1  (* FAtom 0 ↦ 1 *)
240  else if eqb x 1 then 1  (* FAtom 1 ↦ 1 *)
241  else if eqb x 2 then 0  (* FAtom 2 ↦ 0 *)
242  else if eqb x 3 then 1  (* FAtom 3 ↦ 1 *)
243  else                 0. (* FAtom _ ↦ 0 *) 
244
245
246 definition esempio1 ≝ 
247   (FImpl (FNot (FAtom 3)) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))).
248
249 (* Decommenta ed esegui. *)
250
251 (* eval normalize on [[ esempio1 ]]v1101. *)
252
253
254 (* Esercizio 3
255    ===========
256    
257    Definire la funzione di sostituzione di una formula `G` al posto
258    degli atomi uguali a `x` in una formula `F`. 
259 *)
260 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
261  match F with
262   [ FBot ⇒ FBot
263   | FTop ⇒ (*BEGIN*)FTop(*END*)
264   | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else ((*BEGIN*)FAtom n(*END*))
265   (*BEGIN*)
266   | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
267   | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
268   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
269   (*END*)
270   | FNot F ⇒ FNot (subst x G F)
271   ].
272
273
274 (* NOTA
275    ====
276    
277    I comandi che seguono definiscono la seguente notazione:
278
279   * F [ G / x ]
280   
281   Questa notazione utilizza la funzione `subst` appena definita, in particolare
282   la scrittura `F [ G /x ]` è una abbreviazione per `subst x G F`. 
283   
284   * F ≡ G
285   
286   Questa notazione è una abbreviazione per `∀v.[[ f ]]v = [[ g ]]v`. 
287   Asserisce che for ogni funzione di valutazione `v`, la semantica di `f`
288   in `v` è uguale alla semantica di `g` in `v`.
289
290
291   ATTENZIONE
292   ==========
293   
294   Non modificare le linee seguenti 
295 *)
296 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
297 notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
298 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
299 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]v = [[ F2 ]]v.
300 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
301 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
302 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
303
304 (* Test 2
305    ======
306    
307    Viene fornita una formula di esempio `esempio2`,
308    e una formula `esempio3` che rimpiazzerà gli atomi
309    `FAtom 2` di `esempio2`.
310    
311    Il risultato atteso è la formula:
312    
313         FAnd (FImpl (FOr (FAtom O) (FAtom 1)) (FAtom 1)) 
314              (FOr (FAtom O) (FAtom 1))
315    
316 *)
317
318 definition esempio2 ≝ (FAnd (FImpl (FAtom 2) (FAtom 1)) (FAtom 2)). 
319    
320 definition esempio3 ≝ (FOr (FAtom 0) (FAtom 1)).
321
322 (* Decommenta ed esegui *)
323
324 (* eval normalize on (esempio2 [ esempio3 / 2]). *)
325
326 (*DOCBEGIN
327    
328 Il linguaggio di dimostrazione di Matita
329 ========================================
330
331 L'ultimo esercizio richiede di scrivere una dimostrazione. Tale dimostrazione
332 deve essere scritta utilizzando il linguaggio di dimostrazione di Matita.
333 Tale linguaggio è composto dai seguenti comandi:
334
335 * `assume nome : tipo`
336
337   Quando si deve dimostrare un tesi come `∀F : Formula.P`, il comando
338   `assume F : Formula` fissa una generica `Formula` `F` e la tesi
339   diventa `P` dove `F` è fissata. 
340
341 * `suppose P (nome)`
342
343   Quando si deve dimostrare una tesi come `P → Q`, il comando
344   `suppose P (Ipotesi1)` da il nome `Ipotesi1` a `P` e cambia la tesi
345   `Q`, che ora può essere dimostrata facendo riferimento all'assunzione 
346   `P` tramite il nome `Ipotesi1`. 
347
348 * `we procede by induction on F to prove Q`
349
350   Se `F` è il nome di una (ad esempio) `Formula` precedentemente
351   assunta tramite il comando `assume`, inizia una prova per induzione su `F`.  
352
353 * `case name`
354
355   Nelle prove per induzione o per casi, ogni caso deve iniziare con il
356   comando `case nome`, ad esempio se si procede per induzione di una
357   formula uno dei casi sarà quello in cui la formula è `⊥`, si deve quindi
358   iniziare la sotto dimostrazione per tale caso con `case ⊥`. 
359
360 * `we procede by cases on x to prove Q`
361
362   Analogo a `we procede by induction on F to prove Q`
363
364 * `by induction hypothesis we know P (name)`
365
366   Nei casi non base di una prova per induzione sono disponibili delle ipotesi
367   induttive, quindi la tesi è della forma `P → Q`, ed è possibile 
368   dare un nome a `P` e procedere a dimostrare `Q`. Simile a `suppose`. 
369
370 * `the thesis becomes P` 
371
372   Permette di modificare la tesi, utilizzando le definizioni (eventualmente 
373   ricorsive) che vi compaiono. Ad esempio se la tesi fosse `min 3 5 = max 1 3`
374   si potrebbe usare il comando `the thesis becomes (3 = max 1 3)` in quanto
375   per definizione di minimo, il minimo tra `3` e `5` è `3`. 
376
377 * `by name1 we proved P (name2)`
378
379   Permette di ottenere una nuova ipotesi `P` chiamandola `name2` utilizzando 
380   l'ipotesi `name1`. 
381
382 * `conclude (P) = (Q) by name`
383
384   Quando la tesi è della forma `P = Q`, si possono utilizzare delle ipotesi
385   della forma `A = B` riscrivendo `A` in `B` (o viceversa) in `P`. Per esempio
386   se la tesi fosse `sin π + 3 = 7 - 4` e si avesse una ipotesi `sin π = 0` dal
387   nome `H`, si potrebbe usare il comando `conclude (sin π + 3) = (0 + 3) by H`
388   per cambiare la conclusione in `0 + 3 = 7 - 4`.
389
390 * `= (P) by name`
391
392   Da utilizzare in seguito a un comando `conclude` per riscrivere con altre
393   ipotesi. 
394
395 * `done`
396
397   Termina un caso della dimostrazione, è possibile utilizzarlo quando la tesi
398   è della forma `t = t`, ad esempio `0 = 0` oppure `v x = v x`.
399       
400 DOCEND*)
401
402 (* Esercizio 4
403    ===========
404    
405    Dimostra il teorema di sostituzione visto a lezione
406 *)
407 theorem sostituzione: ∀G1,G2,F,x. G1 ≡ G2 → F[G1/x] ≡ F[G2/x].
408 assume G1 : Formula.
409 assume G2 : Formula.
410 (*BEGIN*)
411 assume F : Formula.
412 assume x : ℕ.
413 (*END*)
414 suppose (G1 ≡ G2) (H).
415 we proceed by induction on F to prove (F[ G1/x ] ≡ F[ G2/x ]). 
416 case FBot.
417   the thesis becomes (FBot[ G1/x ] ≡ FBot[ G2/x ]).
418   the thesis becomes (FBot ≡ FBot[ G2/x ]).
419   the thesis becomes (FBot ≡ FBot).
420   the thesis becomes (∀v.[[FBot]]v = [[FBot]]v).
421   assume v : (ℕ → ℕ).
422   the thesis becomes (0 = [[FBot]]v).
423   the thesis becomes (0 = 0).
424   done.  
425 case FTop.
426   (*BEGIN*)
427   the thesis becomes (FTop[ G1/x ] ≡ FTop[ G2/x ]).
428   the thesis becomes (FTop ≡ FTop).
429   the thesis becomes (∀v. [[FTop]]v = [[FTop]]v).
430   assume v : (ℕ → ℕ).
431   the thesis becomes (1 = 1).
432   (*END*)
433   done.
434 case FAtom.
435   assume n : ℕ.
436   the thesis becomes ((FAtom n)[ G1/x ] ≡ (FAtom n)[ G2/x ]).
437   the thesis becomes 
438     (if eqb n x then G1 else (FAtom n) ≡ (FAtom n)[ G2/x ]).    
439   the thesis becomes
440     (if eqb n x then G1 else (FAtom n) ≡
441      if eqb n x then G2 else (FAtom n)).
442   we proceed by cases on (eqb n x) to prove 
443     (if eqb n x then G1 else (FAtom n) ≡
444      if eqb n x then G2 else (FAtom n)).
445   case true.
446     the thesis becomes (G1 ≡ G2).
447     by H done.
448   case false.
449     (*BEGIN*)
450     the thesis becomes (FAtom n ≡ FAtom n).
451     the thesis becomes (∀v. [[FAtom n]]v = [[FAtom n]]v).
452     assume v : (ℕ → ℕ).
453     the thesis becomes (v n = v n).
454     (*END*)
455     done.
456 case FAnd.
457   assume F1 : Formula.
458   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).    
459   assume F2 : Formula.
460   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).    
461   the thesis becomes 
462     (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]v = [[ (FAnd F1 F2)[ G2/x ] ]]v).
463   assume v : (ℕ → ℕ). 
464   the thesis becomes 
465     (min ([[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v) = 
466      min ([[ F1[ G2/x ] ]]v) ([[ F2[ G2/x ] ]]v)).
467   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]v1 = [[ F1[ G2/x ] ]]v1) (IH11).
468   by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]v2 = [[ F2[ G2/x ] ]]v2) (IH22).
469   by IH11 we proved ([[ F1[ G1/x ] ]]v = [[ F1[ G2/x ] ]]v) (IH111).
470   by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]v = [[ F2[ G2/x ] ]]v) (IH222).
471   conclude 
472       (min ([[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v)) 
473     = (min ([[ F1[ G2/x ] ]]v) ([[ F2[ G1/x ] ]]v)) by IH111.
474     = (min ([[(F1[ G2/x ])]]v) ([[(F2[ G2/x ])]]v)) by (*BEGIN*)IH222(*END*).
475   (*END*)
476   done.
477 case FOr.
478   (*BEGIN*) 
479   assume F1 : Formula.
480   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).    
481   assume F2 : Formula.
482   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).    
483   the thesis becomes 
484     (∀v.[[ (FOr F1 F2)[ G1/x ] ]]v = [[ (FOr F1 F2)[ G2/x ] ]]v).
485   assume v : (ℕ → ℕ). 
486   the thesis becomes 
487     (max ([[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v) = 
488      max ([[ F1[ G2/x ] ]]v) ([[ F2[ G2/x ] ]]v)).
489   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]v1 = [[ F1[ G2/x ] ]]v1) (IH11).
490   by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]v2 = [[ F2[ G2/x ] ]]v2) (IH22).
491   by IH11 we proved ([[ F1[ G1/x ] ]]v = [[ F1[ G2/x ] ]]v) (IH111).
492   by IH22 we proved ([[ F2[ G1/x ] ]]v = [[ F2[ G2/x ] ]]v) (IH222).
493   conclude 
494       (max ([[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v)) 
495     = (max ([[ F1[ G2/x ] ]]v) ([[ F2[ G1/x ] ]]v)) by IH111.
496     = (max ([[(F1[ G2/x ])]]v) ([[(F2[ G2/x ])]]v)) by IH222.
497   (*END*)
498   done.
499 case FImpl.
500   (*BEGIN*)
501   assume F1 : Formula.
502   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
503   assume F2 : Formula.
504   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
505   the thesis becomes 
506     (∀v.max (1 - [[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v) =
507         max (1 - [[ F1[ G2/x ] ]]v) ([[ F2[ G2/x ] ]]v)).
508   assume v : (ℕ → ℕ).       
509   by IH1 we proved ([[ F1[ G1/x ] ]]v = [[ F1[ G2/x ] ]]v) (IH11).
510   by IH2 we proved ([[ F2[ G1/x ] ]]v = [[ F2[ G2/x ] ]]v) (IH22).
511   conclude 
512       (max (1-[[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v))
513     = (max (1-[[ F1[ G2/x ] ]]v) ([[ F2[ G1/x ] ]]v)) by IH11.  
514     = (max (1-[[ F1[ G2/x ] ]]v) ([[ F2[ G2/x ] ]]v)) by IH22.
515   done. 
516 case FNot.
517   (*BEGIN*)
518   assume F1 : Formula.
519   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH).   
520   the thesis becomes (FNot (F1[ G1/x ]) ≡ FNot (F1[ G2/x ])).
521   the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]v = [[FNot (F1[ G2/x ])]]v).
522   assume v : (ℕ → ℕ).
523   the thesis becomes (1 - [[F1[ G1/x ]]]v = [[FNot (F1[ G2/x ])]]v).
524   the thesis becomes (1 - [[ F1[ G1/x ] ]]v = 1 - [[ F1[ G2/x ] ]]v).
525   by IH we proved (∀v1.[[ F1[  G1/x ] ]]v1 = [[ F1[ G2/x ] ]]v1) (IH1).
526   by IH1 we proved ([[ F1[ G1/x ] ]]v = [[ F1[ G2/x ] ]]v) (IH2).
527   conclude 
528       (1-[[ F1[ G1/x ] ]]v) 
529     = (1-[[ F1[ G2/x ] ]]v) by IH2.
530   (*END*)
531   done.
532 qed.
533     
534 (* Questionario
535
536    Compilare mettendo una X nella risposta scelta.
537
538    1) Pensi che sia utile l'integrazione del corso con una attività di 
539       laboratorio?
540    
541       [ ] per niente        [ ] poco     [ ] molto       
542      
543      
544    2) Pensi che gli esercizi proposti ti siano stati utili a capire meglio
545       quanto visto a lezione?
546    
547       [ ] per niente        [ ] poco     [ ] molto       
548
549
550    3) Gli esercizi erano
551     
552       [ ] troppo facili     [ ] alla tua portata      [ ] impossibili       
553
554      
555    4) Il tempo a disposizione è stato     
556    
557       [ ] poco              [ ] giusto          [ ] troppo       
558
559      
560    5) Cose che miglioreresti nel software Matita
561      
562       .........
563
564       
565    6) Suggerimenti sullo svolgimento delle attività in laboratorio
566    
567         .........
568
569    
570 *) 
571    
572