natural deduction support for lemmas with premises

[helm.git] / helm / software / matita / library / didactic / exercises / natural_deduction.ma

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 5e71888149f9047fcab44fe45da3a8a8798e9c56..1bc9717fd5ec7966d41efcf09d674705955e012d 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -1,3 +1,9 @@
+(* Istruzioni: 
+
+     http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html 
+
+*)
+
 (* Esercizio 0
    ===========
 
@@ -17,6 +23,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
 ===================
 
@@ -32,11 +48,8 @@ Per digitare i connettivi logici:
 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 scritti tra `(` e `)`.
+  una regola, vengono scritte tra `(` e `)`.
 
 * I nomi delle ipotesi, quando argomenti di
   una regola, vengono scritti tra `[` e `]`.
@@ -50,7 +63,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)
@@ -60,12 +73,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
 =====================
@@ -91,8 +108,10 @@ 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]).
@@ -154,7 +173,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));
@@ -176,6 +195,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*)
@@ -213,9 +234,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]);
@@ -238,7 +259,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]);
@@ -246,7 +267,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]);
@@ -297,5 +318,5 @@ apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
            ]
        ]
 (*END*)
-qed. 
+qed.