(* *)
(**************************************************************************)
-include "demo/natural_deduction_support.ma".
-
-lemma ex1 : ΠA,B,C,E: CProp.
-
- (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
-
- intros 4 (A B C E);apply (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨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 (⇒_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));
-[ apply [H];
-| apply (∨_i_l (E∧C));
- apply (∧_i E C);
- [ apply (⇒_e (A⇒E) A);
- [ apply [C1];
- | apply (∧_e_l (A∧C)); apply [K];
+include "didactic/support/natural_deduction.ma".
+
+lemma RAA_to_EM : A ∨ ¬ A.
+
+ apply rule (prove (A ∨ ¬ A));
+
+ apply rule (RAA [H] ⊥);
+ apply rule (¬_e (¬A) A);
+ [ apply rule (¬_i [H1] ⊥);
+ apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+ [ apply rule (discharge [H]);
+ | apply rule (∨_i_l A);
+ apply rule (discharge [H1]);
+ ]
+ | apply rule (RAA [H2] ⊥);
+ apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+ [ apply rule (discharge [H]);
+ | apply rule (∨_i_r (¬A));
+ apply rule (discharge [H2]);
+ ]
]
- | apply (∧_e_r (A∧C)); apply [K];
- ]
-| apply (∨_i_r B); apply [C2];
-]
qed.
-lemma ex2: ΠN:Type.ΠR:N→N→CProp.
+lemma RA_to_EM1 : A ∨ ¬ A.
- (∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y.
+ apply rule (prove (A ∨ ¬ A));
+
+ apply rule (RAA [H] ⊥);
+ apply rule (¬_e (¬¬A) (¬A));
+ [ apply rule (¬_i [H2] ⊥);
+ apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+ [ apply rule (discharge [H]);
+ | apply rule (∨_i_r (¬A));
+ apply rule (discharge [H2]);
+ ]
+ | apply rule (¬_i [H1] ⊥);
+ apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+ [ apply rule (discharge [H]);
+ | apply rule (∨_i_l A);
+ apply rule (discharge [H1]);
+ ]
+ ]
+qed.
+
+lemma ex1 : (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
+
+ apply rule (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
- 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));
-
- apply (⇒_i [H] (∀z:N.(∃x:N.R x z)⇒∃y:N.R z y));
- apply (∀_i [z] ((∃x:N.R x z)⇒∃y:N.R z y));
- apply (⇒_i [H2] (∃y:N.R z y));
- apply (∃_e (∃x:N.R x z) [n] [H3] (∃y:N.R z y));
- [ apply [H2]
- | apply (∃_i n (R z n));
- apply (⇒_e (R n z ⇒ R z n) (R n z));
- [ apply (∀_e (∀b:N.R n b ⇒ R b n) z);
- apply (∀_e (∀a:N.∀b:N.R a b ⇒ R b a) n);
- apply [H]
- | apply [H3]
- ]
+ apply rule (⇒_i [H] (A∧C⇒E∧C∨B));
+ apply rule (⇒_i [K] (E∧C∨B));
+ apply rule (∨_e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
+[ apply rule (discharge [H]);
+| apply rule (∨_i_l (E∧C));
+ apply rule (∧_i E C);
+ [ apply rule (⇒_e (A⇒E) A);
+ [ apply rule (discharge [C1]);
+ | apply rule (∧_e_l (A∧C)); apply rule (discharge [K]);
+ ]
+ | apply rule (∧_e_r (A∧C)); apply rule (discharge [K]);
]
+| apply rule (∨_i_r B); apply rule (discharge [C2]);
+]
qed.
+