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 ex1 : ΠA,B,C,E: CProp.
  18
  19    (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
  20
  21  intros 4 (A B C E);apply (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
  22
  23  (*NICE: TRY THIS ERROR!
  24  apply (⇒_i [H] (A∧C⇒E∧E∧C∨B));
  25  apply (⇒_i [K] (E∧E∧C∨B));
  26   OR DO THE RIGHT THING *)
  27  apply (⇒_i [H] (A∧C⇒E∧C∨B));
  28  apply (⇒_i [K] (E∧C∨B));
  29  apply (∨_e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
  30 [ apply [H];
  31 | apply (∨_i_l (E∧C));
  32   apply (∧_i E C);
  33   [ apply (⇒_e (A⇒E) A);
  34     [ apply [C1];
  35     | apply (∧_e_l (A∧C)); apply [K];
  36     ]
  37   | apply (∧_e_r (A∧C)); apply [K];
  38   ]
  39 | apply (∨_i_r B); apply [C2];
  40 ]
  41 qed.
  42
  43 lemma ex2: ΠN:Type.ΠR:N→N→CProp.
  44
  45    (∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y.
  46
  47  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));
  48
  49  apply (⇒_i [H] (∀z:N.(∃x:N.R x z)⇒∃y:N.R z y));
  50  apply (∀_i [z] ((∃x:N.R x z)⇒∃y:N.R z y));
  51  apply (⇒_i [H2] (∃y:N.R z y));
  52  apply (∃_e (∃x:N.R x z) [n] [H3] (∃y:N.R z y));
  53   [ apply [H2]
  54   | apply (∃_i n (R z n));
  55     apply (⇒_e (R n z ⇒ R z n) (R n z));
  56      [ apply (∀_e (∀b:N.R n b ⇒ R b n) z);
  57        apply (∀_e (∀a:N.∀b:N.R a b ⇒ R b a) n);
  58        apply [H]
  59      | apply [H3]
  60      ]
  61   ]
  62 qed.