From eba5539fdc38fc8aef80b38dc46a74bd8eec09b5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 15 Nov 2008 15:45:52 +0000 Subject: [PATCH] New bug. --- .../didactic/exercises/natural_deduction.ma | 35 ++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma index c26fcb6e8..7d4e1ff11 100644 --- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma +++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma @@ -18,7 +18,28 @@ include "didactic/support/natural_deduction.ma". - +theorem EM: ∀A. A ∨ ¬ A. +assume A: CProp. +apply rule (prove (A ∨ ¬A)); +apply rule (RAA [H] (⊥)). +apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A)); + [ apply rule (discharge [H]). + | apply rule (¬_e (¬¬A) (¬A)); + [ apply rule (¬_i [K] (⊥)). + apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A)); + [ apply rule (discharge [H]). + | apply rule (∨_i_r (¬A)). + apply rule (discharge [K]). + ] + | apply rule (¬_i [K] (⊥)). + apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A)); + [ apply rule (discharge [H]). + | apply rule (∨_i_l (A)). + apply rule (discharge [K]). + ] + ] + ] +qed. theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B. apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B)); @@ -27,4 +48,16 @@ apply rule (RAA [K] (⊥)); apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B)); [ apply rule (discharge [K]). | apply rule (∨_i_l (¬A)); + apply rule (¬_i [L] (⊥)). + apply rule (¬_e (¬B) (B)); + [ apply rule (¬_i [M] (⊥)). + apply rule (¬_e (¬(A ∧ B)) (A ∧ B)); + [ apply rule (discharge [H]). + | apply rule (∧_i (A) (B)); + [ apply rule (discharge [L]). + | apply rule (discharge [M]). + ] + ] + | apply rule EM; + ] ] -- 2.39.2