helm/software/matita/library/didactic/exercises/natural_deduction_theories.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 (* Esercizio 0
  16    ===========
  17
  18    Compilare i seguenti campi:
  19
  20    Nome1: ...
  21    Cognome1: ...
  22    Matricola1: ...
  23    Account1: ...
  24
  25    Nome2: ...
  26    Cognome2: ...
  27    Matricola2: ...
  28    Account2: ...
  29
  30 *)
  31
  32 (*DOCBEGIN
  33
  34 I connettivi logici
  35 ===================
  36
  37 Per digitare i connettivi logici:
  38
  39 * `∧` : `\land`
  40 * `∨` : `\lor`
  41 * `¬` : `\lnot`
  42 * `⇒` : `=>`, `\Rightarrow`
  43 * `⊥` : `\bot`
  44 * `⊤` : `\top`
  45
  46 Per digitare i quantificatori:
  47
  48 * `∀` : `\forall`
  49 * `∃` : `\exists`
  50
  51 I termini, le formule e i nomi delle ipotesi
  52 ============================================
  53
  54 * I termini quantificati da `∀` e `∃`, quando argomenti di
  55   una regola, vengono scritti tra `{` e `}`.
  56
  57 * Le formule, quando argomenti di
  58   una regola, vengono scritte tra `(` e `)`.
  59
  60 * I nomi delle ipotesi, quando argomenti di
  61   una regola, vengono scritti tra `[` e `]`.
  62
  63 Le regole di deduzione naturale
  64 ===============================
  65
  66 Per digitare le regole di deduzione naturale
  67 è possibile utilizzare la palette che compare
  68 sulla sinistra dopo aver premuto `F2`.
  69
  70 L'albero si descrive partendo dalla radice. Le regole
  71 con premesse multiple sono seguite da `[`, `|` e `]`.
  72 Ad esempio:
  73
  74         apply rule (∧#i (A∨B) ⊥);
  75           [ …continua qui il sottoalbero per (A∨B)
  76           | …continua qui il sottoalbero per ⊥
  77           ]
  78
  79 Le regole vengono applicate alle loro premesse, ovvero
  80 gli argomenti delle regole sono le formule che normalmente
  81 scrivete sopra la linea che rappresenta l'applicazione della
  82 regola stessa. Ad esempio:
  83
  84         apply rule (∨#e (A∨B) [h1] C [h2] C);
  85           [ …prova di (A∨B)
  86           | …prova di C sotto l'ipotesi A (di nome h1)
  87           | …prova di C sotto l'ipotesi B (di nome h2)
  88           ]
  89
  90 Le regole che hanno una sola premessa non vengono seguite
  91 da parentesi quadre.
  92
  93 L'albero di deduzione
  94 =====================
  95
  96 Per visualizzare l'albero man mano che viene costruito
  97 dai comandi impartiti al sistema, premere `F3` e poi
  98 premere sul bottome home (in genere contraddistinto da
  99 una icona rappresentate una casa).
 100
 101 Si suggerisce di marcare tale finestra come `always on top`
 102 utilizzando il menu a tendina che nella maggior parte degli
 103 ambienti grafici si apre cliccando nel suo angolo in
 104 alto a sinistra.
 105
 106 Applicazioni di regole errate vengono contrassegnate con
 107 il colore rosso.
 108
 109 Usare i lemmi dimostrati in precedenza
 110 ======================================
 111
 112 Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
 113 riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
 114
 115 La "regola" `lem` prende come argomenti:
 116
 117 - Il numero delle ipotesi del lemma che si vuole utilizzare, nel
 118   caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
 119
 120 - Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
 121
 122 - Infine, le formule che devono essere scritte come premesse per la
 123   "regola".
 124
 125 Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
 126 `lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
 127 `lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario
 128 far seguire le parentesi quadre come spiegato in precedenza.
 129
 130 Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
 131 per rappresentare l'albero di prova del lemma che si sta riutilizzando.
 132
 133 Per motivi che saranno più chiari una volta studiate logiche del
 134 primo ordine o di ordine superiore, i lemmi che si intende
 135 riutilizzare è bene che siano dimostrati astratti sugli atomi.
 136 Ovvero per ogni atomo `A`...`Z` che compare nella formula,
 137 è bene aggiungere una quantificazione all'inizio della formula stessa.
 138 Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
 139 La dimostrazione deve poi iniziare con il comando `assume`.
 140
 141 In tale modo il lemma EM può essere utilizzato sia per dimostrare
 142 `A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
 143
 144 DOCEND*)
 145
 146 include "nat/plus.ma".
 147
 148 lemma ex0: ∀n. n + O = n.
 149  assume n: nat.
 150  we proceed by induction on n to prove (n + O = n).
 151   case O.
 152    the thesis becomes (O + O = O).
 153     conclude
 154         (O + O)
 155       = O
 156     done.
 157   case S.
 158    assume n : nat.
 159    by induction hypothesis we know (n + O = n) (H).
 160    the thesis becomes (S n + O = S n).
 161     conclude
 162        (S n + O)
 163      = (S (n + O)).
 164      = (S n) by H
 165     done.
 166 qed.
 167
 168 include "didactic/support/natural_deduction.ma".
 169
 170 (* Il nostro linguaggio del primo ordine prevede le seguenti
 171    - costanti: O
 172    - funzioni: S (unaria), plus, mult (binarie)
 173    - predicati: eq (binari)
 174 *)
 175 axiom O : sort.                  (* zero *)
 176 axiom S : sort → sort.           (* successore *)
 177 axiom plus : sort → sort → sort. (* addizione *)
 178 axiom mult: sort → sort → sort.  (* moltiplicazione *)
 179 axiom eq : sort → sort → CProp.  (* uguaglianza *)
 180
 181 (*
 182 notation < "+  term 90 x  term 90 y" non associative with precedence 80 for @{'plus $x $y}.
 183 notation < "★  term 90 x  term 90 y" non associative with precedence 80 for @{'mult $x $y}.
 184 notation < "=  term 90 x  term 90 y" non associative with precedence 80 for @{'eq $x $y}.
 185 notation < "\S  term 90 x" non associative with precedence 80 for @{'S $x}.
 186 notation < "\O" non associative with precedence 80 for @{'O}.
 187 interpretation "O" 'O = O.
 188 interpretation "S" 'S x y = (S x y).
 189 interpretation "mult" 'mult x y = (mult x y).
 190 interpretation "plus" 'plus x y = (plus x y).
 191 interpretation "eq" 'eq x y = (eq x y).
 192 *)
 193
 194 interpretation "+" 'my_plus x y = (plus x y).
 195 interpretation "*" 'my_mult x y = (mult x y).
 196 interpretation "=" 'my_eq x y = (eq x y).
 197 interpretation "S" 'my_S x = (S x).
 198 interpretation "O" 'my_O = O.
 199
 200 notation "x + y" non associative with precedence 50 for @{'my_plus $x $y}.
 201 notation "x * y" non associative with precedence 55 for @{'my_mult $x $y}.
 202 notation "x = y" non associative with precedence 45 for @{'my_eq $x $y}.
 203 notation > "'S' x" non associative with precedence 40 for @{'my_S $x}.
 204 notation < "'S'  x" non associative with precedence 40 for @{'my_S $x}.
 205 notation "'O'" non associative with precedence 90 for @{'my_O}.
 206
 207 (* Assumiamo la seguente teoria *)
 208
 209 (* l'uguaglianza e' una relazione d'equivalenza *)
 210 axiom refl: ∀x. x = x.
 211 axiom sym: ∀x.∀y. x = y ⇒ y = x.
 212 axiom trans: ∀x.∀y.∀z. x = y ⇒ y = z ⇒ x = z.
 213
 214 (* assiomi di Peano *)
 215 axiom discr: ∀x. ¬ O = (S x).
 216 axiom inj: ∀x.∀y. (S x) = (S y) ⇒ x = y.
 217 (* Questo è uno schema di assiomi: è come avere una regola di induzione per
 218    ogni predicato unario P. Il sistema inferisce automaticamente P. *)
 219 axiom induct: ΠP. P O ⇒ (∀n. P n ⇒ P (S n)) ⇒ ∀x.P x.
 220
 221 (* definizione ricorsiva di addizione *)
 222 axiom plus_O: ∀x. O + x = x.
 223 axiom plus_S: ∀x.∀y. (S x) + y = S (x + y).
 224
 225 (* definizione ricorsiva di moltiplicazione *)
 226 axiom mult_O: ∀x.O * x = O.
 227 axiom mult_S: ∀x.∀y. (S x) * y = x * y + y.
 228
 229 (* l'uguaglianza e' una congruenza rispetto a tutte le funzioni e predicati *)
 230 axiom eq_S: ∀x.∀x'. x = x' ⇒ (S x) = (S x').
 231 axiom eq_plus: ∀x.∀x'.∀y.∀y'. x = x' ⇒ y = y' ⇒ x + y = x' + y'.
 232 axiom eq_mult: ∀x.∀x'.∀y.∀y'. x = x' ⇒ y = y' ⇒ x * y = x' * y'.
 233
 234 (* intuizionista *)
 235 lemma ex1: ∀x.x + O = x.
 236 apply rule (prove (∀x.x + O = x));
 237 (* poichè tutti gli assiomi della teoria sono assiomi e non dimostrazioni,
 238    l'unica forma di `apply rule lem` che potete usare è
 239    `apply rule (lem 0 nome_assioma)` *)
 240 (*BEGIN*)
 241 apply rule (⇒#e ((∀n.(n + O) = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (∀n.(n + O) = n ⇒ ((S n) + O) = (S n)));
 242         [ apply rule (⇒#e ((O + O) = O ⇒ (∀n.n + O = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (O + O = O));
 243            [ apply rule (lem 0 induct);
 244            | apply rule (∀#e {O} (∀y.(O + y) =y));
 245              apply rule (lem 0 plus_O);
 246            ]
 247         | apply rule (∀#i {n} (n + O = n ⇒ ((S n) + O) = (S n)));
 248     apply rule (⇒#i [H] (((S n) + O) = (S n)));
 249     apply rule (⇒#e ((S (n + O)) = (S n) ⇒ ((S n) + O) = (S n)) ((S (n + O)) = (S n)));
 250            [ apply rule (⇒#e (((S n) + O) =(S (n + O)) ⇒ (S (n + O)) = (S n)⇒((S n) + O) =(S n)) (((S n) + O) =(S (n + O))));
 251               [ apply rule (∀#e {S n} (∀z.((S n) + O) =(S (n + O))⇒(S (n + O))= z⇒((S n) + O) =z));
 252                 apply rule (∀#e {(S (n + O))} (∀y.∀z.((S n) + O) =y ⇒ y = z ⇒ ((S n) + O) =z));
 253           apply rule (∀#e {(S n) + O} (∀x.∀y.∀z.x = y ⇒ y = z ⇒ x = z));
 254           apply rule (lem 0 trans);
 255               | apply rule (∀#e {O} (∀m.(S n) + m = (S (n + m))));
 256           apply rule (∀#e {n} (∀n.∀m.(S n) + m = (S (n + m))));
 257           apply rule (lem 0 plus_S);
 258               ]
 259            | apply rule (⇒#e (n + O = n ⇒ (S (n + O)) = (S n)) (n + O = n));
 260               [ apply rule (∀#e {n} (∀w.n + O = w ⇒ (S (n + O)) = (S w)));
 261           apply rule (∀#e {(n + O)} (∀y.∀w.y = w ⇒ (S y) = (S w)));
 262           apply rule (lem 0 eq_S);
 263               | apply rule (discharge [H]);
 264               ]
 265            ]
 266         ]
 267 (*END*)
 268 qed.