helm/software/matita/library/didactic/exercises/natural_deduction.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* Istruzioni:
  16
  17      http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html
  18
  19 *)
  20
  21 (* Esercizio 0
  22    ===========
  23
  24    Compilare i seguenti campi:
  25
  26    Nome1: ...
  27    Cognome1: ...
  28    Matricola1: ...
  29    Account1: ...
  30
  31    Nome2: ...
  32    Cognome2: ...
  33    Matricola2: ...
  34    Account2: ...
  35
  36 *)
  37
  38 (*DOCBEGIN
  39
  40 Scopo della lezione
  41 ===================
  42
  43 Lo scopo della lezione è di farvi imparare ad usare Matita
  44 per auto-correggervi gli esercizi di deduzione naturale, che
  45 saranno parte dell'esame scritto. Il consiglio è di
  46 fare prima gli esercizi su carta e poi digitarli in Matita
  47 per verificarne la correttezza. Fare direttamente gli esercizi
  48 con Matita è difficile e richiede molto più tempo.
  49
  50 I connettivi logici
  51 ===================
  52
  53 Per digitare i connettivi logici:
  54
  55 * `∧` : `\land`
  56 * `∨` : `\lor`
  57 * `¬` : `\lnot`
  58 * `⇒` : `=>`, `\Rightarrow`
  59 * `⊥` : `\bot`
  60 * `⊤` : `\top`
  61
  62 I termini, le formule e i nomi delle ipotesi
  63 ============================================
  64
  65 * Le formule, quando argomenti di
  66   una regola, vengono scritte tra `(` e `)`.
  67
  68 * I nomi delle ipotesi, quando argomenti di
  69   una regola, vengono scritti tra `[` e `]`.
  70
  71 Le regole di deduzione naturale
  72 ===============================
  73
  74 Per digitare le regole di deduzione naturale
  75 è possibile utilizzare la palette che compare
  76 sulla sinistra dopo aver premuto `F2`.
  77
  78 L'albero si descrive partendo dalla radice. Le regole
  79 con premesse multiple sono seguite da `[`, `|` e `]`.
  80 Ad esempio:
  81
  82         apply rule (∧#i (A∨B) ⊥);
  83           [ …continua qui il sottoalbero per (A∨B)
  84           | …continua qui il sottoalbero per ⊥
  85           ]
  86
  87 Le regole vengono applicate alle loro premesse, ovvero
  88 gli argomenti delle regole sono le formule che normalmente
  89 scrivete sopra la linea che rappresenta l'applicazione della
  90 regola stessa. Ad esempio:
  91
  92         aply rule (∨#e (A∨B) [h1] C [h2] C);
  93           [ …prova di (A∨B)
  94           | …prova di C sotto l'ipotesi A (di nome h1)
  95           | …prova di C sotto l'ipotesi B (di nome h2)
  96           ]
  97
  98 Le regole che hanno una sola premessa non vengono seguite
  99 da parentesi quadre.
 100
 101 L'albero di deduzione
 102 =====================
 103
 104 Per visualizzare l'albero man mano che viene costruito
 105 dai comandi impartiti al sistema, premere `F3` e poi
 106 premere sul bottome home (in genere contraddistinto da
 107 una icona rappresentate una casa).
 108
 109 Si suggerisce di marcare tale finestra come `always on top`
 110 utilizzando il menu a tendina che nella maggior parte degli
 111 ambienti grafici si apre cliccando nel suo angolo in
 112 alto a sinistra.
 113
 114 Applicazioni di regole errate vengono contrassegnate con
 115 il colore rosso.
 116
 117 Usare i lemmi dimostrati in precedenza
 118 ======================================
 119
 120 Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
 121 riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
 122
 123 La "regola" `lem` prende come argomenti:
 124
 125 - Il numero delle ipotesi del lemma che si vuole utilizzare, nel
 126   caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
 127
 128 - Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
 129
 130 - Infine, le formule che devono essere scritte come premesse per la
 131   "regola".
 132
 133 Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
 134 `lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
 135 `lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario
 136 far seguire le parentesi quadre come spiegato in precedenza.
 137
 138 Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
 139 per rappresentare l'albero di prova del lemma che si sta riutilizzando.
 140
 141 Per motivi che saranno più chiari una volta studiate logiche del
 142 primo ordine o di ordine superiore, i lemmi che si intende
 143 riutilizzare è bene che siano dimostrati astratti sugli atomi.
 144 Ovvero per ogni atomo `A`...`Z` che compare nella formula,
 145 è bene aggiungere una quantificazione all'inizio della formula stessa.
 146 Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
 147 La dimostrazione deve poi iniziare con il comando `assume`.
 148
 149 In tale modo il lemma EM può essere utilizzato sia per dimostrare
 150 `A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
 151
 152 DOCEND*)
 153
 154 include "didactic/support/natural_deduction.ma".
 155
 156 theorem EM: ∀A:CProp. A ∨ ¬ A.
 157 (* Il comando assume è necessario perchè dimostriamo A∨¬A
 158    per una A generica. *)
 159 assume A: CProp.
 160 (* Questo comando inizia a disegnare l'albero *)
 161 apply rule (prove (A ∨ ¬A));
 162 (* qui inizia l'albero, eseguite passo passo osservando come
 163    si modifica l'albero. *)
 164 apply rule (RAA [H] (⊥)).
 165 apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
 166         [ apply rule (discharge [H]).
 167         | apply rule (⊥#e (⊥));
 168           apply rule (¬#e (¬¬A) (¬A));
 169            [ apply rule (¬#i [K] (⊥)).
 170        apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
 171               [ (*BEGIN*)apply rule (discharge [H]).(*END*)
 172               | (*BEGIN*)apply rule (∨#i_r (¬A)).
 173           apply rule (discharge [K]).(*END*)
 174               ]
 175            | (*BEGIN*)apply rule (¬#i [K] (⊥)).
 176        apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
 177               [ apply rule (discharge [H]).
 178               | apply rule (∨#i_l (A)).
 179           apply rule (discharge [K]).
 180               ](*END*)
 181            ]
 182         ]
 183 qed.
 184
 185 theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
 186 apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
 187 (*BEGIN*)
 188 apply rule (⇒#i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
 189 apply rule (⇒#i [h2] (G ∨ L ⇒ ¬L ⇒ E));
 190 apply rule (⇒#i [h3] (¬L ⇒ E));
 191 apply rule (⇒#i [h4] (E));
 192 apply rule (∨#e (G∨L) [h5] (E) [h6] (E));
 193         [ apply rule (discharge [h3]);
 194         | apply rule (∨#e (E∨C) [h6] (E) [h7] (E));
 195             [ apply rule (⇒#e (¬L ⇒ E∨C) (¬L));
 196                 [ apply rule (discharge [h2]);
 197                 | apply rule (discharge [h4]);
 198                 ]
 199             | apply rule (discharge [h6]);
 200             | apply rule (⇒#e (C∧G ⇒ E) (C∧G));
 201                 [ apply rule (discharge [h1]);
 202                 | apply rule (∧#i (C) (G));
 203                     [ apply rule (discharge [h7]);
 204                     | apply rule (discharge [h5]);
 205                 ]
 206                 ]
 207             ]
 208         | apply rule (⊥#e (⊥));
 209           apply rule (¬#e (¬L) (L));
 210             [ apply rule (discharge [h4]);
 211             | apply rule (discharge [h6]);
 212             ]
 213         ]
 214 (*END*)
 215 qed.
 216
 217 theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
 218 apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
 219 (*BEGIN*)
 220 apply rule (⇒#i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
 221 apply rule (⇒#i [h2] ((D ⇒ A) ⇒ D ⇒ C));
 222 apply rule (⇒#i [h3] (D ⇒ C));
 223 apply rule (⇒#i [h4] (C));
 224 apply rule (∨#e (B∨¬B) [h5] (C) [h6] (C));
 225         [ apply rule (lem 0 EM);
 226         | apply rule (⇒#e (B∧D⇒C) (B∧D));
 227             [ apply rule (discharge [h2]);
 228         | apply rule (∧#i (B) (D));
 229                 [ apply rule (discharge [h5]);
 230                 | apply rule (discharge [h4]);
 231                 ]
 232             ]
 233         | apply rule (⇒#e (A∧¬B⇒C) (A∧¬B));
 234             [ apply rule (discharge [h1]);
 235             | apply rule (∧#i (A) (¬B));
 236                 [ apply rule (⇒#e (D⇒A) (D));
 237                     [ apply rule (discharge [h3]);
 238                     | apply rule (discharge [h4]);
 239                     ]
 240                 | apply rule (discharge [h6]);
 241                 ]
 242             ]
 243         ]
 244 (*END*)
 245 qed.
 246
 247 (* Per dimostrare questo teorema torna comodo il lemma EM
 248    dimostrato in precedenza. *)
 249 theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
 250 apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
 251 (*BEGIN*)
 252 apply rule (⇒#i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
 253 apply rule (⇒#i [h2] ((L⇒F) ⇒ L ⇒ E));
 254 apply rule (⇒#i [h3] (L ⇒ E));
 255 apply rule (⇒#i [h4] (E));
 256 apply rule (∨#e (G∨E) [h5] (E) [h6] (E));
 257         [ apply rule (⇒#e (F ⇒ G∨E) (F));
 258             [ apply rule (discharge [h1]);
 259             | apply rule (⇒#e (L⇒F) (L));
 260                 [ apply rule (discharge [h3]);
 261                 | apply rule (discharge [h4]);
 262                 ]
 263             ]
 264         |apply rule (∨#e (¬L∨E) [h7] (E) [h8] (E));
 265             [ apply rule (⇒#e (G⇒¬L∨E) (G));
 266                 [ apply rule (discharge [h2]);
 267                 | apply rule (discharge [h5]);
 268                 ]
 269             | apply rule (⊥#e (⊥));
 270         apply rule (¬#e (¬L) (L));
 271                 [ apply rule (discharge [h7]);
 272                 | apply rule (discharge [h4]);
 273                 ]
 274             | apply rule (discharge [h8]);
 275             ]
 276         | apply rule (discharge [h6]);
 277         ]
 278 (*END*)
 279 qed.
 280
 281 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
 282 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
 283 (*BEGIN*)
 284 apply rule (⇒#i [h1] (¬A∨¬B));
 285 apply rule (∨#e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
 286         [ apply rule (lem 0 EM);
 287         | apply rule (∨#e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
 288             [ apply rule (lem 0 EM);
 289             | apply rule (⊥#e (⊥));
 290               apply rule (¬#e (¬(A∧B)) (A∧B));
 291                 [ apply rule (discharge [h1]);
 292                 | apply rule (∧#i (A) (B));
 293                     [ apply rule (discharge [h2]);
 294                     | apply rule (discharge [h4]);
 295                     ]
 296                 ]
 297             | apply rule (∨#i_r (¬B));
 298         apply rule (discharge [h5]);
 299             ]
 300         | apply rule (∨#i_l (¬A));
 301     apply rule (discharge [h3]);
 302         ]
 303 (*END*)
 304 qed.
 305
 306 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
 307 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
 308 (*BEGIN*)
 309 apply rule (⇒#i [h1] (¬A ∧ ¬B));
 310 apply rule (∨#e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
 311         [ apply rule (lem 0 EM);
 312         | apply rule (⊥#e (⊥));
 313     apply rule (¬#e (¬(A∨B)) (A∨B));
 314             [ apply rule (discharge [h1]);
 315             | apply rule (∨#i_l (A));
 316         apply rule (discharge [h2]);
 317             ]
 318         | apply rule (∨#e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
 319             [ apply rule (lem 0 EM);
 320             | apply rule (⊥#e (⊥));
 321         apply rule (¬#e (¬(A∨B)) (A∨B));
 322                 [ apply rule (discharge [h1]);
 323                 | apply rule (∨#i_r (B));
 324             apply rule (discharge [h10]);
 325                 ]
 326             | apply rule (∧#i (¬A) (¬B));
 327                 [ apply rule (discharge [h3]);
 328                 |apply rule (discharge [h11]);
 329                 ]
 330             ]
 331         ]
 332 (*END*)
 333 qed.
 334
 335 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
 336 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
 337 (*BEGIN*)
 338 apply rule (⇒#i [h1] (¬(A∨B)));
 339 apply rule (¬#i [h2] (⊥));
 340 apply rule (∨#e (A∨B) [h3] (⊥) [h3] (⊥));
 341         [ apply rule (discharge [h2]);
 342         | apply rule (¬#e (¬A) (A));
 343             [ apply rule (∧#e_l (¬A∧¬B));
 344         apply rule (discharge [h1]);
 345             | apply rule (discharge [h3]);
 346             ]
 347         | apply rule (¬#e (¬B) (B));
 348             [ apply rule (∧#e_r (¬A∧¬B));
 349         apply rule (discharge [h1]);
 350             | apply rule (discharge [h3]);
 351             ]
 352         ]
 353 (*END*)
 354 qed.
 355
 356 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
 357 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
 358 (*BEGIN*)
 359 apply rule (⇒#i [h1] (A));
 360 apply rule (RAA [h2] (⊥));
 361 apply rule (⇒#e ((A⇒⊥)⇒⊥) (A⇒⊥));
 362         [ apply rule (discharge [h1]);
 363         | apply rule (⇒#i [h3] (⊥));
 364           apply rule (¬#e (¬A) (A));
 365             [ apply rule (discharge [h2]);
 366             | apply rule (discharge [h3]);
 367             ]
 368         ]
 369 (*END*)
 370 qed.
 371