helm/software/matita/library/demo/natural_deduction.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "demo/natural_deduction_support.ma".
  16
  17 lemma RAA_to_EM : A ∨ ¬ A.
  18
  19   apply (prove (A ∨ ¬ A));
  20
  21   apply (RAA [H] ⊥);
  22   apply (¬_e (¬A) A);
  23     [ apply (¬_i [H1] ⊥);
  24       apply (¬_e (¬(A∨¬A)) (A∨¬A));
  25       [ apply [H];
  26       | apply (∨_i_l A);
  27         apply [H1];
  28       ]
  29     | apply (RAA [H2] ⊥);
  30       apply (¬_e (¬(A∨¬A)) (A∨¬A));
  31       [ apply [H];
  32       | apply (∨_i_r (¬A));
  33         apply [H2];
  34       ]
  35     ]
  36 qed.
  37
  38 lemma RA_to_EM1 : A ∨ ¬ A.
  39
  40   apply (prove (A ∨ ¬ A));
  41
  42   apply (RAA [H] ⊥);
  43   apply (¬_e (¬¬A) (¬A));
  44     [ apply (¬_i [H2] ⊥);
  45       apply (¬_e (¬(A∨¬A)) (A∨¬A));
  46       [ apply [H];
  47       | apply (∨_i_r (¬A));
  48         apply [H2];
  49       ]
  50     | apply (¬_i [H1] ⊥);
  51       apply (¬_e (¬(A∨¬A)) (A∨¬A));
  52       [ apply [H];
  53       | apply (∨_i_l A);
  54         apply [H1];
  55       ]
  56     ]
  57 qed.
  58
  59 lemma ex0 : (A ⇒ ⊥) ⇒ A ⇒ B ∧ ⊤.
  60
  61   apply (prove ((A ⇒ ⊥) ⇒ A ⇒ B∧⊤));
  62
  63   apply (⇒_i [H] (A ⇒ B∧⊤));
  64   apply (⇒_i [H1] (B∧⊤));
  65   apply (∧_i B ⊤);
  66   [ apply (⊥_e ⊥);
  67     apply (⇒_e (A ⇒ ⊥) A);
  68     [ apply [H];
  69     | apply [H1];
  70     ]
  71   | apply (⊤_i);
  72   ]
  73 qed.
  74
  75 lemma ex1 : (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
  76
  77  apply (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
  78
  79  apply (⇒_i [H] (A∧C⇒E∧C∨B));
  80  apply (⇒_i [K] (E∧C∨B));
  81  apply (∨_e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
  82 [ apply [H];
  83 | apply (∨_i_l (E∧C));
  84   apply (∧_i E C);
  85   [ apply (⇒_e (A⇒E) A);
  86     [ apply [C1];
  87     | apply (∧_e_l (A∧C)); apply [K];
  88     ]
  89   | apply (∧_e_r (A∧C)); apply [K];
  90   ]
  91 | apply (∨_i_r B); apply [C2];
  92 ]
  93 qed.
  94
  95 lemma dmg : ¬(A ∨ B) ⇒ ¬A ∧ ¬B.
  96
  97   apply (prove (¬(A ∨ B) ⇒ ¬A ∧ ¬B));
  98   apply (⇒_i [H] (¬A ∧ ¬B));
  99
 100   apply (¬_e (¬A) A);
 101
 102
 103
 104
 105 (*
 106 lemma ex2: ΠN:Type.ΠR:N→N→CProp.
 107
 108    (∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y.
 109
 110  intros (N R);apply (prove ((∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y));
 111
 112  apply (⇒_i [H] (∀z:N.(∃x:N.R x z)⇒∃y:N.R z y));
 113  apply (∀_i [z] ((∃x:N.R x z)⇒∃y:N.R z y));
 114  apply (⇒_i [H2] (∃y:N.R z y));
 115  apply (∃_e (∃x:N.R x z) [n] [H3] (∃y:N.R z y));
 116   [ apply [H2]
 117   | apply (∃_i n (R z n));
 118     apply (⇒_e (R n z ⇒ R z n) (R n z));
 119      [ apply (∀_e (∀b:N.R n b ⇒ R b n) z);
 120        apply (∀_e (∀a:N.∀b:N.R a b ⇒ R b a) n);
 121        apply [H]
 122      | apply [H3]
 123      ]
 124   ]
 125 qed.
 126 *)