helm/software/matita/contribs/didactic/induction.ma

   1 (* Esercitazione di logica 22/10/2008. *)
   2
   3 (* Nota per gli studenti
   4    =====================
   5
   6    * La lezione del pomeriggio con il Prof. Sacerdoti si terrà in aula
   7      Pinkerle e non Cremona.
   8
   9    * Un piccolo manuale sul software Matita è disponibile al seguente URL:
  10
  11        http://mowgli.cs.unibo.it/~tassi/exercise-induction.ma.html
  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 eval normalize on [[ esempio1 ]]_v1101.
 250
 251
 252 (* Esercizio 3
 253    ===========
 254
 255    Definire la funzione di sostituzione di una formula `G` al posto
 256    degli atomi uguali a `x` in una formula `F`.
 257 *)
 258 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
 259  match F with
 260   [ FBot ⇒ FBot
 261   | FTop ⇒ (*BEGIN*)FTop(*END*)
 262   | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else ((*BEGIN*)FAtom n(*END*))
 263   (*BEGIN*)
 264   | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
 265   | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
 266   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
 267   (*END*)
 268   | FNot F ⇒ FNot (subst x G F)
 269   ].
 270
 271
 272 (* NOTA
 273    ====
 274
 275    I comandi che seguono definiscono la seguente notazione:
 276
 277   * F [ G / x ]
 278
 279   Questa notazione utilizza la funzione `subst` appena definita, in particolare
 280   la scrittura `F [ G /x ]` è una abbreviazione per `subst x G F`.
 281
 282   * F ≡ G
 283
 284   Questa notazione è una abbreviazione per `∀v.[[ f ]]_v = [[ g ]]_v`.
 285   Asserisce che for ogni funzione di valutazione `v`, la semantica di `f`
 286   in `v` è uguale alla semantica di `g` in `v`.
 287
 288
 289   ATTENZIONE
 290   ==========
 291
 292   Non modificare le linee seguenti
 293 *)
 294 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
 295 notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
 296 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
 297 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
 298 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 299 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 300 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 301
 302 (* Test 2
 303    ======
 304
 305    Viene fornita una formula di esempio `esempio2`,
 306    e una formula `esempio3` che rimpiazzerà gli atomi
 307    `FAtom 2` di `esempio2`.
 308
 309    Il risultato atteso è la formula:
 310
 311         FAnd (FImpl (FOr (FAtom O) (FAtom 1)) (FAtom 1))
 312              (FOr (FAtom O) (FAtom 1))
 313
 314 *)
 315
 316 definition esempio2 ≝ (FAnd (FImpl (FAtom 2) (FAtom 1)) (FAtom 2)).
 317
 318 definition esempio3 ≝ (FOr (FAtom 0) (FAtom 1)).
 319
 320 eval normalize on (esempio2 [ esempio3 / 2]).
 321
 322 (*DOCBEGIN
 323
 324 Il linguaggio di dimostrazione di Matita
 325 ========================================
 326
 327 L'ultimo esercizio richiede di scrivere una dimostrazione. Tale dimostrazione
 328 deve essere scritta utilizzando il linguaggio di dimostrazione di Matita.
 329 Tale linguaggio è composto dai seguenti comandi:
 330
 331 * `assume nome : tipo`
 332
 333   Quando si deve dimostrare un tesi come `∀F : Formula.P`, il comando
 334   `assume F : Formula` fissa una generica `Formula` `F` e la tesi
 335   diventa `P` dove `F` è fissata.
 336
 337 * `suppose P (nome)`
 338
 339   Quando si deve dimostrare una tesi come `P → Q`, il comando
 340   `suppose P (Ipotesi1)` da il nome `Ipotesi1` a `P` e cambia la tesi
 341   `Q`, che ora può essere dimostrata facendo riferimento all'assunzione
 342   `P` tramite il nome `Ipotesi1`.
 343
 344 * `we procede by induction on F to prove Q`
 345
 346   Se `F` è il nome di una (ad esempio) `Formula` precedentemente
 347   assunta tramite il comando `assume`, inizia una prova per induzione su `F`.
 348
 349 * `case name`
 350
 351   Nelle prove per induzione o per casi, ogni caso deve iniziare con il
 352   comando `case nome`, ad esempio se si procede per induzione di una
 353   formula uno dei casi sarà quello in cui la formula è `⊥`, si deve quindi
 354   iniziare la sotto dimostrazione per tale caso con `case ⊥`.
 355
 356 * `we procede by cases on x to prove Q`
 357
 358   Analogo a `we procede by induction on F to prove Q`
 359
 360 * `by induction hypothesis we know P (name)`
 361
 362   Nei casi non base di una prova per induzione sono disponibili delle ipotesi
 363   induttive, quindi la tesi è della forma `P → Q`, ed è possibile
 364   dare un nome a `P` e procedere a dimostrare `Q`. Simile a `suppose`.
 365
 366 * `the thesis becomes P`
 367
 368   Permette di modificare la tesi, utilizzando le definizioni (eventualmente
 369   ricorsive) che vi compaiono. Ad esempio se la tesi fosse `min 3 5 = max 1 3`
 370   si potrebbe usare il comando `the thesis becomes (3 = max 1 3)` in quanto
 371   per definizione di minimo, il minimo tra `3` e `5` è `3`.
 372
 373 * `by name1 we proved P (name2)`
 374
 375   Permette di ottenere una nuova ipotesi `P` chiamandola `name2` utilizzando
 376   l'ipotesi `name1`.
 377
 378 * `conclude (P) = (Q) by name`
 379
 380   Quando la tesi è della forma `P = Q`, si possono utilizzare delle ipotesi
 381   della forma `A = B` riscrivendo `A` in `B` (o viceversa) in `P`. Per esempio
 382   se la tesi fosse `sin π + 3 = 7 - 4` e si avesse una ipotesi `sin π = 0` dal
 383   nome `H`, si potrebbe usare il comando `conclude (sin π + 3) = (0 + 3) by H`
 384   per cambiare la conclusione in `0 + 3 = 7 - 4`.
 385
 386 * `= (P) by name`
 387
 388   Da utilizzare in seguito a un comando `conclude` per riscrivere con altre
 389   ipotesi.
 390
 391 * `done`
 392
 393   Termina un caso della dimostrazione, è possibile utilizzarlo quando la tesi
 394   è della forma `t = t`, ad esempio `0 = 0` oppure `v x = v x`.
 395
 396 DOCEND*)
 397
 398 (* Esercizio 4
 399    ===========
 400
 401    Dimostra il teorema di sostituzione visto a lezione
 402 *)
 403 theorem sostituzione: ∀G1,G2,F,x. G1 ≡ G2 → F[G1/x] ≡ F[G2/x].
 404 assume G1 : Formula.
 405 assume G2 : Formula.
 406 (*BEGIN*)
 407 assume F : Formula.
 408 assume x : ℕ.
 409 (*END*)
 410 suppose (G1 ≡ G2) (H).
 411 we proceed by induction on F to prove (F[ G1/x ] ≡ F[ G2/x ]).
 412 case FBot.
 413   the thesis becomes (FBot[ G1/x ] ≡ FBot[ G2/x ]).
 414   the thesis becomes (FBot ≡ FBot[ G2/x ]).
 415   the thesis becomes (FBot ≡ FBot).
 416   the thesis becomes (∀v.[[FBot]]_v = [[FBot]]_v).
 417   assume v : (ℕ → ℕ).
 418   the thesis becomes (0 = [[FBot]]_v).
 419   the thesis becomes (0 = 0).
 420   done.
 421 case FTop.
 422   (*BEGIN*)
 423   the thesis becomes (FTop[ G1/x ] ≡ FTop[ G2/x ]).
 424   the thesis becomes (FTop ≡ FTop).
 425   the thesis becomes (∀v. [[FTop]]_v = [[FTop]]_v).
 426   assume v : (ℕ → ℕ).
 427   the thesis becomes (1 = 1).
 428   (*END*)
 429   done.
 430 case FAtom.
 431   assume n : ℕ.
 432   the thesis becomes ((FAtom n)[ G1/x ] ≡ (FAtom n)[ G2/x ]).
 433   the thesis becomes
 434     (if eqb n x then G1 else (FAtom n) ≡ (FAtom n)[ G2/x ]).
 435   the thesis becomes
 436     (if eqb n x then G1 else (FAtom n) ≡
 437      if eqb n x then G2 else (FAtom n)).
 438   we proceed by cases on (eqb n x) to prove
 439     (if eqb n x then G1 else (FAtom n) ≡
 440      if eqb n x then G2 else (FAtom n)).
 441   case true.
 442     the thesis becomes (G1 ≡ G2).
 443     done.
 444   case false.
 445     (*BEGIN*)
 446     the thesis becomes (FAtom n ≡ FAtom n).
 447     the thesis becomes (∀v. [[FAtom n]]_v = [[FAtom n]]_v).
 448     assume v : (ℕ → ℕ).
 449     the thesis becomes (v n = v n).
 450     (*END*)
 451     done.
 452 case FAnd.
 453   assume F1 : Formula.
 454   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 455   assume F2 : Formula.
 456   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 457   the thesis becomes
 458     (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]_v = [[ (FAnd F1 F2)[ G2/x ] ]]_v).
 459   assume v : (ℕ → ℕ).
 460   the thesis becomes
 461     (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 462      min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 463   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 464   by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 465   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 466   by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 467   conclude
 468       (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 469     = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 470     = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*).
 471   (*END*)
 472   done.
 473 case FOr.
 474   (*BEGIN*)
 475   assume F1 : Formula.
 476   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 477   assume F2 : Formula.
 478   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 479   the thesis becomes
 480     (∀v.[[ (FOr F1 F2)[ G1/x ] ]]_v = [[ (FOr F1 F2)[ G2/x ] ]]_v).
 481   assume v : (ℕ → ℕ).
 482   the thesis becomes
 483     (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 484      max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 485   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 486   by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 487   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 488   by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 489   conclude
 490       (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 491     = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 492     = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111.
 493   (*END*)
 494   done.
 495 case FImpl.
 496   (*BEGIN*)
 497   assume F1 : Formula.
 498   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 499   assume F2 : Formula.
 500   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 501   the thesis becomes
 502     (∀v.max (1 - [[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 503         max (1 - [[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 504   assume v : (ℕ → ℕ).
 505   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH11).
 506   by IH2 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH22).
 507   conclude
 508       (max (1-[[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 509     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH11.
 510     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)) by IH22.
 511   done.
 512 case FNot.
 513   (*BEGIN*)
 514   assume F1 : Formula.
 515   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH).
 516   the thesis becomes (FNot (F1[ G1/x ]) ≡ FNot (F1[ G2/x ])).
 517   the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]_v = [[FNot (F1[ G2/x ])]]_v).
 518   assume v : (ℕ → ℕ).
 519   the thesis becomes (1 - [[F1[ G1/x ]]]_v = [[FNot (F1[ G2/x ])]]_v).
 520   the thesis becomes (1 - [[ F1[ G1/x ] ]]_v = 1 - [[ F1[ G2/x ] ]]_v).
 521   by IH we proved (∀v1.[[ F1[  G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH1).
 522   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH2).
 523   conclude
 524       (1-[[ F1[ G1/x ] ]]_v)
 525     = (1-[[ F1[ G2/x ] ]]_v) by IH2.
 526   (*END*)
 527   done.
 528 qed.
 529
 530 (* Questionario
 531
 532    Compilare mettendo una X nella risposta scelta.
 533
 534    1) Pensi che sia utile l'integrazione del corso con una attività di
 535       laboratorio?
 536
 537       [ ] per niente        [ ] poco     [ ] molto
 538
 539
 540    2) Pensi che gli esercizi proposti ti siano stati utili a capire meglio
 541       quanto visto a lezione?
 542
 543       [ ] per niente        [ ] poco     [ ] molto
 544
 545
 546    3) Gli esercizi erano
 547
 548       [ ] troppo facili     [ ] alla tua portata      [ ] impossibili
 549
 550
 551    4) Il tempo a disposizione è stato
 552
 553       [ ] poco              [ ] giusto          [ ] troppo
 554
 555
 556    5) Cose che miglioreresti nel software Matita
 557
 558       .........
 559
 560
 561    6) Suggerimenti sullo svolgimento delle attività in laboratorio
 562
 563         .........
 564
 565
 566 *)
 567
 568