helm/software/matita/library/didactic/exercises/substitution.ma

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