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