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 (*DOCBEGIN
  25
  26    Come scrivere i simboli
  27    =======================
  28
  29    Per inserire i simboli matematici è necessario digitare il loro nome
  30    e poi premere CTRL-L. In generale i nomi dei simboli sono della forma
  31    '\nome', ad esempio '\equiv'. Alcuni simboli molto frequenti hanno
  32    dei sinonimi più comodi da digitare, per esemio ⇒ ha sia il nome
  33    '\Rightarrow' sia '=>'.
  34
  35    Segue un elenco dei simboli più comuni e i loro nomi separati da virgola,
  36    Se sono necessari dei simboli non riportati di seguito si può visualizzare
  37    l'intera lista dal menù a tendina 'View ▹ TeX/UTF8 table'.
  38
  39    * → : \to, ->
  40    * ⇒ : \Rightarrow, =>
  41    * ℕ : \naturals
  42    * ≝ : \def, :=
  43    * ≡ : \equiv
  44    * ∀ : \forall
  45
  46    La sintassi '∀v.P' significa "per tutti i 'v' vale 'P'".
  47
  48    La sintassi 'F → G' dove 'F' e 'G' sono proposizioni nel metalinguaggio
  49    significa "'F' implica 'G'". Attenzione, il simbolo '⇒' (usato a lezione)
  50    non ha lo stesso significato in Matita.
  51
  52    La sintassi 'ℕ → ℕ' è il tipo delle funzioni che preso un numero naturale
  53    restituiscono un numero naturale.
  54
  55    LA sintassi ..
  56    ==============
  57    * applicazione
  58    * match
  59    * min/max a b
  60    * sottrazione
  61
  62    I comandi per le definizioni
  63    ============================
  64
  65    Esistono due tipi di definizioni: definizioni ricorsive tramite sintassi
  66    simile a BNF, definizione di funzioni per ricorsione strutturale.
  67
  68    Definire una nuova sintassi astratta
  69    ------------------------------------
  70
  71    Definizione
  72
  73 DOCEND*)
  74
  75 (* non modificare le seguenti tre righe *)
  76 include "nat/minus.ma".
  77 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.
  78 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.
  79
  80 (* Esercizio 1: Definire l'albero di sintassi astratta delle formule *)
  81 inductive Formula : Type ≝
  82 | FBot: Formula
  83 | FTop: (*BEGIN*)Formula(*END*)
  84 | FAtom: nat → Formula (* usiamo i naturali al posto delle lettere *)
  85 | FAnd: Formula → Formula → Formula
  86 | FOr: (*BEGIN*)Formula → Formula → Formula(*END*)
  87 | FImpl: (*BEGIN*)Formula → Formula → Formula(*END*)
  88 | FNot: (*BEGIN*)Formula → Formula(*END*)
  89 .
  90
  91 (* Esercizio 2: Data la funzione di valutazione per gli atomi 'v', definire la
  92    funzione 'sem' per una generica formula 'F' che vi associa la semantica
  93    (o denotazione) *)
  94 let rec sem (v: nat → nat) (F: Formula) on F ≝
  95  match F with
  96   [ FBot ⇒ 0
  97   | FTop ⇒ (*BEGIN*)1(*END*)
  98   (*BEGIN*)
  99   | FAtom n ⇒ v n
 100   (*END*)
 101   | FAnd F1 F2 ⇒ (*BEGIN*)min (sem v F1) (sem v F2)(*END*)
 102   (*BEGIN*)
 103   | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
 104   | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
 105   (*END*)
 106   | FNot F1 ⇒ 1 - (sem v F1)
 107   ]
 108 .
 109
 110 (* I comandi che seguono definiscono la seguente notazione:
 111
 112    if e then risultato1 else risultato2
 113
 114    Questa notazione permette di valutare l'espressione 'e'. Se questa
 115    è vera restituisce 'risultato1', altrimenti restituisce 'risultato2'.
 116
 117    Un esempio di espressione è 'eqb n m', che confronta i due numeri naturali
 118    'n' ed 'm'.
 119
 120    * [[ formula ]]_v
 121
 122    Questa notazione utilizza la funzione 'sem' precedentemente definita, in
 123    particolare '[[ f ]]_v' è una abbreviazione per 'sem v f'.
 124
 125   Non modificare le linee seguenti, saltare all'esercizio 3
 126 *)
 127 definition if_then_else ≝ λe,t,f.match e return λ_.Formula with [ true ⇒ t | false ⇒ f].
 128 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 }.
 129 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 }.
 130 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else e t f).
 131 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 132 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 133 notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
 134 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
 135
 136
 137 (* Esercizio 3: Definire la funzione di sostituzione di una formula 'G' al posto
 138    degli atomi uguali a 'x' in una formula 'F'. *)
 139 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
 140  match F with
 141   [ FBot ⇒ FBot
 142   | FTop ⇒ (*BEGIN*)FTop(*END*)
 143   | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else (*BEGIN*)(FAtom n)(*END*)
 144   (*BEGIN*)
 145   | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
 146   | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
 147   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
 148   (*END*)
 149   | FNot F ⇒ FNot (subst x G F)
 150   ].
 151
 152 (* I comandi che seguono definiscono la seguente notazione:
 153
 154   * F [ G / x ]
 155
 156   Questa notazione utilizza la funzione 'subst' appena definita, in particolare
 157   la scrittura 'F [ G /x ]' è una abbreviazione per 'subst x G F'.
 158
 159   * F ≡ G
 160
 161   Questa notazione è una abbreviazione per '∀v.[[ f ]]_v = [[ g ]]_v'.
 162   Asserisce che for ogni funzione di valutazione 'v', la semantica di 'f'
 163   in 'v' è uguale alla semantica di 'g' in 'v'.
 164
 165   Non modificare le linee seguenti, saltare all'esercizio 4
 166 *)
 167 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
 168 notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
 169 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
 170 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
 171 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 172 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 173 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 174
 175 (* Esercizio 4: Prove the substitution theorem *)
 176 theorem substitution: ∀G1,G2,F,x. G1 ≡ G2 → F[G1/x] ≡ F[G2/x].
 177 assume G1 : Formula.
 178 assume G2 : Formula.
 179 (*BEGIN*)
 180 assume F : Formula.
 181 assume x : ℕ.
 182 (*END*)
 183 suppose (G1 ≡ G2) (H).
 184 we proceed by induction on F to prove (F[ G1/x ] ≡ F[ G2/x ]).
 185 case FBot.
 186   the thesis becomes (FBot ≡ FBot[ G2/x ]).
 187   the thesis becomes (FBot ≡ FBot).
 188   the thesis becomes (∀v.[[FBot]]_v = [[FBot]]_v).
 189   assume v : (ℕ → ℕ).
 190   the thesis becomes (0 = [[FBot]]_v).
 191   the thesis becomes (0 = 0).
 192   done.
 193 case FTop.
 194   (*BEGIN*)
 195   the thesis becomes (FTop ≡ FTop).
 196   the thesis becomes (∀v. [[FTop]]_v = [[FTop]]_v).
 197   assume v : (ℕ → ℕ).
 198   the thesis becomes (1 = 1).
 199   (*END*)
 200   done.
 201 case FAtom.
 202   assume n : ℕ.
 203   the thesis becomes
 204     (if eqb n x then G1 else (FAtom n) ≡ (FAtom n)[ G2/x ]).
 205   the thesis becomes
 206     (if eqb n x then G1 else (FAtom n) ≡
 207      if eqb n x then G2 else (FAtom n)).
 208   we proceed by cases on (eqb n x) to prove
 209     (if eqb n x then G1 else (FAtom n) ≡
 210      if eqb n x then G2 else (FAtom n)).
 211   case true.
 212     the thesis becomes (G1 ≡ G2).
 213     done.
 214   case false.
 215     (*BEGIN*)
 216     the thesis becomes (FAtom n ≡ FAtom n).
 217     the thesis becomes (∀v. [[FAtom n]]_v = [[FAtom n]]_v).
 218     assume v : (ℕ → ℕ).
 219     the thesis becomes (v n = v n).
 220     (*END*)
 221     done.
 222 case FAnd.
 223   assume F1 : Formula.
 224   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 225   assume F2 : Formula.
 226   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 227   the thesis becomes
 228     (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]_v = [[ (FAnd F1 F2)[ G2/x ] ]]_v).
 229   assume v : (ℕ → ℕ).
 230   the thesis becomes
 231     (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 232      min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 233   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 234   by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 235   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 236   by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 237   conclude
 238       (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 239     = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 240     = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*).
 241   (*END*)
 242   done.
 243 case FOr.
 244   (*BEGIN*)
 245   assume F1 : Formula.
 246   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 247   assume F2 : Formula.
 248   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 249   the thesis becomes
 250     (∀v.[[ (FOr F1 F2)[ G1/x ] ]]_v = [[ (FOr F1 F2)[ G2/x ] ]]_v).
 251   assume v : (ℕ → ℕ).
 252   the thesis becomes
 253     (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 254      max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 255   by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
 256   by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
 257   by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
 258   by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
 259   conclude
 260       (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 261     = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
 262     = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111.
 263   (*END*)
 264   done.
 265 case FImpl.
 266   (*BEGIN*)
 267   assume F1 : Formula.
 268   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1).
 269   assume F2 : Formula.
 270   by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2).
 271   the thesis becomes
 272     (∀v.max (1 - [[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
 273         max (1 - [[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
 274   assume v : (ℕ → ℕ).
 275   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH11).
 276   by IH2 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH22).
 277   conclude
 278       (max (1-[[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
 279     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH11.
 280     = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)) by IH22.
 281   done.
 282 case FNot.
 283   (*BEGIN*)
 284   assume F1 : Formula.
 285   by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH).
 286   the thesis becomes (FNot (F1[ G1/x ]) ≡ FNot (F1[ G2/x ])).
 287   the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]_v = [[FNot (F1[ G2/x ])]]_v).
 288   assume v : (ℕ → ℕ).
 289   the thesis becomes (1 - [[F1[ G1/x ]]]_v = [[FNot (F1[ G2/x ])]]_v).
 290   the thesis becomes (1 - [[ F1[ G1/x ] ]]_v = 1 - [[ F1[ G2/x ] ]]_v).
 291   by IH we proved (∀v1.[[ F1[  G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH1).
 292   by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH2).
 293   conclude
 294       (1-[[ F1[ G1/x ] ]]_v)
 295     = (1-[[ F1[ G2/x ] ]]_v) by IH2.
 296   (*END*)
 297   done.
 298 qed.
 299
 300 (* Questionario
 301
 302    Compilare mettendo una X nella risposta scelta.
 303
 304    1) Pensi che sia utile l'integrazione del corso con una attività di
 305       laboratorio?
 306
 307       [ ] per niente        [ ] poco     [ ] molto
 308
 309
 310    2) Pensi che gli esercizi proposti ti siano stati utili a capire meglio
 311       quanto visto a lezione?
 312
 313       [ ] per niente        [ ] poco     [ ] molto
 314
 315
 316    3) Gli esercizi erano
 317
 318       [ ] troppo facili     [ ] alla tua portata      [ ] impossibili
 319
 320
 321    4) Il tempo a disposizione è stato
 322
 323       [ ] poco              [ ] giusto          [ ] troppo
 324
 325
 326    5) Cose che miglioreresti nel software Matita
 327
 328       .........
 329
 330
 331    6) Suggerimenti sullo svolgimento delle attività in laboratorio
 332
 333         .........
 334
 335
 336 *)
 337
 338