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 DOCEND*)
 116
 117 (* ATTENZIONE
 118    ==========
 119
 120    Non modificare le seguenti tre righe
 121 *)
 122 include "nat/minus.ma".
 123 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.
 124 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.
 125
 126
 127 (* Esercizio 1
 128    ===========
 129
 130    Definire il linguaggio delle formule riempiendo gli spazi
 131 *)
 132 inductive Formula : Type ≝
 133 | FBot: Formula
 134 | FTop: (*BEGIN*)Formula(*END*)
 135 | FAtom: nat → Formula (* usiamo i naturali al posto delle lettere *)
 136 | FAnd: Formula → Formula → Formula
 137 | FOr: (*BEGIN*)Formula → Formula → Formula(*END*)
 138 | FImpl: (*BEGIN*)Formula → Formula → Formula(*END*)
 139 | FNot: (*BEGIN*)Formula → Formula(*END*)
 140 .
 141
 142
 143 (* Esercizio 2
 144    ===========
 145
 146    Data la funzione di valutazione per gli atomi 'v', definire la
 147    funzione 'sem' per una generica formula 'F' che vi associa la semantica
 148    (o denotazione)
 149 *)
 150 let rec sem (v: nat → nat) (F: Formula) on F ≝
 151  match F with
 152   [ FBot ⇒ 0
 153   | FTop ⇒ (*BEGIN*)1(*END*)
 154   (*BEGIN*)
 155   | FAtom n ⇒ v n
 156   (*END*)
 157   | FAnd F1 F2 ⇒ (*BEGIN*)min (sem v F1) (sem v F2)(*END*)
 158   (*BEGIN*)
 159   | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
 160   | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
 161   (*END*)
 162   | FNot F1 ⇒ 1 - (sem v F1)
 163   ]
 164 .
 165
 166 (* NOTA
 167    ====
 168
 169    I comandi che seguono definiscono la seguente notazione:
 170
 171    if e then risultato1 else risultato2
 172
 173    Questa notazione permette di valutare l'espressione 'e'. Se questa
 174    è vera restituisce 'risultato1', altrimenti restituisce 'risultato2'.
 175
 176    Un esempio di espressione è 'eqb n m', che confronta i due numeri naturali
 177    'n' ed 'm'.
 178
 179    * [[ formula ]]_v
 180
 181    Questa notazione utilizza la funzione 'sem' precedentemente definita, in
 182    particolare '[[ f ]]_v' è una abbreviazione per 'sem v f'.
 183
 184
 185    ATTENZIONE
 186    ==========
 187
 188    Non modificare le linee seguenti
 189 *)
 190 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
 191 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 }.
 192 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 }.
 193 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
 194 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 195 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 196 notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
 197 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
 198
 199
 200 (* Test 1
 201    ======
 202
 203    Viene fornita una funzione di valutazione di esempio chiamata 'v1101'.
 204    Tale funzione associa agli atomi 0, 1 e 3 un valore pari a 1,
 205    invece a 2,4,5,6... un valore pari a 0.
 206
 207    Viene fornita una formula di esempio chiamata 'esempio1' che rappresenta
 208    la formula
 209
 210        D => (C ∨ (B ∧ A))
 211
 212    Dove A è rappresentato con l'atomo 0, B con l'atomo 1, ...
 213
 214    Tale formula è valida per la funzione di valutazione 'v1101'.
 215
 216    Il comando 'eval normalize [[ esempio1 ]]_v1101' permette di calcolare
 217    la funzione 'sem' che avete appena definito. Tale funzione deve
 218    computare a 1 (verrà mostrata una finestra col risultato).
 219    Se così non fosse significa che avete commesso un errore nella
 220    definizione di 'sem' e prima di continuare è necessario che la sistemiate.
 221 *)
 222 definition v1101 ≝ λx.
 223       if eqb x 0 then 1  (* Atom 0 ↦ 1 *)
 224  else if eqb x 1 then 1  (* Atom 1 ↦ 1 *)
 225  else if eqb x 2 then 0  (* Atom 2 ↦ 0 *)
 226  else if eqb x 3 then 1  (* Atom 3 ↦ 1 *)
 227  else                 0. (* Atom _ ↦ 0 *)
 228
 229
 230 definition esempio1 ≝ (FImpl (FAtom 3) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))).
 231
 232 (* eval normalize on [[ esempio1 ]]_v1101. *)
 233
 234
 235 (* Esercizio 3
 236    ===========
 237
 238    Definire la funzione di sostituzione di una formula 'G' al posto
 239    degli atomi uguali a 'x' in una formula 'F'.
 240 *)
 241 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
 242  match F with
 243   [ FBot ⇒ FBot
 244   | FTop ⇒ (*BEGIN*)FTop(*END*)
 245   | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else (*BEGIN*)(FAtom n)(*END*)
 246   (*BEGIN*)
 247   | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
 248   | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
 249   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
 250   (*END*)
 251   | FNot F ⇒ FNot (subst x G F)
 252   ].
 253
 254 (* AGGIUNGERE ALCUNI TEST *)
 255
 256
 257 (* NOTA
 258    ====
 259
 260    I comandi che seguono definiscono la seguente notazione:
 261
 262   * F [ G / x ]
 263
 264   Questa notazione utilizza la funzione 'subst' appena definita, in particolare
 265   la scrittura 'F [ G /x ]' è una abbreviazione per 'subst x G F'.
 266
 267   * F ≡ G
 268
 269   Questa notazione è una abbreviazione per '∀v.[[ f ]]_v = [[ g ]]_v'.
 270   Asserisce che for ogni funzione di valutazione 'v', la semantica di 'f'
 271   in 'v' è uguale alla semantica di 'g' in 'v'.
 272
 273
 274   ATTENZIONE
 275   ==========
 276
 277   Non modificare le linee seguenti
 278 *)
 279 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
 280 notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
 281 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
 282 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
 283 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 284 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 285 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 286
 287
 288 (*DOCBEGIN
 289
 290    Il linguaggio di dimostrazione di Matita
 291    ========================================
 292
 293    L'ultimo esercizio richiede di scrivere una dimostrazione. Tale dimostrazione
 294    deve essere scritta utilizzando il linguaggio di dimostrazione di Matita.
 295    Tale linguaggio è composto dai seguenti comandi:
 296
 297    * 'assume nome : tipo'
 298    * 'suppose nome : tipo'
 299    * we procede by induction on x to prove Q'
 300    * the thesis becomes
 301
 302
 303 DOCEND*)
 304
 305 (* Esercizio 4
 306    ===========
 307
 308    Dimostra il teorema di sostituzione visto a lezione
 309 *)
 310 theorem sostituzione: ∀G1,G2,F,x. G1 ≡ G2 → F[G1/x] ≡ F[G2/x].
 311 assume G1 : Formula.
 312 assume G2 : Formula.
 313 (*BEGIN*)
 314 assume F : Formula.
 315 assume x : ℕ.
 316 (*END*)
 317 suppose (G1 ≡ G2) (H).
 318 we proceed by induction on F to prove (F[ G1/x ] ≡ F[ G2/x ]).
 319 case FBot.
 320   the thesis becomes (FBot ≡ FBot[ G2/x ]).
 321   the thesis becomes (FBot ≡ FBot).
 322   the thesis becomes (∀v.[[FBot]]_v = [[FBot]]_v).
 323   assume v : (ℕ → ℕ).
 324   the thesis becomes (0 = [[FBot]]_v).
 325   the thesis becomes (0 = 0).
 326   done.
 327 case FTop.
 328   (*BEGIN*)
 329   the thesis becomes (FTop ≡ FTop).
 330   the thesis becomes (∀v. [[FTop]]_v = [[FTop]]_v).
 331   assume v : (ℕ → ℕ).
 332   the thesis becomes (1 = 1).
 333   (*END*)
 334   done.
 335 case FAtom.
 336   assume n : ℕ.
 337   the thesis becomes
 338     (if eqb n x then G1 else (FAtom n) ≡ (FAtom n)[ G2/x ]).
 339   the thesis becomes
 340     (if eqb n x then G1 else (FAtom n) ≡
 341      if eqb n x then G2 else (FAtom n)).
 342   we proceed by cases on (eqb n x) to prove
 343     (if eqb n x then G1 else (FAtom n) ≡
 344      if eqb n x then G2 else (FAtom n)).
 345   case true.
 346     the thesis becomes (G1 ≡ G2).
 347     done.
 348   case false.
 349     (*BEGIN*)
 350     the thesis becomes (FAtom n ≡ FAtom n).
 351     the thesis becomes (∀v. [[FAtom n]]_v = [[FAtom n]]_v).
 352     assume v : (ℕ → ℕ).
 353     the thesis becomes (v n = v n).
 354     (*END*)
 355     done.
 356 case FAnd.
 357   assume F1 : Formula.
 358   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 359   assume F2 : Formula.
 360   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 361   the thesis becomes
 362     (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]_v = [[ (FAnd F1 F2)[ G2/x ] ]]_v).
 363   assume v : (ℕ → ℕ).
 364   the thesis becomes
 365     (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 366      min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 367   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 368   by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 369   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 370   by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 371   conclude
 372       (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 373     = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 374     = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*).
 375   (*END*)
 376   done.
 377 case FOr.
 378   (*BEGIN*)
 379   assume F1 : Formula.
 380   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 381   assume F2 : Formula.
 382   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 383   the thesis becomes
 384     (∀v.[[ (FOr F1 F2)[ G1/x ] ]]_v = [[ (FOr F1 F2)[ G2/x ] ]]_v).
 385   assume v : (ℕ → ℕ).
 386   the thesis becomes
 387     (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 388      max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 389   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 390   by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 391   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 392   by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 393   conclude
 394       (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 395     = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 396     = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111.
 397   (*END*)
 398   done.
 399 case FImpl.
 400   (*BEGIN*)
 401   assume F1 : Formula.
 402   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 403   assume F2 : Formula.
 404   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 405   the thesis becomes
 406     (∀v.max (1 - [[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 407         max (1 - [[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 408   assume v : (ℕ → ℕ).
 409   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH11).
 410   by IH2 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH22).
 411   conclude
 412       (max (1-[[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 413     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH11.
 414     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)) by IH22.
 415   done.
 416 case FNot.
 417   (*BEGIN*)
 418   assume F1 : Formula.
 419   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH).
 420   the thesis becomes (FNot (F1[ G1/x ]) ≡ FNot (F1[ G2/x ])).
 421   the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]_v = [[FNot (F1[ G2/x ])]]_v).
 422   assume v : (ℕ → ℕ).
 423   the thesis becomes (1 - [[F1[ G1/x ]]]_v = [[FNot (F1[ G2/x ])]]_v).
 424   the thesis becomes (1 - [[ F1[ G1/x ] ]]_v = 1 - [[ F1[ G2/x ] ]]_v).
 425   by IH we proved (∀v1.[[ F1[  G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH1).
 426   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH2).
 427   conclude
 428       (1-[[ F1[ G1/x ] ]]_v)
 429     = (1-[[ F1[ G2/x ] ]]_v) by IH2.
 430   (*END*)
 431   done.
 432 qed.
 433
 434 (* Questionario
 435
 436    Compilare mettendo una X nella risposta scelta.
 437
 438    1) Pensi che sia utile l'integrazione del corso con una attività di
 439       laboratorio?
 440
 441       [ ] per niente        [ ] poco     [ ] molto
 442
 443
 444    2) Pensi che gli esercizi proposti ti siano stati utili a capire meglio
 445       quanto visto a lezione?
 446
 447       [ ] per niente        [ ] poco     [ ] molto
 448
 449
 450    3) Gli esercizi erano
 451
 452       [ ] troppo facili     [ ] alla tua portata      [ ] impossibili
 453
 454
 455    4) Il tempo a disposizione è stato
 456
 457       [ ] poco              [ ] giusto          [ ] troppo
 458
 459
 460    5) Cose che miglioreresti nel software Matita
 461
 462       .........
 463
 464
 465    6) Suggerimenti sullo svolgimento delle attività in laboratorio
 466
 467         .........
 468
 469
 470 *)
 471
 472