From 99b5244c1c9406c3e048db6eeedbe0d129a775bd Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 17 Nov 2008 11:44:55 +0000
Subject: [PATCH] all ex done

---
 .../didactic/exercises/natural_deduction.ma   | 281 ++++++++++++++++--
 1 file changed, 248 insertions(+), 33 deletions(-)

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 052e00679..98142db2f 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -15,12 +15,72 @@
 
 *)
 
+(*DOCBEGIN
+
+I connettivi logici
+===================
+
+Per digitare i connettivi logici:
+
+* `∧` : `\land`
+* `∨` : `\lor`
+* `¬` : `\lnot`
+* `⇒` : `=>`, `\Rightarrow` 
+* `⊥` : `\bot`
+* `⊤` : `\top`
+
+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.
+
+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 `]`.  
+
+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.
+
+DOCEND*)
 
 include "didactic/support/natural_deduction.ma".
 
 theorem EM: ∀A. A ∨ ¬ A.
+(* Il comando assume è necessario perchè dimostriamo A∨¬A
+   per una A generica. *)
 assume A: CProp.
 apply rule (prove (A ∨ ¬A));
+
 apply rule (RAA [H] (⊥)).
 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
 	[ apply rule (discharge [H]).
@@ -28,47 +88,202 @@ apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
 	  apply rule (¬_e (¬¬A) (¬A));
 	   [ apply rule (¬_i [K] (⊥)).
        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
-	      [ apply rule (discharge [H]).
-	      | apply rule (∨_i_r (¬A)).
-          apply rule (discharge [K]).
+	      [ (*BEGIN*)apply rule (discharge [H]).(*END*)
+	      | (*BEGIN*)apply rule (∨_i_r (¬A)).
+          apply rule (discharge [K]).(*END*)
 	      ]
-	   | apply rule (¬_i [K] (⊥)).
+	   | (*BEGIN*)apply rule (¬_i [K] (⊥)).
        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
 	      [ apply rule (discharge [H]).
 	      | apply rule (∨_i_l (A)).
           apply rule (discharge [K]).
-	      ]
+	      ](*END*)
 	   ]
 	]
 qed.
 
