From e189bde1e0a562e8689ff41d55d392431609e749 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 15 Nov 2008 17:26:07 +0000 Subject: [PATCH] apply rule (lem EM) works --- .../didactic/exercises/natural_deduction.ma | 13 +- .../didactic/support/natural_deduction.ma | 47 ++++++- helm/software/matita/matita.glade | 120 ++++++++++-------- helm/software/matita/matitaGui.ml | 2 + 4 files changed, 121 insertions(+), 61 deletions(-) diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma index 7d4e1ff11..de1c1f482 100644 --- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma +++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma @@ -24,7 +24,8 @@ 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 (⊥_e (⊥)); + apply rule (¬_e (¬¬A) (¬A)); [ apply rule (¬_i [K] (⊥)). apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A)); [ apply rule (discharge [H]). @@ -58,6 +59,14 @@ apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B)); | apply rule (discharge [M]). ] ] - | apply rule EM; + | apply rule (∨_e (B ∨ ¬B) [h1] (B) [h2] (B)); + [ apply rule (lem EM); + + + | apply rule (discharge [h1]); + | + ] + + apply rule (show EM); ] ] diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma index 8a7399167..9ae03f502 100644 --- a/helm/software/matita/library/didactic/support/natural_deduction.ma +++ b/helm/software/matita/library/didactic/support/natural_deduction.ma @@ -111,6 +111,43 @@ notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 for @{ 'leaf_ko $a $t }. interpretation "leaf KO" 'leaf_ko a t = (cast _ _ (show a t)). +(* already proved lemma *) +definition Lemma : ∀A.A→A ≝ λA:CProp.λa:A.a. + +notation < "\infrule \nbsp p mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19 +for @{ 'lemma_ko_1 $p $H }. +interpretation "lemma_ko_1" 'lemma_ko_1 p H = + (show p (cast _ _ (Lemma _ H))). + +notation < "\infrule \nbsp mstyle color #ff0000 (p) mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19 +for @{ 'lemma_ko_2 $p $H }. +interpretation "lemma_ko_2" 'lemma_ko_2 p H = + (cast _ _ (show p (cast _ _ (Lemma _ H)))). + +notation < "\infrule \nbsp p (\lem\emsp H)" non associative with precedence 19 +for @{ 'lemma_ok_1 $p $H }. +interpretation "lemma_ok_1" 'lemma_ok_1 p H = + (show p (Lemma _ H)). +interpretation "lemma_ok_11" 'lemma_ok_1 p H = + (show p (Lemma _ H _)). +interpretation "lemma_ok_111" 'lemma_ok_1 p H = + (show p (Lemma _ H _ _)). + +notation < "\infrule \nbsp mstyle color #ff0000 (p) (\lem\emsp H)" non associative with precedence 19 +for @{ 'lemma_ok_2 $p $H }. +interpretation "lemma_ok_2" 'lemma_ok_2 p H = + (cast _ _ (show p (Lemma _ H))). +interpretation "lemma_ok_22" 'lemma_ok_2 p H = + (cast _ _ (show p (Lemma _ H _))). +interpretation "lemma_ok_22" 'lemma_ok_2 p H = + (cast _ _ (show p (Lemma _ H _ _))). + +notation > "'lem' term 90 p" non associative with precedence 19 +for @{ 'Lemma $p }. +interpretation "lemma KO" 'Lemma p = (cast _ _ (Lemma _ p)). +interpretation "lemma OK" 'Lemma p = (Lemma _ p). + + (* discharging *) notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 for @{ 'discharge_ko_1 $a $H }. @@ -310,7 +347,7 @@ interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab = (show ab (Or_intro_r _ _ a)). notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19 -for @{ 'Or_intro_r_ok_1 $a $ab }. +for @{ 'Or_intro_r_ok_2 $a $ab }. interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = (cast _ _ (show ab (Or_intro_r _ _ a))). @@ -427,22 +464,22 @@ interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a) interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a). (* ¬ elimination *) -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19 for @{ 'Not_elim_ko_1 $ab $a $b }. interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b = (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a)))). -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19 for @{ 'Not_elim_ko_2 $ab $a $b }. interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b = (cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))))). -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub\e) " with precedence 19 +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) " with precedence 19 for @{ 'Not_elim_ok_1 $ab $a $b }. interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b = (show b (Not_elim _ ab a)). -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub\e) " with precedence 19 +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19 for @{ 'Not_elim_ok_2 $ab $a $b }. interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b = (cast _ _ (show b (Not_elim _ ab a))). diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 62eefcfd7..a14858d91 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -1597,12 +1597,24 @@ 0 + + + True + True + True + Use lemma (lem) + 0 + + + 1 + + True True True - Discharge (discharge [ ]) + Discharge (discharge) 0 @@ -2338,59 +2350,6 @@ 3 2 5 - - - True - 0 - Find: - - - - - - - - - True - 0 - Replace with: - - - 1 - 2 - - - - - - - True - True - True - True - True - * - - - 1 - 2 - - - - - - True - True - * - - - 1 - 2 - 1 - 2 - - - True @@ -2489,6 +2448,59 @@ 5 + + + True + True + * + + + 1 + 2 + 1 + 2 + + + + + + True + True + True + True + True + * + + + 1 + 2 + + + + + + True + 0 + Replace with: + + + 1 + 2 + + + + + + + True + 0 + Find: + + + + + + diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 84909e95b..db26ba20a 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -791,6 +791,8 @@ class gui () = (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n"); connect_button main#butRAA (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n"); + connect_button main#butUseLemma + (fun () -> source_buffer#insert "apply rule (lem …);\n"); connect_button main#butDischarge (fun () -> source_buffer#insert "apply rule (discharge […]);\n"); -- 2.39.2