From c99a38b6539be1eb667cced1eed2db3fc75e3162 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 17 Nov 2008 16:20:08 +0000 Subject: [PATCH] exercises ready --- .../didactic/exercises/natural_deduction.ma | 14 +- .../didactic/support/natural_deduction.ma | 218 ++++++++++++------ helm/software/matita/matita.glade | 48 ++++ helm/software/matita/matitaGui.ml | 10 + 4 files changed, 223 insertions(+), 67 deletions(-) diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma index 98142db2f..5e7188814 100644 --- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma +++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma @@ -29,6 +29,18 @@ Per digitare i connettivi logici: * `⊥` : `\bot` * `⊤` : `\top` +I termini, le formule e i nomi delle ipotesi +============================================ + +* I termini quantificati da `∀` e `∃`, quando argomenti di + una regola, vengono scritti tra `{` e `}`. + +* Le formule, quando argomenti di + una regola, vengono scritti tra `(` e `)`. + +* I nomi delle ipotesi, quando argomenti di + una regola, vengono scritti tra `[` e `]`. + Le regole di deduzione naturale =============================== @@ -75,7 +87,7 @@ DOCEND*) include "didactic/support/natural_deduction.ma". -theorem EM: ∀A. A ∨ ¬ A. +theorem EM: ∀A:CProp. A ∨ ¬ A. (* Il comando assume è necessario perchè dimostriamo A∨¬A per una A generica. *) assume A: CProp. diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma index 90ebd7217..84fbeee78 100644 --- a/helm/software/matita/library/didactic/support/natural_deduction.ma +++ b/helm/software/matita/library/didactic/support/natural_deduction.ma @@ -45,6 +45,21 @@ definition Discharge := λA:CProp.λa:A. axiom Raa : ∀A.(Not A → Bot) → A. +axiom sort : Type. + +inductive Exists (A:Type) (P:A→CProp) : CProp ≝ + Exists_intro: ∀w:A. P w → Exists A P. + +definition Exists_elim ≝ + λA:Type.λP:A→CProp.λC:CProp.λc:Exists A P.λH:(Πx.P x → C). + match c with [ Exists_intro w p ⇒ H w p ]. + +inductive Forall (A:Type) (P:A→CProp) : CProp ≝ + Forall_intro: (∀n:A. P n) → Forall A P. + +definition Forall_elim ≝ + λA:Type.λP:A→CProp.λn:A.λf:Forall A P.match f with [ Forall_intro g ⇒ g n ]. + (* Dummy proposition *) axiom unit : CProp. @@ -61,7 +76,17 @@ interpretation "Bot" 'Bot = Bot. interpretation "Not" 'not a = (Not a). notation "✶" non associative with precedence 90 for @{'unit}. interpretation "dummy prop" 'unit = unit. - +notation > "\exists list1 ident x sep , . term 19 Px" with precedence 20 +for ${ fold right @{$Px} rec acc @{'myexists (λ${ident x}.$acc)} }. +notation < "hvbox(\exists ident i break . p)" with precedence 20 +for @{ 'myexists (\lambda ${ident i} : $ty. $p) }. +interpretation "constructive ex" 'myexists \eta.x = (Exists sort x). +notation > "\forall ident x.break term 19 Px" with precedence 20 +for @{ 'Forall (λ${ident x}.$Px) }. +notation < "\forall ident x.break term 19 Px" with precedence 20 +for @{ 'Forall (λ${ident x}:$tx.$Px) }. +interpretation "Forall" 'Forall \eta.Px = (Forall _ Px). + (* Variables *) axiom A : CProp. axiom B : CProp. @@ -78,24 +103,20 @@ axiom L : CProp. axiom M : CProp. axiom N : CProp. axiom O : CProp. -axiom P : CProp. -axiom Q : CProp. -axiom R : CProp. -axiom S : CProp. -axiom T : CProp. -axiom U : CProp. -axiom V : CProp. -axiom W : CProp. -axiom X : CProp. -axiom Y : CProp. -axiom Z : CProp. +axiom P : sort →CProp. +axiom Q : sort →CProp. +axiom R : sort →sort →CProp. +axiom S : sort →sort →CProp. +axiom f : sort → sort. +axiom g : sort → sort. +axiom h : sort → sort → sort. (* Every formula user provided annotates its proof: `A` becomes `(show A ?)` *) -definition show : ∀A.A→A ≝ λA:CProp.λa:A.a. +definition show : ΠA.A→A ≝ λA:CProp.λa:A.a. (* When something does not fit, this daemon is used *) -axiom cast: ∀A,B:CProp.B → A. +axiom cast: ΠA,B:CProp.B → A. (* begin a proof: draws the root *) notation > "'prove' p" non associative with precedence 19 @@ -112,7 +133,7 @@ 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. +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 }. @@ -517,54 +538,119 @@ for @{ 'Raa (λ${ident H}.show $b ?) }. interpretation "RAA KO" 'Raa p = (cast _ unit (Raa _ (cast _ (unit_to _) p))). interpretation "RAA OK" 'Raa p = (Raa _ p). -(*DOCBEGIN -Templates for rules: - - apply rule (⇒_i […] (…)). - - apply rule (∧_i (…) (…)); - [ - | - ] - - apply rule (∨_i_l (…)). - - apply rule (∨_i_r (…)). - - apply rule (¬_i […] (…)). - - apply rule (⊤_i). - - apply rule (⇒_e (…) (…)); - [ - | - ] - - apply rule (∧_e_l (…)). - - apply rule (∧_e_r (…)). - - apply rule (∨_e (…) […] (…) […] (…)); - [ - | - | - ] - - apply rule (¬_e (…) (…)); - [ - | - ] - - apply rule (⊥_e (…)). - - apply rule (prove (…)). - - apply rule (RAA […] (…)). - - apply rule (discharge […]). - -DOCEND*) - - - - +(* ∃ introduction *) +notation < "\infrule hbox(\emsp Pn \emsp) Px mstyle color #ff0000 (∃\sub\i)" with precedence 19 +for @{ 'Exists_intro_ko_1 $Pn $Px }. +interpretation "Exists_intro_ko_1" 'Exists_intro_ko_1 Pn Px = + (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn)))). + +notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) mstyle color #ff0000 (∃\sub\i)" with precedence 19 +for @{ 'Exists_intro_ko_2 $Pn $Px }. +interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px = + (cast _ _ (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn))))). + +notation < "\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)" with precedence 19 +for @{ 'Exists_intro_ok_1 $Pn $Px }. +interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px = + (show Px (Exists_intro _ _ _ Pn)). + +notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) (∃\sub\i)" with precedence 19 +for @{ 'Exists_intro_ok_2 $Pn $Px }. +interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px = + (cast _ _ (show Px (Exists_intro _ _ _ Pn))). + +notation >"∃_'i' {term 90 t} term 90 Pt" non associative with precedence 19 +for @{'Exists_intro $t (λ_.?) (show $Pt ?)}. +interpretation "Exists_intro KO" 'Exists_intro t P Pt = + (cast _ _ (Exists_intro sort P t (cast _ _ Pt))). +interpretation "Exists_intro OK" 'Exists_intro t P Pt = + (Exists_intro sort P t Pt). + +(* ∃ elimination *) +notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19 +for @{ 'Exists_elim_ko_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }. +interpretation "Exists_elim_ko_1" 'Exists_elim_ko_1 ExPx Pc c = + (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc)))). + +notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19 +for @{ 'Exists_elim_ko_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }. +interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c = + (cast _ _ (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc))))). + +notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19 +for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }. +interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c = + (show c (Exists_elim _ _ _ ExPx Pc)). + +notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19 +for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }. +interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c = + (cast _ _ (show c (Exists_elim _ _ _ ExPx Pc))). + +definition ex_concl := λx:CProp.sort → unit → x. +definition fake_pred := λx:sort.unit. + +notation >"∃_'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19 +for @{'Exists_elim (λ_.?) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}. +interpretation "Exists_elim KO" 'Exists_elim P ExPt c = + (cast _ _ (Exists_elim sort P _ + (cast (Exists _ P) _ ExPt) (cast (ex_concl unit) (ex_concl _) c))). +interpretation "Exists_elim OK" 'Exists_elim P ExPt c = + (Exists_elim sort P _ ExPt c). + +(* ∀ introduction *) + +notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19 +for @{ 'Forall_intro_ko_1 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "Forall_intro_ko_1" 'Forall_intro_ko_1 Px Pn = + (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px)))). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19 +for @{ 'Forall_intro_ko_2 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn = + (cast _ _ (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px))))). + +notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)" with precedence 19 +for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn = + (show Pn (Forall_intro _ _ Px)). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\i \emsp ident x)" with precedence 19 +for @{ 'Forall_intro_ok_2 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "Forall_intro_ok_2" 'Forall_intro_ok_2 Px Pn = + (cast _ _ (show Pn (Forall_intro _ _ Px))). + +notation > "∀_'i' {ident y} term 90 Px" non associative with precedence 19 +for @{ 'Forall_intro (λ_.?) (λ${ident y}.show $Px ?) }. +interpretation "Forall_intro KO" 'Forall_intro P Px = + (cast _ _ (Forall_intro sort P (cast _ _ Px))). +interpretation "Forall_intro OK" 'Forall_intro P Px = + (Forall_intro sort P Px). + +(* ∀ elimination *) +notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\e))" with precedence 19 +for @{ 'Forall_elim_ko_1 $Px $Pn }. +interpretation "Forall_elim_ko_1" 'Forall_elim_ko_1 Px Pn = + (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px)))). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\e))" with precedence 19 +for @{ 'Forall_elim_ko_2 $Px $Pn }. +interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn = + (cast _ _ (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px))))). + +notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)" with precedence 19 +for @{ 'Forall_elim_ok_1 $Px $Pn }. +interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn = + (show Pn (Forall_elim _ _ _ Px)). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\e)" with precedence 19 +for @{ 'Forall_elim_ok_2 $Px $Pn }. +interpretation "Forall_elim_ok_2" 'Forall_elim_ok_2 Px Pn = + (cast _ _ (show Pn (Forall_elim _ _ _ Px))). + +notation > "∀_'e' {term 90 t} term 90 Pn" non associative with precedence 19 +for @{ 'Forall_elim (λ_.?) $t (show $Pn ?) }. +interpretation "Forall_elim KO" 'Forall_elim P t Px = + (cast _ unit (Forall_elim sort P t (cast _ _ Px))). +interpretation "Forall_elim OK" 'Forall_elim P t Px = + (Forall_elim sort P t Px). diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index a14858d91..4739e14f8 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -1472,6 +1472,30 @@ 5 + + + True + True + True + Universal (∀_i) + 0 + + + 6 + + + + + True + True + True + Existential (∃_i) + 0 + + + 7 + + @@ -1564,6 +1588,30 @@ 5 + + + True + True + True + Universal (∀_e) + 0 + + + 6 + + + + + True + True + True + Existential (∃_e) + 0 + + + 7 + + diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index db26ba20a..8bc226ed4 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -795,6 +795,16 @@ class gui () = (fun () -> source_buffer#insert "apply rule (lem …);\n"); connect_button main#butDischarge (fun () -> source_buffer#insert "apply rule (discharge […]);\n"); + + connect_button main#butForall_intro + (fun () -> source_buffer#insert "apply rule (∀_i {…} (…));\n"); + connect_button main#butForall_elim + (fun () -> source_buffer#insert "apply rule (∀_e {…} (…));\n"); + connect_button main#butExists_intro + (fun () -> source_buffer#insert "apply rule (∃_i {…} (…));\n"); + connect_button main#butExists_elim + (fun () -> source_buffer#insert + "apply rule (∃_e (…) {…} […] (…));\n\t[\n\t|\n\t]\n"); (* TO BE REMOVED *) -- 2.39.2