From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 24 Nov 2008 18:11:08 +0000 (+0000)
Subject: ....
X-Git-Tag: make_still_working~4510
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ece1166d5202b74ee25bdceef1b4951de979a99b;p=helm.git

....
---

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction1.ma b/helm/software/matita/library/didactic/exercises/natural_deduction1.ma
new file mode 100644
index 000000000..8f90dd67c
--- /dev/null
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction1.ma
@@ -0,0 +1,185 @@
+(* Istruzioni: 
+
+     http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html 
+
+*)
+
+(* Esercizio 0
+   ===========
+
+   Compilare i seguenti campi:
+
+   Nome1: ...
+   Cognome1: ...
+   Matricola1: ...
+   Account1: ...
+
+   Nome2: ...
+   Cognome2: ...
+   Matricola2: ...
+   Account2: ...
+
+*)
+
+include "didactic/support/natural_deduction.ma".
+
+theorem EM: ∀A:CProp. A ∨ ¬ A.
+assume A: CProp.
+apply rule (prove (A ∨ ¬A));
+apply rule (RAA [H] (⊥)).
+apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+	[ apply rule (discharge [H]).
+	| apply rule (⊥_e (⊥));
+	  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]).
+	      ]
+	   | apply rule (¬_i [K] (⊥)).
+       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+	      [ apply rule (discharge [H]).
+	      | apply rule (∨_i_l (A)).
+          apply rule (discharge [K]).
+	      ]
+	   ]
+	]
+qed.
+
+theorem ex0 : (F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E.
+apply rule (prove ((F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
+(*BEGIN*)
+apply rule (⇒_i [h1] ((G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
+apply rule (⇒_i [h2] (F ∧ L ⇒ E));
+apply rule (⇒_i [h3] (E));
+apply rule (∨_e (G∨¬G) [h4] (E) [h4] (E));
+	[ apply rule (lem EM);
+	| apply rule (⇒_e (G∧L⇒E) (G∧L));
+	    [ apply rule (discharge [h2]);
+	    | apply rule (∧_i (G) (L));
+	        [ apply rule (discharge [h4]);
+	        | apply rule (∧_e_r (F∧L));
+	          apply rule (discharge [h3]);
+	        ]
+	    ]
+	| apply rule (⇒_e (L⇒E) (L));
+	    [ apply rule (⇒_e (F∧¬G ⇒ L ⇒ E) (F∧¬G));
+	        [ apply rule (discharge [h1]);
+	        | apply rule (∧_i (F) (¬G));
+	            [ apply rule (∧_e_l (F∧L));
+	              apply rule (discharge [h3]);
+	            | apply rule (discharge [h4]);
+	            ]
+	        ]  
+	    | apply rule (∧_e_r (F∧L));
+	      apply rule (discharge [h3]);
+	    ]
+	]
+(*END*)
+qed.
+
+theorem ex1 : (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 (¬L∨F) [h5] (E) [h5] (E));
+	[ apply rule (discharge [h3]);
+	| apply rule (⊥_e (⊥));
+    apply rule (¬_e (¬L) (L));
+	    [ apply rule (discharge [h5]);
+	    | apply rule (discharge [h4]);
+	    ]
+	| apply rule (∨_e (G∨E) [h6] (E) [h6] (E));
+	   [ apply rule (⇒_e (F⇒G∨E) (F));
+	      [ apply rule (discharge [h1]);
+	      | apply rule (discharge [h5]);
+	      ]
+	   | apply rule (RAA [h7] (⊥));
+       apply rule (¬_e (¬ (L ∧ ¬E)) (L ∧ ¬E));
+	       [ apply rule (⇒_e (G ⇒ ¬ (L ∧ ¬E)) (G));
+	           [apply rule (discharge [h2]);
+	           |apply rule (discharge [h6]);
+	           ]
+	       | apply rule (∧_i (L) (¬E));
+	           [ apply rule (discharge [h4]);
+	           | apply rule (discharge [h7]);
+	           ]
+	       ]
+	   | apply rule (discharge [h6]);
+	   ]
+	]
+(*END*)
+qed.
+
+theorem ex2 : (F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E.
+apply rule (prove ((F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
+(*BEGIN*)
+apply rule (⇒_i [h1] ((H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
+apply rule (⇒_i [h2] ((¬G ⇒ ¬H) ⇒ H ⇒ E));
+apply rule (⇒_i [h3] (H ⇒ E));
+apply rule (⇒_i [h4] (E));
+apply rule (∨_e (G∨¬G) [h5] (E) [h5] (E));
+	[apply rule (lem EM);
+	| apply rule (∨_e (E∨F) [h6] (E) [h6] (E));
+	   [ apply rule (⇒_e (H ⇒ E∨F) (H));
+	       [ apply rule (discharge [h2]);
+	       | apply rule (discharge [h4]);
+	       ]
+	   | apply rule (discharge [h6]);
+	   | apply rule (⇒_e (F∧G ⇒ E) (F∧G));
+	      [apply rule (discharge [h1]);
+	      |apply rule (∧_i (F) (G));
+	        [ apply rule (discharge [h6]);
+	        | apply rule (discharge [h5]);
+	        ]
+	      ]
+	   ]
+	| apply rule (⊥_e (⊥));
+    apply rule (¬_e (¬H) (H));
+    	[ apply rule (⇒_e (¬G ⇒ ¬H) (¬G));
+	       [ apply rule (discharge [h3]);
+	       | apply rule (discharge [h5]);
+	       ]
+	    | apply rule (discharge [h4]);
+	    ]
+	]
+(*END*)
+qed.
+
+theorem ex3 : (F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E.
+apply rule (prove ((F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E)).
+(*BEGIN*)
+apply rule (⇒_i [h1] ((¬E ⇒ G∨¬L) ⇒ (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 (RAA [h5] (⊥));
+apply rule (∨_e (G∨¬L) [h6] (⊥) [h6] (⊥));
+	[ apply rule (⇒_e (¬E ⇒ G∨¬L) (¬E));
+	    [ apply rule (discharge [h2]);
+	    | apply rule (discharge [h5]);
+	    ]
+	| apply rule (¬_e (¬E) (E));
+    	[ apply rule (discharge [h5]);
+	    | apply rule (⇒_e (F∧G ⇒ E) (F∧G));
+	       [ apply rule (discharge [h1]);
+	       | apply rule (∧_i (F) (G));
+	           [ apply rule (⇒_e (L⇒F) (L));
+	              [ apply rule (discharge [h3]);
+	              | apply rule (discharge [h4]);
+	              ]
+	           | apply rule (discharge [h6]);
+	           ]
+	       ]
+	    ]
+	| apply rule (¬_e (¬L) (L));
+	    [ apply rule (discharge [h6]);
+	    | apply rule (discharge [h4]);
+	    ]
+	]
+(*END*)
+qed.
\ No newline at end of file