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

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