natural deduction palette

[helm.git] / helm / software / matita / library / demo / natural_deduction.ma

diff --git a/helm/software/matita/library/demo/natural_deduction.ma b/helm/software/matita/library/demo/natural_deduction.ma
index ba0f565e4baf624030382e6dbaf2d706222eae17..64b3daccbb5fd4f687a421fc7c0c92c123cc5f71 100644 (file)
--- a/helm/software/matita/library/demo/natural_deduction.ma
+++ b/helm/software/matita/library/demo/natural_deduction.ma
@@ -14,16 +14,68 @@
 
 include "demo/natural_deduction_support.ma".
 
-lemma ex1 : ΠA,B,C,E: CProp.
+lemma RAA_to_EM : A ∨ ¬ A.
 
-   (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
+  apply (prove (A ∨ ¬ A));
+  
+  apply (RAA [H] ⊥);
+  apply (¬_e (¬A) A);
+    [ apply (¬_i [H1] ⊥);
+      apply (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply [H];
+      | apply (∨_i_l A);
+        apply [H1];
+      ]
+    | apply (RAA [H2] ⊥);
+      apply (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply [H];
+      | apply (∨_i_r (¬A));
+        apply [H2];
+      ]
+    ]
+qed.
+
+lemma RA_to_EM1 : A ∨ ¬ A.
+
+  apply (prove (A ∨ ¬ A));
+  
+  apply (RAA [H] ⊥);
+  apply (¬_e (¬¬A) (¬A));
+    [ apply (¬_i [H2] ⊥);
+      apply (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply [H];
+      | apply (∨_i_r (¬A));
+        apply [H2];
+      ]
+    | apply (¬_i [H1] ⊥);
+      apply (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply [H];
+      | apply (∨_i_l A);
+        apply [H1];
+      ]
+    ]
+qed.
 
- intros 4 (A B C E);apply (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
+lemma ex0 : (A ⇒ ⊥) ⇒ A ⇒ B ∧ ⊤. 
  
- (*NICE: TRY THIS ERROR! 
- apply (⇒_i [H] (A∧C⇒E∧E∧C∨B));
- apply (⇒_i [K] (E∧E∧C∨B));
-  OR DO THE RIGHT THING *)
+  apply (prove ((A ⇒ ⊥) ⇒ A ⇒ B∧⊤));
+  
+  apply (⇒_i [H] (A ⇒ B∧⊤));
+  apply (⇒_i [H1] (B∧⊤));
+  apply (∧_i B ⊤);
+  [ apply (⊥_e ⊥);
+    apply (⇒_e (A ⇒ ⊥) A); 
+    [ apply [H];
+    | apply [H1];
+    ]
+  | apply (⊤_i);
+  ]
+qed.
+
+lemma ex1 : (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
+
+ apply (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
+   
  apply (⇒_i [H] (A∧C⇒E∧C∨B));
  apply (⇒_i [K] (E∧C∨B));
  apply (∨_e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
@@ -40,6 +92,17 @@ lemma ex1 : ΠA,B,C,E: CProp.
 ]
 qed.
 
+lemma dmg : ¬(A ∨ B) ⇒ ¬A ∧ ¬B.
+
+  apply (prove (¬(A ∨ B) ⇒ ¬A ∧ ¬B));
+  apply (⇒_i [H] (¬A ∧ ¬B));
+  
+  apply (¬_e (¬A) A);
+  
+  
+
+
+(*
 lemma ex2: ΠN:Type.ΠR:N→N→CProp.
 
    (∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y.
@@ -60,3 +123,4 @@ lemma ex2: ΠN:Type.ΠR:N→N→CProp.
      ]
   ]
 qed.
+*)
\ No newline at end of file