From 01d82c5e0c4f01881aeb746062438dcc3d05bc29 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 8 Dec 2008 23:56:26 +0000 Subject: [PATCH] A (boring and long) once-in-a-life exercise on proving a trivial property on natural numbers in ND. --- .../exercises/natural_deduction_theories.ma | 220 ++++++++++++++++++ 1 file changed, 220 insertions(+) create mode 100644 helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma new file mode 100644 index 000000000..38d28c83c --- /dev/null +++ b/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma @@ -0,0 +1,220 @@ +(* Esercizio 0 + =========== + + Compilare i seguenti campi: + + Nome1: ... + Cognome1: ... + Matricola1: ... + Account1: ... + + Nome2: ... + Cognome2: ... + Matricola2: ... + Account2: ... + +*) + +(*DOCBEGIN + +I connettivi logici +=================== + +Per digitare i connettivi logici: + +* `∧` : `\land` +* `∨` : `\lor` +* `¬` : `\lnot` +* `⇒` : `=>`, `\Rightarrow` +* `⊥` : `\bot` +* `⊤` : `\top` + +Per digitare i quantificatori: + +* `∀` : `\forall` +* `∃` : `\exists` + +I termini, le formule e i nomi delle ipotesi +============================================ + +* I termini quantificati da `∀` e `∃`, quando argomenti di + una regola, vengono scritti tra `{` e `}`. + +* Le formule, quando argomenti di + una regola, vengono scritte tra `(` e `)`. + +* I nomi delle ipotesi, quando argomenti di + una regola, vengono scritti tra `[` e `]`. + +Le regole di deduzione naturale +=============================== + +Per digitare le regole di deduzione naturale +è possibile utilizzare la palette che compare +sulla sinistra dopo aver premuto `F2`. + +L'albero si descrive partendo dalla radice. Le regole +con premesse multiple sono seguite da `[`, `|` e `]`. +Ad esempio: + + apply rule (∧_i (A∨B) ⊥); + [ …continua qui il sottoalbero per (A∨B) + | …continua qui il sottoalbero per ⊥ + ] + +Le regole vengono applicate alle loro premesse, ovvero +gli argomenti delle regole sono le formule che normalmente +scrivete sopra la linea che rappresenta l'applicazione della +regola stessa. Ad esempio: + + apply rule (∨_e (A∨B) [h1] C [h2] C); + [ …prova di (A∨B) + | …prova di C sotto l'ipotesi A (di nome h1) + | …prova di C sotto l'ipotesi B (di nome h2) + ] + +Le regole che hanno una sola premessa non vengono seguite +da parentesi quadre. + +L'albero di deduzione +===================== + +Per visualizzare l'albero man mano che viene costruito +dai comandi impartiti al sistema, premere `F3` e poi +premere sul bottome home (in genere contraddistinto da +una icona rappresentate una casa). + +Si suggerisce di marcare tale finestra come `always on top` +utilizzando il menu a tendina che nella maggior parte degli +ambienti grafici si apre cliccando nel suo angolo in +alto a sinistra. + +Applicazioni di regole errate vengono contrassegnate con +il colore rosso. + +Usare i lemmi dimostrati in precedenza +====================================== + +Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile +riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`. + +La "regola" `lem` prende come argomenti: + +- Il numero delle ipotesi del lemma che si vuole utilizzare, nel + caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`. + +- Dopo il numero di ipotesi, è necessario digitare il nome del lemma. + +- Infine, le formule che devono essere scritte come premesse per la + "regola". + +Ad esempio, per usare il lemma EM (terzo escluso) basta digitare +`lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare +`lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario +far seguire le parentesi quadre come spiegato in precedenza. + +Si noti che "regola" `lem` non è una vera regola, ma una forma compatta +per rappresentare l'albero di prova del lemma che si sta riutilizzando. + +Per motivi che saranno più chiari una volta studiate logiche del +primo ordine o di ordine superiore, i lemmi che si intende +riutilizzare è bene che siano dimostrati astratti sugli atomi. +Ovvero per ogni atomo `A`...`Z` che compare nella formula, +è bene aggiungere una quantificazione all'inizio della formula stessa. +Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`. +La dimostrazione deve poi iniziare con il comando `assume`. + +In tale modo il lemma EM può essere utilizzato sia per dimostrare +`A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ... + +DOCEND*) + +include "nat/plus.ma". + +lemma ex0: ∀n. n + O = n. + assume n: nat. + we proceed by induction on n to prove (n + O = n). + case O. + the thesis becomes (O + O = O). + conclude + (O + O) + = O + done. + case S (n:nat). + by induction hypothesis we know (n + O = n) (H). + the thesis becomes (S n + O = S n). + conclude + (S n + O) + = (S (n + O)). + = (S n) by H + done. +qed. + +include "didactic/support/natural_deduction.ma". + +(* Il nostro linguaggio del primo ordine prevede le seguenti + - costanti: O + - funzioni: S (unaria), plus, mult (binarie) + - predicati: eq (binari) +*) +axiom O : sort. (* zero *) +axiom S : sort → sort. (* successore *) +axiom plus : sort → sort → sort. (* addizione *) +axiom mult: sort → sort → sort. (* moltiplicazione *) +axiom eq : sort → sort → CProp. (* uguaglianza *) + +(* Assumiamo la seguente teoria *) + +(* l'uguaglianza e' una relazione d'equivalenza *) +axiom refl: ∀x. eq x x. +axiom sym: ∀x.∀y. eq x y ⇒ eq y x. +axiom trans: ∀x.∀y.∀z. eq x y ⇒ eq y z ⇒ eq x z. + +(* assiomi di Peano *) +axiom discr: ∀x. ¬ eq O (S x). +axiom inj: ∀x.∀y. eq (S x) (S y) ⇒ eq x y. +axiom induct: ΠP. P O ⇒ (∀n. P n ⇒ P (S n)) ⇒ ∀x. P x. + +(* definizione ricorsiva di addizione *) +axiom plus_O: ∀x. eq (plus O x) x. +axiom plus_S: ∀x.∀y. eq (plus (S x) y) (S (plus x y)). + +(* definizione ricorsiva di moltiplicazione *) +axiom mult_O: ∀x.eq (mult O x) O. +axiom mult_S: ∀x.∀y. eq (mult (S x) y) (plus (mult x y) y). + +(* l'uguaglianza e' una congruenza rispetto a tutte le funzioni e predicati *) +axiom eq_S: ∀x.∀x'. eq x x' ⇒ eq (S x) (S x'). +axiom eq_plus: ∀x.∀x'.∀y.∀y'. eq x x' ⇒ eq y y' ⇒ eq (plus x y) (plus x' y'). +axiom eq_mult: ∀x.∀x'.∀y.∀y'. eq x x' ⇒ eq y y' ⇒ eq (mult x y) (mult x' y'). + +(* intuizionista *) +lemma ex1: ∀x.eq (plus x O) x. +apply rule (prove (∀x.eq (plus x O) x)); +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))); + [ 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)); + [ apply rule (lem 0 induct); + | apply rule (∀_e {O} (∀y.eq (plus O y) y)); + apply rule (lem 0 plus_O); + ] + | apply rule (∀_i {n} (eq (plus n O) n ⇒ eq (plus (S n) O) (S n))); + apply rule (⇒_i [H] (eq (plus (S n) O) (S n))); + apply rule (⇒_e (eq (S (plus n O)) (S n) ⇒ eq (plus (S n) O) (S n)) (eq (S (plus n O)) (S n))); + [ 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)))); + [ 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)); + apply rule (∀_e {(S (plus n O))} (∀y.∀z.eq (plus (S n) O) y ⇒ eq y z ⇒ eq (plus (S n) O) z)); + apply rule (∀_e {plus (S n) O} (∀x.∀y.∀z.eq x y ⇒ eq y z ⇒ eq x z)); + apply rule (lem 0 trans); + | apply rule (∀_e {O} (∀m.eq (plus (S n) m) (S (plus n m)))); + apply rule (∀_e {n} (∀n.∀m.eq (plus (S n) m) (S (plus n m)))); + apply rule (lem 0 plus_S); + ] + | apply rule (⇒_e (eq (plus n O) n ⇒ eq (S (plus n O)) (S n)) (eq (plus n O) n)); + [ apply rule (∀_e {n} (∀w.eq (plus n O) w ⇒ eq (S (plus n O)) (S w))); + apply rule (∀_e {(plus n O)} (∀y.∀w.eq y w ⇒ eq (S y) (S w))); + apply rule (lem 0 eq_S); + | apply rule (discharge [H]); + ] + ] + ] +qed. \ No newline at end of file -- 2.39.2