From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 8 Dec 2008 23:56:26 +0000 (+0000)
Subject: A (boring and long) once-in-a-life exercise on proving a trivial property
X-Git-Tag: make_still_working~4432
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=01d82c5e0c4f01881aeb746062438dcc3d05bc29;p=helm.git

A (boring and long) once-in-a-life exercise on proving a trivial property
on natural numbers in ND.
---

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