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  (* 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 = 7 - 4` e si avesse una ipotesi `sin π = 0` dal
 350   nome `H`, si potrebbe usare il comando `conclude (sin π + 3) = (0 + 3) by H`
 351   per cambiare la conclusione in `0 + 3 = 7 - 4`.
 352
 353 * `= (P) by name`
 354
 355   Da utilizzare in seguito a un comando `conclude` per riscrivere con altre
 356   ipotesi.
 357
 358 * `done`
 359
 360   Termina un caso della dimostrazione, è possibile utilizzarlo quando la tesi
 361   è della forma `t = t`, ad esempio `0 = 0` oppure `v x = v x`.
 362
 363 DOCEND*)
 364
 365 (* Esercizio 4
 366    ===========
 367
 368    Dimostra il teorema di sostituzione visto a lezione
 369 *)
 370 theorem sostituzione: ∀G1,G2,F,x. G1 ≡ G2 → F[G1/x] ≡ F[G2/x].
 371 assume G1 : Formula.
 372 assume G2 : Formula.
 373 (*BEGIN*)
 374 assume F : Formula.
 375 assume x : ℕ.
 376 (*END*)
 377 suppose (G1 ≡ G2) (H).
 378 we proceed by induction on F to prove (F[ G1/x ] ≡ F[ G2/x ]).
 379 case FBot.
 380   the thesis becomes (FBot[ G1/x ] ≡ FBot[ G2/x ]).
 381   the thesis becomes (FBot ≡ FBot[ G2/x ]).
 382   the thesis becomes (FBot ≡ FBot).
 383   the thesis becomes (∀v.[[FBot]]_v = [[FBot]]_v).
 384   assume v : (ℕ → ℕ).
 385   the thesis becomes (0 = [[FBot]]_v).
 386   the thesis becomes (0 = 0).
 387   done.
 388 case FTop.
 389   (*BEGIN*)
 390   the thesis becomes (FTop[ G1/x ] ≡ FTop[ G2/x ]).
 391   the thesis becomes (FTop ≡ FTop).
 392   the thesis becomes (∀v. [[FTop]]_v = [[FTop]]_v).
 393   assume v : (ℕ → ℕ).
 394   the thesis becomes (1 = 1).
 395   (*END*)
 396   done.
 397 case FAtom.
 398   assume n : ℕ.
 399   the thesis becomes ((FAtom n)[ G1/x ] ≡ (FAtom n)[ G2/x ]).
 400   the thesis becomes
 401     (if eqb n x then G1 else (FAtom n) ≡ (FAtom n)[ G2/x ]).
 402   the thesis becomes
 403     (if eqb n x then G1 else (FAtom n) ≡
 404      if eqb n x then G2 else (FAtom n)).
 405   we proceed by cases on (eqb n x) to prove
 406     (if eqb n x then G1 else (FAtom n) ≡
 407      if eqb n x then G2 else (FAtom n)).
 408   case true.
 409     the thesis becomes (G1 ≡ G2).
 410     done.
 411   case false.
 412     (*BEGIN*)
 413     the thesis becomes (FAtom n ≡ FAtom n).
 414     the thesis becomes (∀v. [[FAtom n]]_v = [[FAtom n]]_v).
 415     assume v : (ℕ → ℕ).
 416     the thesis becomes (v n = v n).
 417     (*END*)
 418     done.
 419 case FAnd.
 420   assume F1 : Formula.
 421   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 422   assume F2 : Formula.
 423   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 424   the thesis becomes
 425     (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]_v = [[ (FAnd F1 F2)[ G2/x ] ]]_v).
 426   assume v : (ℕ → ℕ).
 427   the thesis becomes
 428     (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 429      min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 430   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 431   by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 432   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 433   by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 434   conclude
 435       (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 436     = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 437     = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*).
 438   (*END*)
 439   done.
 440 case FOr.
 441   (*BEGIN*)
 442   assume F1 : Formula.
 443   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 444   assume F2 : Formula.
 445   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 446   the thesis becomes
 447     (∀v.[[ (FOr F1 F2)[ G1/x ] ]]_v = [[ (FOr F1 F2)[ G2/x ] ]]_v).
 448   assume v : (ℕ → ℕ).
 449   the thesis becomes
 450     (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 451      max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 452   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 453   by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 454   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 455   by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 456   conclude
 457       (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 458     = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 459     = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111.
 460   (*END*)
 461   done.
 462 case FImpl.
 463   (*BEGIN*)
 464   assume F1 : Formula.
 465   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 466   assume F2 : Formula.
 467   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 468   the thesis becomes
 469     (∀v.max (1 - [[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 470         max (1 - [[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 471   assume v : (ℕ → ℕ).
 472   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH11).
 473   by IH2 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH22).
 474   conclude
 475       (max (1-[[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 476     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH11.
 477     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)) by IH22.
 478   done.
 479 case FNot.
 480   (*BEGIN*)
 481   assume F1 : Formula.
 482   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH).
 483   the thesis becomes (FNot (F1[ G1/x ]) ≡ FNot (F1[ G2/x ])).
 484   the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]_v = [[FNot (F1[ G2/x ])]]_v).
 485   assume v : (ℕ → ℕ).
 486   the thesis becomes (1 - [[F1[ G1/x ]]]_v = [[FNot (F1[ G2/x ])]]_v).
 487   the thesis becomes (1 - [[ F1[ G1/x ] ]]_v = 1 - [[ F1[ G2/x ] ]]_v).
 488   by IH we proved (∀v1.[[ F1[  G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH1).
 489   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH2).
 490   conclude
 491       (1-[[ F1[ G1/x ] ]]_v)
 492     = (1-[[ F1[ G2/x ] ]]_v) by IH2.
 493   (*END*)
 494   done.
 495 qed.
 496
 497 (* Questionario
 498
 499    Compilare mettendo una X nella risposta scelta.
 500
 501    1) Pensi che sia utile l'integrazione del corso con una attività di
 502       laboratorio?
 503
 504       [ ] per niente        [ ] poco     [ ] molto
 505
 506
 507    2) Pensi che gli esercizi proposti ti siano stati utili a capire meglio
 508       quanto visto a lezione?
 509
 510       [ ] per niente        [ ] poco     [ ] molto
 511
 512
 513    3) Gli esercizi erano
 514
 515       [ ] troppo facili     [ ] alla tua portata      [ ] impossibili
 516
 517
 518    4) Il tempo a disposizione è stato
 519
 520       [ ] poco              [ ] giusto          [ ] troppo
 521
 522
 523    5) Cose che miglioreresti nel software Matita
 524
 525       .........
 526
 527
 528    6) Suggerimenti sullo svolgimento delle attività in laboratorio
 529
 530         .........
 531
 532
 533 *)
 534
 535