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

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