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