From: Claudio Sacerdoti Coen Date: Sat, 15 Nov 2008 15:45:52 +0000 (+0000) Subject: New bug. X-Git-Tag: make_still_working~4550 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eba5539fdc38fc8aef80b38dc46a74bd8eec09b5;p=helm.git New bug. --- 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; + ] ]