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