X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fnatural_deduction.ma;h=feac0296dd456259de8dd7246b3748032af6d364;hb=f524a0d716de2bdc0874aace8f82f6289034eccf;hp=98142db2fd7f19ea8462c81839918798f538f8c2;hpb=99b5244c1c9406c3e048db6eeedbe0d129a775bd;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 98142db2f..feac0296d 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -1,3 +1,23 @@
+(**************************************************************************)
+(*       ___	                                                          *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* Istruzioni: 
+
+     http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html 
+
+*)
+
 (* Esercizio 0
    ===========
 
@@ -17,6 +37,16 @@
 
 (*DOCBEGIN
 
+Scopo della lezione
+===================
+
+Lo scopo della lezione è di farvi imparare ad usare Matita
+per auto-correggervi gli esercizi di deduzione naturale, che
+saranno parte dell'esame scritto. Il consiglio è di 
+fare prima gli esercizi su carta e poi digitarli in Matita
+per verificarne la correttezza. Fare direttamente gli esercizi
+con Matita è difficile e richiede molto più tempo.
+
 I connettivi logici
 ===================
 
@@ -29,6 +59,15 @@ Per digitare i connettivi logici:
 * `⊥` : `\bot`
 * `⊤` : `\top`
 
+I termini, le formule e i nomi delle ipotesi
+============================================
+
+* 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
 ===============================
 
@@ -38,7 +77,7 @@ sulla sinistra dopo aver premuto `F2`.
 
 L'albero si descrive partendo dalla radice. Le regole
 con premesse multiple sono seguite da `[`, `|` e `]`.
-Ad esempio 
+Ad esempio: 
 
         apply rule (∧_i (A∨B) ⊥);
           [ …continua qui il sottoalbero per (A∨B)
@@ -48,12 +87,16 @@ Ad esempio
 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.
+regola stessa. Ad esempio:
+
+        aply 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 formule sono racchiuse tra `(` e `)`, mentre i nomi
-che date ad ipotesi aggiuntive (nella regola di eliminazione
-dell' OR, in RAA, e nella regola di introduzione 
-dell'implicazione) sono ragghiusi tra `[` e `]`.  
+Le regole che hanno una sola premessa non vengono seguite 
+da parentesi quadre.
 
 L'albero di deduzione
 =====================
@@ -71,16 +114,53 @@ 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 "didactic/support/natural_deduction.ma".
 
-theorem EM: ∀A. A ∨ ¬ A.
+theorem EM: ∀A:CProp. A ∨ ¬ A.
 (* Il comando assume è necessario perchè dimostriamo A∨¬A
    per una A generica. *)
 assume A: CProp.
+(* Questo comando inizia a disegnare l'albero *)
 apply rule (prove (A ∨ ¬A));
-
+(* qui inizia l'albero, eseguite passo passo osservando come
+   si modifica l'albero. *)
 apply rule (RAA [H] (⊥)).
 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
 	[ apply rule (discharge [H]).
@@ -142,7 +222,7 @@ apply rule (⇒_i [h2] ((D ⇒ A) ⇒ D ⇒ C));
 apply rule (⇒_i [h3] (D ⇒ C));
 apply rule (⇒_i [h4] (C));
 apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
-	[ apply rule (lem EM);
+	[ apply rule (lem 0 EM);
 	| apply rule (⇒_e (B∧D⇒C) (B∧D));
 	    [ apply rule (discharge [h2]);
     	| apply rule (∧_i (B) (D));
@@ -164,6 +244,8 @@ apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
 (*END*)
 qed.
 
+(* Per dimostrare questo teorema torna comodo il lemma EM
+   dimostrato in precedenza. *)
 theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
 apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
 (*BEGIN*)
@@ -201,9 +283,9 @@ apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
 (*BEGIN*)
 apply rule (⇒_i [h1] (¬A∨¬B));
 apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
-	[ apply rule (lem EM);
+	[ apply rule (lem 0 EM);
 	| apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
-	    [ apply rule (lem EM);
+	    [ apply rule (lem 0 EM);
 	    | apply rule (⊥_e (⊥));
 	      apply rule (¬_e (¬(A∧B)) (A∧B));
 	        [ apply rule (discharge [h1]);
@@ -226,7 +308,7 @@ apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
 (*BEGIN*)
 apply rule (⇒_i [h1] (¬A ∧ ¬B));
 apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
-	[ apply rule (lem EM);
+	[ apply rule (lem 0 EM);
 	| apply rule (⊥_e (⊥));
     apply rule (¬_e (¬(A∨B)) (A∨B));
 	    [ apply rule (discharge [h1]);
@@ -234,7 +316,7 @@ apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
         apply rule (discharge [h2]);
 	    ]
 	| apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
-	    [ apply rule (lem EM);
+	    [ apply rule (lem 0 EM);
 	    | apply rule (⊥_e (⊥));
         apply rule (¬_e (¬(A∨B)) (A∨B));
 	        [ apply rule (discharge [h1]);
@@ -285,5 +367,5 @@ apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
 	    ]
 	]
 (*END*)
-qed. 
+qed.