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