helm/software/matita/contribs/didactic/induction.ma

   1 (* Esercitazione di logica 22/10/2008.
   2
   3    Esercizio 0: compilare i seguenti campi
   4
   5    Nome1: ...
   6    Cognome1: ...
   7    Matricola1: ...
   8    Account1: ...
   9
  10    Nome2: ...
  11    Cognome2: ...
  12    Matricola2: ...
  13    Account2: ...
  14
  15    Prima di abbandonare la postazione:
  16
  17    * compilare il questionario in fondo al file
  18
  19    * salvare il file (menu 'File ▹ Save as ...') nella directory (cartella)
  20      /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui
  21      account è mrossi deve salvare il file in /public/linguaggi_mrossi.ma
  22 *)
  23
  24 (*
  25    Come scrivere i simboli
  26    =======================
  27
  28    Per inserire i simboli matematici è necessario digitare il loro nome
  29    e poi premere CTRL-L. In generale i nomi dei simboli sono della forma
  30    '\nome', ad esempio '\equiv'. Alcuni simboli molto frequenti hanno
  31    dei sinonimi più comodi da digitare, per esemio ⇒ ha sia il nome
  32    '\Rightarrow' sia '=>'.
  33
  34    Segue un elenco dei simboli più comuni e i loro nomi separati da virgola,
  35    Se sono necessari dei simboli non riportati di seguito si può visualizzare
  36    l'intera lista dal menù a tendina 'View ▹ TeX/UTF8 table'.
  37
  38    * → : \to, ->
  39    * ⇒ : \Rightarrow, =>
  40    * ℕ : \naturals
  41    * ≝ : \def, :=
  42    * ≡ : \equiv
  43    * ∀ : \forall
  44
  45    La sintassi '∀v.P' significa "per tutti i 'v' vale 'P'".
  46
  47    La sintassi 'F → G' dove 'F' e 'G' sono proposizioni nel metalinguaggio
  48    significa "'F' implica 'G'". Attenzione, il simbolo '⇒' (usato a lezione)
  49    non ha lo stesso significato in Matita.
  50
  51    La sintassi 'ℕ → ℕ' è il tipo delle funzioni che preso un numero naturale
  52    restituiscono un numero naturale.
  53
  54    La sintassi di Matita
  55    =====================
  56
  57    Il linguaggio di Matita si basa sul λ-calcolo CIC, la cui sintassi si
  58    differenzia in vari aspetti da quella che solitamente viene utilizzata
  59    per fare matematica, e ricorda quella di Scheme che state vedendo nel corso
  60    di programmazione.
  61
  62    * applicazione
  63
  64      Se 'f' è una funzione che si aspetta due argomenti, l'applucazione di 'f'
  65      agli argomenti 'x' e 'y' si scrive '(f x y)' e non 'f(x,y)'. Le parentesi
  66      possono essere omesse se il senso è chiaro dal contesto. In particolare
  67      vengono omesse quando l'applicazione è argomento di un operatore binario.
  68      Esempio: 'f x y + f y x' si legge '(f x y) + (f y x)'.
  69
  70    * minimo e massimo
  71
  72      Le funzioni 'min' e 'max' non fanno eccezione, per calcolare il
  73      massimo tra 'x' e 'y' si scrive '(max x y)' e non 'max{x,y}'
  74
  75    * Le funzioni definite per ricorsione strutturale utilizzano il costrutto
  76      'let rec' (ricorsione) e il costrutto 'match' (analisi per casi).
  77
  78      Ad esempio la funzione count definita a lezione come
  79
  80         count ⊤ ≝ 1
  81         count (F1 ∧ F2) ≝ 1 + count F1 + count F2
  82         ...
  83
  84      la si esprime come
  85
  86         let rec count F on F ≝
  87           match F with
  88           [ ⊤ ⇒ 1
  89           | F1 ∧ F2 ⇒ 1 + count F1 + count F2
  90           ...
  91           ].
  92
  93    * Per dare la definizione ricorsiva (di un linguaggio) si usa una sintassi
  94      simile a BNF. Per esempio per definire
  95
  96        <A> ::= <A> "+" <A> | <A> "*" <A> | "0" | "1"
  97
  98      si usa il seguente comando
  99
 100        inductive A : Type ≝
 101        | Plus : A → A → A
 102        | Times : A → A → A
 103        | Zero : A
 104        | One : A
 105        .
 106
 107    La ratio è che 'Plus' prende due argomenti di tipo A per darmi un A,
 108    mentre 'Zero' non prende nessun argomento per darmi un A. Al posto di usare
 109    operatori infissi (0 + 0) la definizione crea operatori prefissi (funzioni).
 110    Quindi (0+0) si scriverà come (Plus Zero Zero).
 111
 112 *)
 113
 114 (* non modificare le seguenti tre righe *)
 115 include "nat/minus.ma".
 116 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.
 117 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.
 118
 119
 120 (* Esercizio 1: Definire l'albero di sintassi astratta delle formule *)
 121 inductive Formula : Type ≝
 122 | FBot: Formula
 123 | FTop: (*BEGIN*)Formula(*END*)
 124 | FAtom: nat → Formula (* usiamo i naturali al posto delle lettere *)
 125 | FAnd: Formula → Formula → Formula
 126 | FOr: (*BEGIN*)Formula → Formula → Formula(*END*)
 127 | FImpl: (*BEGIN*)Formula → Formula → Formula(*END*)
 128 | FNot: (*BEGIN*)Formula → Formula(*END*)
 129 .
 130
 131
 132 (* Esercizio 2: Data la funzione di valutazione per gli atomi 'v', definire la
 133    funzione 'sem' per una generica formula 'F' che vi associa la semantica
 134    (o denotazione) *)
 135 let rec sem (v: nat → nat) (F: Formula) on F ≝
 136  match F with
 137   [ FBot ⇒ 0
 138   | FTop ⇒ (*BEGIN*)1(*END*)
 139   (*BEGIN*)
 140   | FAtom n ⇒ v n
 141   (*END*)
 142   | FAnd F1 F2 ⇒ (*BEGIN*)min (sem v F1) (sem v F2)(*END*)
 143   (*BEGIN*)
 144   | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
 145   | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
 146   (*END*)
 147   | FNot F1 ⇒ 1 - (sem v F1)
 148   ]
 149 .
 150
 151
 152 (* I comandi che seguono definiscono la seguente notazione:
 153
 154    if e then risultato1 else risultato2
 155
 156    Questa notazione permette di valutare l'espressione 'e'. Se questa
 157    è vera restituisce 'risultato1', altrimenti restituisce 'risultato2'.
 158
 159    Un esempio di espressione è 'eqb n m', che confronta i due numeri naturali
 160    'n' ed 'm'.
 161
 162    * [[ formula ]]_v
 163
 164    Questa notazione utilizza la funzione 'sem' precedentemente definita, in
 165    particolare '[[ f ]]_v' è una abbreviazione per 'sem v f'.
 166
 167   Non modificare le linee seguenti, saltare all'esercizio 3
 168 *)
 169 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
 170 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 }.
 171 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 }.
 172 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
 173 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 174 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 175 notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
 176 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
 177
 178
 179 (* TESTARE LA DEFINIZIONE DI SEM *)
 180 definition v110 ≝ λx.
 181       if eqb x 0 then 1  (* Atom 0 ↦ 1 *)
 182  else if eqb x 1 then 1  (* Atom 1 ↦ 1 *)
 183  else if eqb x 2 then 0  (* Atom 2 ↦ 0 *)
 184  else                 0. (* Atom _ ↦ 0 *)
 185
 186
 187 definition formula1 ≝ (FAnd (FAtom 1) (FAtom 0)).
 188
 189
 190 eval normalize on [[ formula1 ]]_v110.
 191
 192
 193 (* Esercizio 3: Definire la funzione di sostituzione di una formula 'G' al posto
 194    degli atomi uguali a 'x' in una formula 'F'. *)
 195 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
 196  match F with
 197   [ FBot ⇒ FBot
 198   | FTop ⇒ (*BEGIN*)FTop(*END*)
 199   | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else (*BEGIN*)(FAtom n)(*END*)
 200   (*BEGIN*)
 201   | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
 202   | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
 203   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
 204   (*END*)
 205   | FNot F ⇒ FNot (subst x G F)
 206   ].
 207
 208 (* AGGIUNGERE ALCUNI TEST *)
 209
 210
 211 (* I comandi che seguono definiscono la seguente notazione:
 212
 213   * F [ G / x ]
 214
 215   Questa notazione utilizza la funzione 'subst' appena definita, in particolare
 216   la scrittura 'F [ G /x ]' è una abbreviazione per 'subst x G F'.
 217
 218   * F ≡ G
 219
 220   Questa notazione è una abbreviazione per '∀v.[[ f ]]_v = [[ g ]]_v'.
 221   Asserisce che for ogni funzione di valutazione 'v', la semantica di 'f'
 222   in 'v' è uguale alla semantica di 'g' in 'v'.
 223
 224   Non modificare le linee seguenti, saltare all'esercizio 4
 225 *)
 226 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
 227 notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
 228 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
 229 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
 230 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 231 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 232 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 233
 234
 235
 236 (* Esercizio 4: Prove the substitution theorem *)
 237 theorem substitution: ∀G1,G2,F,x. G1 ≡ G2 → F[G1/x] ≡ F[G2/x].
 238 assume G1 : Formula.
 239 assume G2 : Formula.
 240 (*BEGIN*)
 241 assume F : Formula.
 242 assume x : ℕ.
 243 (*END*)
 244 suppose (G1 ≡ G2) (H).
 245 we proceed by induction on F to prove (F[ G1/x ] ≡ F[ G2/x ]).
 246 case FBot.
 247   the thesis becomes (FBot ≡ FBot[ G2/x ]).
 248   the thesis becomes (FBot ≡ FBot).
 249   the thesis becomes (∀v.[[FBot]]_v = [[FBot]]_v).
 250   assume v : (ℕ → ℕ).
 251   the thesis becomes (0 = [[FBot]]_v).
 252   the thesis becomes (0 = 0).
 253   done.
 254 case FTop.
 255   (*BEGIN*)
 256   the thesis becomes (FTop ≡ FTop).
 257   the thesis becomes (∀v. [[FTop]]_v = [[FTop]]_v).
 258   assume v : (ℕ → ℕ).
 259   the thesis becomes (1 = 1).
 260   (*END*)
 261   done.
 262 case FAtom.
 263   assume n : ℕ.
 264   the thesis becomes
 265     (if eqb n x then G1 else (FAtom n) ≡ (FAtom n)[ G2/x ]).
 266   the thesis becomes
 267     (if eqb n x then G1 else (FAtom n) ≡
 268      if eqb n x then G2 else (FAtom n)).
 269   we proceed by cases on (eqb n x) to prove
 270     (if eqb n x then G1 else (FAtom n) ≡
 271      if eqb n x then G2 else (FAtom n)).
 272   case true.
 273     the thesis becomes (G1 ≡ G2).
 274     done.
 275   case false.
 276     (*BEGIN*)
 277     the thesis becomes (FAtom n ≡ FAtom n).
 278     the thesis becomes (∀v. [[FAtom n]]_v = [[FAtom n]]_v).
 279     assume v : (ℕ → ℕ).
 280     the thesis becomes (v n = v n).
 281     (*END*)
 282     done.
 283 case FAnd.
 284   assume F1 : Formula.
 285   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 286   assume F2 : Formula.
 287   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 288   the thesis becomes
 289     (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]_v = [[ (FAnd F1 F2)[ G2/x ] ]]_v).
 290   assume v : (ℕ → ℕ).
 291   the thesis becomes
 292     (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 293      min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 294   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 295   by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 296   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 297   by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 298   conclude
 299       (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 300     = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 301     = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*).
 302   (*END*)
 303   done.
 304 case FOr.
 305   (*BEGIN*)
 306   assume F1 : Formula.
 307   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 308   assume F2 : Formula.
 309   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 310   the thesis becomes
 311     (∀v.[[ (FOr F1 F2)[ G1/x ] ]]_v = [[ (FOr F1 F2)[ G2/x ] ]]_v).
 312   assume v : (ℕ → ℕ).
 313   the thesis becomes
 314     (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 315      max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 316   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 317   by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 318   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 319   by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 320   conclude
 321       (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 322     = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 323     = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111.
 324   (*END*)
 325   done.
 326 case FImpl.
 327   (*BEGIN*)
 328   assume F1 : Formula.
 329   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 330   assume F2 : Formula.
 331   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 332   the thesis becomes
 333     (∀v.max (1 - [[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 334         max (1 - [[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 335   assume v : (ℕ → ℕ).
 336   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH11).
 337   by IH2 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH22).
 338   conclude
 339       (max (1-[[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 340     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH11.
 341     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)) by IH22.
 342   done.
 343 case FNot.
 344   (*BEGIN*)
 345   assume F1 : Formula.
 346   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH).
 347   the thesis becomes (FNot (F1[ G1/x ]) ≡ FNot (F1[ G2/x ])).
 348   the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]_v = [[FNot (F1[ G2/x ])]]_v).
 349   assume v : (ℕ → ℕ).
 350   the thesis becomes (1 - [[F1[ G1/x ]]]_v = [[FNot (F1[ G2/x ])]]_v).
 351   the thesis becomes (1 - [[ F1[ G1/x ] ]]_v = 1 - [[ F1[ G2/x ] ]]_v).
 352   by IH we proved (∀v1.[[ F1[  G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH1).
 353   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH2).
 354   conclude
 355       (1-[[ F1[ G1/x ] ]]_v)
 356     = (1-[[ F1[ G2/x ] ]]_v) by IH2.
 357   (*END*)
 358   done.
 359 qed.
 360
 361 eval normalize on
 362   (substitution (FAtom 1) (FAtom 1) formula1 1 (λ_.refl_eq ??) v110).
 363
 364 (* Questionario
 365
 366    Compilare mettendo una X nella risposta scelta.
 367
 368    1) Pensi che sia utile l'integrazione del corso con una attività di
 369       laboratorio?
 370
 371       [ ] per niente        [ ] poco     [ ] molto
 372
 373
 374    2) Pensi che gli esercizi proposti ti siano stati utili a capire meglio
 375       quanto visto a lezione?
 376
 377       [ ] per niente        [ ] poco     [ ] molto
 378
 379
 380    3) Gli esercizi erano
 381
 382       [ ] troppo facili     [ ] alla tua portata      [ ] impossibili
 383
 384
 385    4) Il tempo a disposizione è stato
 386
 387       [ ] poco              [ ] giusto          [ ] troppo
 388
 389
 390    5) Cose che miglioreresti nel software Matita
 391
 392       .........
 393
 394
 395    6) Suggerimenti sullo svolgimento delle attività in laboratorio
 396
 397         .........
 398
 399
 400 *)
 401
 402