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 * 'suppose P (nome)'
 300 * 'by induction hypothesis we know P (name)'
 301 * 'we procede by induction on x to prove Q'
 302 * 'we procede by cases on x to prove Q'
 303 * 'case name'
 304 * 'the thesis becomes P'
 305 * 'by name we proved P (name)'
 306 * 'conclude (P) = (Q) by name'
 307 * '= (P) by name'
 308 * 'done'
 309
 310 DOCEND*)
 311
 312 (* Esercizio 4
 313    ===========
 314
 315    Dimostra il teorema di sostituzione visto a lezione
 316 *)
 317 theorem sostituzione: ∀G1,G2,F,x. G1 ≡ G2 → F[G1/x] ≡ F[G2/x].
 318 assume G1 : Formula.
 319 assume G2 : Formula.
 320 (*BEGIN*)
 321 assume F : Formula.
 322 assume x : ℕ.
 323 (*END*)
 324 suppose (G1 ≡ G2) (H).
 325 we proceed by induction on F to prove (F[ G1/x ] ≡ F[ G2/x ]).
 326 case FBot.
 327   the thesis becomes (FBot[ G1/x ] ≡ FBot[ G2/x ]).
 328   the thesis becomes (FBot ≡ FBot[ G2/x ]).
 329   the thesis becomes (FBot ≡ FBot).
 330   the thesis becomes (∀v.[[FBot]]_v = [[FBot]]_v).
 331   assume v : (ℕ → ℕ).
 332   the thesis becomes (0 = [[FBot]]_v).
 333   the thesis becomes (0 = 0).
 334   done.
 335 case FTop.
 336   (*BEGIN*)
 337   the thesis becomes (FTop[ G1/x ] ≡ FTop[ G2/x ]).
 338   the thesis becomes (FTop ≡ FTop).
 339   the thesis becomes (∀v. [[FTop]]_v = [[FTop]]_v).
 340   assume v : (ℕ → ℕ).
 341   the thesis becomes (1 = 1).
 342   (*END*)
 343   done.
 344 case FAtom.
 345   assume n : ℕ.
 346   the thesis becomes ((FAtom n)[ G1/x ] ≡ (FAtom n)[ G2/x ]).
 347   the thesis becomes
 348     (if eqb n x then G1 else (FAtom n) ≡ (FAtom n)[ G2/x ]).
 349   the thesis becomes
 350     (if eqb n x then G1 else (FAtom n) ≡
 351      if eqb n x then G2 else (FAtom n)).
 352   we proceed by cases on (eqb n x) to prove
 353     (if eqb n x then G1 else (FAtom n) ≡
 354      if eqb n x then G2 else (FAtom n)).
 355   case true.
 356     the thesis becomes (G1 ≡ G2).
 357     done.
 358   case false.
 359     (*BEGIN*)
 360     the thesis becomes (FAtom n ≡ FAtom n).
 361     the thesis becomes (∀v. [[FAtom n]]_v = [[FAtom n]]_v).
 362     assume v : (ℕ → ℕ).
 363     the thesis becomes (v n = v n).
 364     (*END*)
 365     done.
 366 case FAnd.
 367   assume F1 : Formula.
 368   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 369   assume F2 : Formula.
 370   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 371   the thesis becomes
 372     (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]_v = [[ (FAnd F1 F2)[ G2/x ] ]]_v).
 373   assume v : (ℕ → ℕ).
 374   the thesis becomes
 375     (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 376      min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 377   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 378   by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 379   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 380   by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 381   conclude
 382       (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 383     = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 384     = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*).
 385   (*END*)
 386   done.
 387 case FOr.
 388   (*BEGIN*)
 389   assume F1 : Formula.
 390   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 391   assume F2 : Formula.
 392   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 393   the thesis becomes
 394     (∀v.[[ (FOr F1 F2)[ G1/x ] ]]_v = [[ (FOr F1 F2)[ G2/x ] ]]_v).
 395   assume v : (ℕ → ℕ).
 396   the thesis becomes
 397     (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 398      max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 399   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 400   by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 401   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 402   by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 403   conclude
 404       (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 405     = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 406     = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111.
 407   (*END*)
 408   done.
 409 case FImpl.
 410   (*BEGIN*)
 411   assume F1 : Formula.
 412   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 413   assume F2 : Formula.
 414   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 415   the thesis becomes
 416     (∀v.max (1 - [[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 417         max (1 - [[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 418   assume v : (ℕ → ℕ).
 419   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH11).
 420   by IH2 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH22).
 421   conclude
 422       (max (1-[[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 423     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH11.
 424     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)) by IH22.
 425   done.
 426 case FNot.
 427   (*BEGIN*)
 428   assume F1 : Formula.
 429   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH).
 430   the thesis becomes (FNot (F1[ G1/x ]) ≡ FNot (F1[ G2/x ])).
 431   the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]_v = [[FNot (F1[ G2/x ])]]_v).
 432   assume v : (ℕ → ℕ).
 433   the thesis becomes (1 - [[F1[ G1/x ]]]_v = [[FNot (F1[ G2/x ])]]_v).
 434   the thesis becomes (1 - [[ F1[ G1/x ] ]]_v = 1 - [[ F1[ G2/x ] ]]_v).
 435   by IH we proved (∀v1.[[ F1[  G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH1).
 436   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH2).
 437   conclude
 438       (1-[[ F1[ G1/x ] ]]_v)
 439     = (1-[[ F1[ G2/x ] ]]_v) by IH2.
 440   (*END*)
 441   done.
 442 qed.
 443
 444 (* Questionario
 445
 446    Compilare mettendo una X nella risposta scelta.
 447
 448    1) Pensi che sia utile l'integrazione del corso con una attività di
 449       laboratorio?
 450
 451       [ ] per niente        [ ] poco     [ ] molto
 452
 453
 454    2) Pensi che gli esercizi proposti ti siano stati utili a capire meglio
 455       quanto visto a lezione?
 456
 457       [ ] per niente        [ ] poco     [ ] molto
 458
 459
 460    3) Gli esercizi erano
 461
 462       [ ] troppo facili     [ ] alla tua portata      [ ] impossibili
 463
 464
 465    4) Il tempo a disposizione è stato
 466
 467       [ ] poco              [ ] giusto          [ ] troppo
 468
 469
 470    5) Cose che miglioreresti nel software Matita
 471
 472       .........
 473
 474
 475    6) Suggerimenti sullo svolgimento delle attività in laboratorio
 476
 477         .........
 478
 479
 480 *)
 481
 482