commented out unfinished proof

[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 c26fcb6e88d0585ee07340a0b3839ab5cc39a571..052e00679c98ca5e5fef8018bc46d69d8b610f9b 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -18,8 +18,31 @@
 
 include "didactic/support/natural_deduction.ma".
 
+theorem EM: ∀A. 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 demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
 apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
 apply rule (⇒_i [H] (¬A ∨ ¬B));
@@ -27,4 +50,25 @@ apply rule (RAA [K] (⊥));
 apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
        [ apply rule (discharge [K]).
        | 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);
+          ]
        ]
+*)
\ No newline at end of file