1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "demo/natural_deduction_support.ma".
17 lemma ex1 : ΠA,B,C,E: CProp.
19 (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
21 intros 4 (A B C E);apply (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
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));
31 | apply (∨_i_l (E∧C));
33 [ apply (⇒_e (A⇒E) A);
35 | apply (∧_e_l (A∧C)); apply [K];
37 | apply (∧_e_r (A∧C)); apply [K];
39 | apply (∨_i_r B); apply [C2];
43 lemma ex2: ΠN:Type.ΠR:N→N→CProp.
45 (∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y.
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));
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));
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);