-(*
-theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
-apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
-apply rule (⇒_i [H] (¬A ∨ ¬B));
-apply rule (RAA [K] (⊥));
-apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
-	[ apply rule (discharge [K]).
+theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
+apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
+(*BEGIN*)
+apply rule (⇒_i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
+apply rule (⇒_i [h2] (G ∨ L ⇒ ¬L ⇒ E));
+apply rule (⇒_i [h3] (¬L ⇒ E));
+apply rule (⇒_i [h4] (E));
+apply rule (∨_e (G∨L) [h5] (E) [h6] (E));
+	[ apply rule (discharge [h3]);
+	| apply rule (∨_e (E∨C) [h6] (E) [h7] (E));
+	    [ apply rule (⇒_e (¬L ⇒ E∨C) (¬L));
+	        [ apply rule (discharge [h2]);
+	        | apply rule (discharge [h4]);
+	        ]
+	    | apply rule (discharge [h6]);
+	    | apply rule (⇒_e (C∧G ⇒ E) (C∧G));
+	        [ apply rule (discharge [h1]);
+	        | apply rule (∧_i (C) (G));
+	            [ apply rule (discharge [h7]);
+	            | apply rule (discharge [h5]);
+             	]
+	        ]
+	    ]
+	| apply rule (⊥_e (⊥));
+	  apply rule (¬_e (¬L) (L));
+	    [ apply rule (discharge [h4]);
+	    | apply rule (discharge [h6]);
+	    ]
+	]
+(*END*)
+qed.
+
+theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
+apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
+(*BEGIN*)
+apply rule (⇒_i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
+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 (⇒_e (B∧D⇒C) (B∧D));
+	    [ apply rule (discharge [h2]);
+    	| apply rule (∧_i (B) (D));
+	        [ apply rule (discharge [h5]);
+	        | apply rule (discharge [h4]);
+	        ]
+	    ] 
+	| apply rule (⇒_e (A∧¬B⇒C) (A∧¬B));
+	    [ apply rule (discharge [h1]);
+	    | apply rule (∧_i (A) (¬B));
+	        [ apply rule (⇒_e (D⇒A) (D));
+	            [ apply rule (discharge [h3]);
+	            | apply rule (discharge [h4]);
+	            ]
+	        | apply rule (discharge [h6]);
+	        ]
+	    ]
+	]
+(*END*)
+qed.
+
+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*)
+apply rule (⇒_i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
+apply rule (⇒_i [h2] ((L⇒F) ⇒ L ⇒ E));
+apply rule (⇒_i [h3] (L ⇒ E));
+apply rule (⇒_i [h4] (E));
+apply rule (∨_e (G∨E) [h5] (E) [h6] (E));
+	[ apply rule (⇒_e (F ⇒ G∨E) (F));
+	    [ apply rule (discharge [h1]);
+	    | apply rule (⇒_e (L⇒F) (L));
+	        [ apply rule (discharge [h3]);
+	        | apply rule (discharge [h4]);
+	        ]
+	    ]
+	|apply rule (∨_e (¬L∨E) [h7] (E) [h8] (E));
+	    [ apply rule (⇒_e (G⇒¬L∨E) (G));
+	        [ apply rule (discharge [h2]);
+	        | apply rule (discharge [h5]);
+	        ]
+	    | apply rule (⊥_e (⊥));
+        apply rule (¬_e (¬L) (L));
+	        [ apply rule (discharge [h7]);
+	        | apply rule (discharge [h4]);
+	        ]
+	    | apply rule (discharge [h8]);
+	    ]
+	| apply rule (discharge [h6]);
+	]
+(*END*)
+qed.
+
+theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
+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 (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
+	    [ apply rule (lem EM);
+	    | apply rule (⊥_e (⊥));
+	      apply rule (¬_e (¬(A∧B)) (A∧B));
+	        [ apply rule (discharge [h1]);
+	        | apply rule (∧_i (A) (B));
+	            [ apply rule (discharge [h2]);
+	            | apply rule (discharge [h4]);
+	            ]
+	        ]
+	    | apply rule (∨_i_r (¬B));
+        apply rule (discharge [h5]);
+	    ]
 	| apply rule (∨_i_l (¬A));
-	  apply rule (¬_i [L] (⊥)).
-	  apply rule (¬_e (¬B) (B));
-	   [ apply rule (¬_i [M] (⊥)).
-       apply rule (¬_e (¬(A ∧ B)) (A ∧ B));
-	      [ apply rule (discharge [H]).
-	      | apply rule (∧_i (A) (B));
-	         [ apply rule (discharge [L]).
-	         | apply rule (discharge [M]).
-	         ]
-	      ]
-	   | apply rule (∨_e (B ∨ ¬B) [h1] (B) [h2] (B));
-	       [ apply rule (lem EM);
-	       
-
-	       | apply rule (discharge [h1]);
-	       |
-	       ]
- 
-	   apply rule (show EM);
-	   ]
+    apply rule (discharge [h3]);
 	]
-*)
\ No newline at end of file
+(*END*)
+qed.
+
+theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
+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 (⊥_e (⊥));
+    apply rule (¬_e (¬(A∨B)) (A∨B));
+	    [ apply rule (discharge [h1]);
+	    | apply rule (∨_i_l (A));
+        apply rule (discharge [h2]);
+	    ]
+	| apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
+	    [ apply rule (lem EM);
+	    | apply rule (⊥_e (⊥));
+        apply rule (¬_e (¬(A∨B)) (A∨B));
+	        [ apply rule (discharge [h1]);
+	        | apply rule (∨_i_r (B));
+            apply rule (discharge [h10]);
+	        ] 
+	    | apply rule (∧_i (¬A) (¬B));
+	        [ apply rule (discharge [h3]);
+	        |apply rule (discharge [h11]);
+	        ]
+	    ]
+	]
+(*END*)
+qed.
+
+theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
+apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
+(*BEGIN*)
+apply rule (⇒_i [h1] (¬(A∨B)));
+apply rule (¬_i [h2] (⊥));
+apply rule (∨_e (A∨B) [h3] (⊥) [h3] (⊥));
+	[ apply rule (discharge [h2]);
+	| apply rule (¬_e (¬A) (A));
+	    [ apply rule (∧_e_l (¬A∧¬B));
+        apply rule (discharge [h1]);
+	    | apply rule (discharge [h3]);
+	    ]
+	| apply rule (¬_e (¬B) (B));
+	    [ apply rule (∧_e_r (¬A∧¬B));
+        apply rule (discharge [h1]);
+	    | apply rule (discharge [h3]);
+	    ]
+	]
+(*END*)
+qed.
+
+theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
+apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
+(*BEGIN*)
+apply rule (⇒_i [h1] (A));
+apply rule (RAA [h2] (⊥));
+apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
+	[ apply rule (discharge [h1]);
+	| apply rule (⇒_i [h3] (⊥));
+	  apply rule (¬_e (¬A) (A));
+	    [ apply rule (discharge [h2]);
+	    | apply rule (discharge [h3]);
+	    ]
+	]
+(*END*)
+qed. 
+
-- 
2.39.2