From: Enrico Tassi Date: Sat, 15 Nov 2008 13:14:48 +0000 (+0000) Subject: house keeping X-Git-Tag: make_still_working~4561 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3895bfa2b76c88af1d6ac41605ff17e2626d353a;p=helm.git house keeping --- diff --git a/helm/software/matita/library/demo/natural_deduction_support.ma b/helm/software/matita/library/demo/natural_deduction_support.ma deleted file mode 100644 index 3969197e9..000000000 --- a/helm/software/matita/library/demo/natural_deduction_support.ma +++ /dev/null @@ -1,438 +0,0 @@ -(* Logic system *) - -inductive Imply (A,B:CProp) : CProp ≝ -| Imply_intro: (A → B) → Imply A B. - -definition Imply_elim ≝ λA,B.λf:Imply A B. λa:A. - match f with [ Imply_intro g ⇒ g a]. - -inductive And (A,B:CProp) : CProp ≝ -| And_intro: A → B → And A B. - -definition And_elim_l ≝ λA,B.λc:And A B. - match c with [ And_intro a b ⇒ a ]. - -definition And_elim_r ≝ λA,B.λc:And A B. - match c with [ And_intro a b ⇒ b ]. - -inductive Or (A,B:CProp) : CProp ≝ -| Or_intro_l: A → Or A B -| Or_intro_r: B → Or A B. - -definition Or_elim ≝ λA,B,C:CProp.λc:Or A B.λfa: A → C.λfb: B → C. - match c with - [ Or_intro_l a ⇒ fa a - | Or_intro_r b ⇒ fb b]. - -inductive Top : CProp := -| Top_intro : Top. - -inductive Bot : CProp := . - -definition Bot_elim ≝ λP:CProp.λx:Bot. - match x in Bot return λx.P with []. - -definition Not := λA:CProp.Imply A Bot. - -definition Not_intro : ∀A.(A → Bot) → Not A ≝ λA. - Imply_intro A Bot. - -definition Not_elim : ∀A.Not A → A → Bot ≝ λA. - Imply_elim ? Bot. - -definition assumpt := λA:CProp.λa:A. - a. - -axiom Raa : ∀A.(Not A → Bot) → A. - -(* Dummy proposition *) -axiom unit : CProp. - -(* Notations *) -notation "hbox(a break ⇒ b)" right associative with precedence 20 -for @{ 'Imply $a $b }. -interpretation "Imply" 'Imply a b = (Imply a b). -interpretation "constructive or" 'or x y = (Or x y). -interpretation "constructive and" 'and x y = (And x y). -notation "⊤" non associative with precedence 90 for @{'Top}. -interpretation "Top" 'Top = Top. -notation "⊥" non associative with precedence 90 for @{'Bot}. -interpretation "Bot" 'Bot = Bot. -interpretation "Not" 'not a = (Not a). -notation "✶" non associative with precedence 90 for @{'unit}. -interpretation "dummy prop" 'unit = unit. - -(* Variables *) -axiom A : CProp. -axiom B : CProp. -axiom C : CProp. -axiom D : CProp. -axiom E : CProp. -axiom F : CProp. -axiom G : CProp. -axiom H : CProp. -axiom I : CProp. -axiom J : CProp. -axiom K : CProp. -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. - -(* Every formula user provided annotates its proof A becomes (show 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. - - -notation > "'prove' p" non associative with precedence 19 -for @{ 'prove $p }. -interpretation "prove KO" 'prove p = (cast _ _ (show p _)). -interpretation "prove OK" 'prove p = (show p _). - -notation < "\infrule (t\atop ⋮) a ?" with precedence 19 for @{ 'leaf_ok $a $t }. -interpretation "leaf OK" 'leaf_ok a t = (show a t). -notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 for @{ 'leaf_ko $a $t }. -interpretation "leaf KO" 'leaf_ko a t = (cast _ a (show _ t)). - -notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 for @{ 'assumpt_ko $a $H }. -interpretation "assumption_ko 1" 'assumpt_ko a H = (show a (cast _ _ (assumpt _ H))). -interpretation "assumption_ko 2" 'assumpt_ko a H = (cast _ _ (show a (cast _ _ (assumpt _ H)))). - -notation < "[ a ] \sup H" with precedence 19 for @{ 'assumpt_ok $a $H }. -interpretation "assumption_ok 1" 'assumpt_ok a H = (show a (assumpt a H)). -notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 for @{ 'assumpt_ok_2 $a $H }. -interpretation "assumption_ok 2" 'assumpt_ok_2 a H = (cast _ _ (show a (assumpt a H))). - -notation > "[H]" with precedence 90 for @{ 'assumpt $H }. -interpretation "assumpt KO" 'assumpt H = (cast _ _ (assumpt _ H)). -interpretation "assumpt OK" 'assumpt H = (assumpt _ H). - -notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19 -for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }. -interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b = - (show ab (cast _ _ (Imply_intro _ _ b))). - -notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19 -for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }. -interpretation "Imply_intro_ko_1" 'Imply_intro_ko_2 ab \eta.b = - (cast _ _ (show ab (cast _ _ (Imply_intro _ _ b)))). - -notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19 -for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }. -interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b = - (show ab (Imply_intro _ _ b)). - -notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19 -for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }. -interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b = - (cast _ _ (show ab (Imply_intro _ _ b))). - -notation > "⇒_'i' [ident H] term 90 b" with precedence 19 -for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }. -interpretation "Imply_intro KO" 'Imply_intro b pb = (cast _ (Imply unit b) (Imply_intro _ b pb)). -interpretation "Imply_intro OK" 'Imply_intro b pb = (Imply_intro _ b pb). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_1 $ab $a $b }. -interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b = - (show b (cast _ _ (Imply_elim _ _ ab a))). -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_2 $ab $a $b }. -interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b = - (cast _ _ (show b (cast _ _ (Imply_elim _ _ ab a)))). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) " with precedence 19 -for @{ 'Imply_elim_ok_1 $ab $a $b }. -interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b = - (show b (Imply_elim _ _ ab a)). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19 -for @{ 'Imply_elim_ok_2 $ab $a $b }. -interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b = - (cast _ _ (show b (Imply_elim _ _ ab a))). - -notation > "⇒_'e' term 90 ab term 90 a" with precedence 19 for @{ 'Imply_elim (show $ab ?) (show $a ?) }. -interpretation "Imply_elim KO" 'Imply_elim ab a = (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))). -interpretation "Imply_elim OK" 'Imply_elim ab a = (Imply_elim _ _ ab a). - -notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_1 $a $b $ab }. -interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab = - (show ab (cast _ _ (And_intro _ _ a b))). -notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_2 $a $b $ab }. -interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab = - (cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))). - -notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)" with precedence 19 -for @{ 'And_intro_ok_1 $a $b $ab }. -interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab = - (show ab (And_intro _ _ a b)). - -notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19 -for @{ 'And_intro_ok_2 $a $b $ab }. -interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab = - (cast _ _ (show ab (And_intro _ _ a b))). - -notation > "∧_'i' term 90 a term 90 b" with precedence 19 for @{ 'And_intro (show $a ?) (show $b ?) }. -interpretation "And_intro KO" 'And_intro a b = (cast _ _ (And_intro _ _ a b)). -interpretation "And_intro OK" 'And_intro a b = (And_intro _ _ a b). - -notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 -for @{ 'And_elim_l_ko_1 $ab $a }. -interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a = - (show a (cast _ _ (And_elim_l _ _ ab))). - -notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 -for @{ 'And_elim_l_ko_2 $ab $a }. -interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a = - (cast _ _ (show a (cast _ _ (And_elim_l _ _ ab)))). - -notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19 -for @{ 'And_elim_l_ok_1 $ab $a }. -interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a = - (show a (And_elim_l _ _ ab)). - -notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19 -for @{ 'And_elim_l_ok_2 $ab $a }. -interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a = - (cast _ _ (show a (And_elim_l _ _ ab))). - -notation > "∧_'e_l' term 90 ab" with precedence 19 -for @{ 'And_elim_l (show $ab ?) }. -interpretation "And_elim_l KO" 'And_elim_l a = (And_elim_l _ _ (cast (And _ unit) _ a)). -interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l _ _ a). - -notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 -for @{ 'And_elim_r_ko_1 $ab $a }. -interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a = - (show a (cast _ _ (And_elim_r _ _ ab))). - -notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 -for @{ 'And_elim_r_ko_2 $ab $a }. -interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a = - (cast _ _ (show a (cast _ _ (And_elim_r _ _ ab)))). - -notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))" with precedence 19 -for @{ 'And_elim_r_ok_1 $ab $a }. -interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a = - (show a (And_elim_r _ _ ab)). - -notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19 -for @{ 'And_elim_r_ok_2 $ab $a }. -interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a = - (cast _ _ (show a (And_elim_r _ _ ab))). - -notation > "∧_'e_r' term 90 ab" with precedence 19 -for @{ 'And_elim_r (show $ab ?) }. -interpretation "And_elim_r KO" 'And_elim_r a = (And_elim_r _ _ (cast (And unit _) _ a)). -interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r _ _ a). - -notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19 -for @{ 'Or_intro_l_ok_1 $a $ab }. -interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab = - (show ab (Or_intro_l _ _ a)). - -notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 -for @{ 'Or_intro_l_ok_1 $a $ab }. -interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = - (cast _ _ (show ab (Or_intro_l _ _ a))). - -notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 -for @{ 'Or_intro_l_ko_1 $a $ab }. -interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab = - (show ab (cast _ _ (Or_intro_l _ _ a))). - -notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 -for @{ 'Or_intro_l_ko_2 $a $ab }. -interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab = - (cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))). - -notation > "∨_'i_l' term 90 a" with precedence 19 -for @{ 'Or_intro_l (show $a ?) }. -interpretation "Or_intro_l KO" 'Or_intro_l a = (cast _ (Or _ unit) (Or_intro_l _ _ a)). -interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l _ _ a). - -notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" with precedence 19 -for @{ 'Or_intro_r_ok_1 $a $ab }. -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 }. -interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = - (cast _ _ (show ab (Or_intro_r _ _ a))). - -notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 -for @{ 'Or_intro_r_ko_1 $a $ab }. -interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab = - (show ab (cast _ _ (Or_intro_r _ _ a))). - -notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 -for @{ 'Or_intro_r_ko_2 $a $ab }. -interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab = - (cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))). - -notation > "∨_'i_r' term 90 a" with precedence 19 -for @{ 'Or_intro_r (show $a ?) }. -interpretation "Or_intro_r KO" 'Or_intro_r a = (cast _ (Or unit _) (Or_intro_r _ _ a)). -interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r _ _ a). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19 -for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }. -interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c = - (show c (Or_elim _ _ _ ab ac bc)). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19 -for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }. -interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c = - (cast _ _ (show c (Or_elim _ _ _ ab ac bc))). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19 -for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }. -interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc = - (show c (cast _ _ (Or_elim _ _ _ ab (cast _ _ ac) (cast _ _ bc)))). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19 -for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }. -interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c = - (cast _ _ (show c (cast _ _ (Or_elim _ _ _ ab (cast _ _ ac) (cast _ _ bc))))). - -definition unit_to ≝ λx:CProp.unit → x. - -notation > "∨_'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19 -for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) $cl $cr }. -interpretation "Or_elim KO" 'Or_elim ab ac bc c1 c2 = - (cast _ _ (Or_elim _ _ _ (cast (Or unit unit) _ ab) (cast (unit_to unit) (unit_to _) ac) (cast (unit_to unit) (unit_to _) bc))). -interpretation "Or_elim OK" 'Or_elim ab ac bc c1 c2 = (Or_elim _ _ _ ab ac bc). - -notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19 -for @{'Top_intro_ko_1}. -interpretation "Top_intro_ko_1" 'Top_intro_ko_1 = (show _ (cast _ _ Top_intro)). - -notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19 -for @{'Top_intro_ok_1}. -interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro). - -notation > "⊤_'i'" with precedence 19 for @{ 'Top_intro }. -interpretation "Top_intro KO" 'Top_intro = (cast _ _ Top_intro). -interpretation "Top_intro OK" 'Top_intro = Top_intro. - -notation < "\infrule b a (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ok_1 $a $b}. -interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b = - (show a (Bot_elim a b)). - -notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ko_1 $a $b}. -interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b = - (show a (Bot_elim a (cast _ _ b))). - -notation > "⊥_'e' term 90 b" with precedence 19 -for @{ 'Bot_elim (show $b ?) }. -interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)). -interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a). - -notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19 -for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }. -interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b = - (show ab (cast _ _ (Not_intro _ (cast _ _ b)))). - -notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19 -for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }. -interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b = - (cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))). - -notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub\i \emsp ident H) " with precedence 19 -for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }. -interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b = - (show ab (Not_intro _ b)). - -notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub\i \emsp ident H) " with precedence 19 -for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }. -interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b = - (cast _ _ (show ab (Not_intro _ b))). - -notation > "¬_'i' [ident H] term 90 b" with precedence 19 -for @{ 'Not_intro (λ${ident H}.show $b ?) }. -interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a))). -interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub\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 -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))). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub\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 (Not_elim _ (cast _ _ ab) a)). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub\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 (Not_elim _ (cast _ _ ab) a))). - -notation > "¬_'e' term 90 ab term 90 a" with precedence 19 -for @{ 'Not_elim (show $ab ?) (show $a ?) }. -interpretation "Not_elim KO" 'Not_elim ab a = (Not_elim _ (cast _ _ ab) a). -interpretation "Not_elim OK" 'Not_elim ab a = (Not_elim _ ab a). - -notation < "\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)" with precedence 19 -for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }. -interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn = - (show Pn (Raa _ Px)). - -notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19 -for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }. -interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn = - (cast _ _ (show Pn (Raa _ Px))). - -notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19 -for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }. -interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn = - (show Pn (Raa _ (cast _ _ Px))). - -notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19 -for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }. -interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn = - (cast _ _ (show Pn (Raa _ (cast _ _ Px)))). - -notation > "'RAA' [ident H] term 90 b" with precedence 19 -for @{ 'Raa (λ${ident H}.show $b ?) }. -interpretation "RAA KO" 'Raa p = (Raa _ (cast _ (unit_to _) p)). -interpretation "RAA OK" 'Raa p = (Raa _ p). - -(*DOCBEGIN -Templates for rules -⇒_i […] (…) -∧_i (…) (…) -∨_i_l (…) -∨_i_r (…) -¬_i […] (…) -⊤_i -⇒_e (…) (…) -∧_e_l (…) -∧_e_r (…) -∨_e (…) […] (…) […] (…) -¬_e (…) (…) -⊥_e (…) -prove (…) -RAA […] (…) -DOCEND*) - - - - diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma new file mode 100644 index 000000000..3969197e9 --- /dev/null +++ b/helm/software/matita/library/didactic/support/natural_deduction.ma @@ -0,0 +1,438 @@ +(* Logic system *) + +inductive Imply (A,B:CProp) : CProp ≝ +| Imply_intro: (A → B) → Imply A B. + +definition Imply_elim ≝ λA,B.λf:Imply A B. λa:A. + match f with [ Imply_intro g ⇒ g a]. + +inductive And (A,B:CProp) : CProp ≝ +| And_intro: A → B → And A B. + +definition And_elim_l ≝ λA,B.λc:And A B. + match c with [ And_intro a b ⇒ a ]. + +definition And_elim_r ≝ λA,B.λc:And A B. + match c with [ And_intro a b ⇒ b ]. + +inductive Or (A,B:CProp) : CProp ≝ +| Or_intro_l: A → Or A B +| Or_intro_r: B → Or A B. + +definition Or_elim ≝ λA,B,C:CProp.λc:Or A B.λfa: A → C.λfb: B → C. + match c with + [ Or_intro_l a ⇒ fa a + | Or_intro_r b ⇒ fb b]. + +inductive Top : CProp := +| Top_intro : Top. + +inductive Bot : CProp := . + +definition Bot_elim ≝ λP:CProp.λx:Bot. + match x in Bot return λx.P with []. + +definition Not := λA:CProp.Imply A Bot. + +definition Not_intro : ∀A.(A → Bot) → Not A ≝ λA. + Imply_intro A Bot. + +definition Not_elim : ∀A.Not A → A → Bot ≝ λA. + Imply_elim ? Bot. + +definition assumpt := λA:CProp.λa:A. + a. + +axiom Raa : ∀A.(Not A → Bot) → A. + +(* Dummy proposition *) +axiom unit : CProp. + +(* Notations *) +notation "hbox(a break ⇒ b)" right associative with precedence 20 +for @{ 'Imply $a $b }. +interpretation "Imply" 'Imply a b = (Imply a b). +interpretation "constructive or" 'or x y = (Or x y). +interpretation "constructive and" 'and x y = (And x y). +notation "⊤" non associative with precedence 90 for @{'Top}. +interpretation "Top" 'Top = Top. +notation "⊥" non associative with precedence 90 for @{'Bot}. +interpretation "Bot" 'Bot = Bot. +interpretation "Not" 'not a = (Not a). +notation "✶" non associative with precedence 90 for @{'unit}. +interpretation "dummy prop" 'unit = unit. + +(* Variables *) +axiom A : CProp. +axiom B : CProp. +axiom C : CProp. +axiom D : CProp. +axiom E : CProp. +axiom F : CProp. +axiom G : CProp. +axiom H : CProp. +axiom I : CProp. +axiom J : CProp. +axiom K : CProp. +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. + +(* Every formula user provided annotates its proof A becomes (show 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. + + +notation > "'prove' p" non associative with precedence 19 +for @{ 'prove $p }. +interpretation "prove KO" 'prove p = (cast _ _ (show p _)). +interpretation "prove OK" 'prove p = (show p _). + +notation < "\infrule (t\atop ⋮) a ?" with precedence 19 for @{ 'leaf_ok $a $t }. +interpretation "leaf OK" 'leaf_ok a t = (show a t). +notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 for @{ 'leaf_ko $a $t }. +interpretation "leaf KO" 'leaf_ko a t = (cast _ a (show _ t)). + +notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 for @{ 'assumpt_ko $a $H }. +interpretation "assumption_ko 1" 'assumpt_ko a H = (show a (cast _ _ (assumpt _ H))). +interpretation "assumption_ko 2" 'assumpt_ko a H = (cast _ _ (show a (cast _ _ (assumpt _ H)))). + +notation < "[ a ] \sup H" with precedence 19 for @{ 'assumpt_ok $a $H }. +interpretation "assumption_ok 1" 'assumpt_ok a H = (show a (assumpt a H)). +notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 for @{ 'assumpt_ok_2 $a $H }. +interpretation "assumption_ok 2" 'assumpt_ok_2 a H = (cast _ _ (show a (assumpt a H))). + +notation > "[H]" with precedence 90 for @{ 'assumpt $H }. +interpretation "assumpt KO" 'assumpt H = (cast _ _ (assumpt _ H)). +interpretation "assumpt OK" 'assumpt H = (assumpt _ H). + +notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19 +for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }. +interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b = + (show ab (cast _ _ (Imply_intro _ _ b))). + +notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19 +for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }. +interpretation "Imply_intro_ko_1" 'Imply_intro_ko_2 ab \eta.b = + (cast _ _ (show ab (cast _ _ (Imply_intro _ _ b)))). + +notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19 +for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }. +interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b = + (show ab (Imply_intro _ _ b)). + +notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19 +for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }. +interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b = + (cast _ _ (show ab (Imply_intro _ _ b))). + +notation > "⇒_'i' [ident H] term 90 b" with precedence 19 +for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }. +interpretation "Imply_intro KO" 'Imply_intro b pb = (cast _ (Imply unit b) (Imply_intro _ b pb)). +interpretation "Imply_intro OK" 'Imply_intro b pb = (Imply_intro _ b pb). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_1 $ab $a $b }. +interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b = + (show b (cast _ _ (Imply_elim _ _ ab a))). +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_2 $ab $a $b }. +interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b = + (cast _ _ (show b (cast _ _ (Imply_elim _ _ ab a)))). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) " with precedence 19 +for @{ 'Imply_elim_ok_1 $ab $a $b }. +interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b = + (show b (Imply_elim _ _ ab a)). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19 +for @{ 'Imply_elim_ok_2 $ab $a $b }. +interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b = + (cast _ _ (show b (Imply_elim _ _ ab a))). + +notation > "⇒_'e' term 90 ab term 90 a" with precedence 19 for @{ 'Imply_elim (show $ab ?) (show $a ?) }. +interpretation "Imply_elim KO" 'Imply_elim ab a = (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))). +interpretation "Imply_elim OK" 'Imply_elim ab a = (Imply_elim _ _ ab a). + +notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_1 $a $b $ab }. +interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab = + (show ab (cast _ _ (And_intro _ _ a b))). +notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_2 $a $b $ab }. +interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab = + (cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))). + +notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)" with precedence 19 +for @{ 'And_intro_ok_1 $a $b $ab }. +interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab = + (show ab (And_intro _ _ a b)). + +notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19 +for @{ 'And_intro_ok_2 $a $b $ab }. +interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab = + (cast _ _ (show ab (And_intro _ _ a b))). + +notation > "∧_'i' term 90 a term 90 b" with precedence 19 for @{ 'And_intro (show $a ?) (show $b ?) }. +interpretation "And_intro KO" 'And_intro a b = (cast _ _ (And_intro _ _ a b)). +interpretation "And_intro OK" 'And_intro a b = (And_intro _ _ a b). + +notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 +for @{ 'And_elim_l_ko_1 $ab $a }. +interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a = + (show a (cast _ _ (And_elim_l _ _ ab))). + +notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 +for @{ 'And_elim_l_ko_2 $ab $a }. +interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a = + (cast _ _ (show a (cast _ _ (And_elim_l _ _ ab)))). + +notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19 +for @{ 'And_elim_l_ok_1 $ab $a }. +interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a = + (show a (And_elim_l _ _ ab)). + +notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19 +for @{ 'And_elim_l_ok_2 $ab $a }. +interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a = + (cast _ _ (show a (And_elim_l _ _ ab))). + +notation > "∧_'e_l' term 90 ab" with precedence 19 +for @{ 'And_elim_l (show $ab ?) }. +interpretation "And_elim_l KO" 'And_elim_l a = (And_elim_l _ _ (cast (And _ unit) _ a)). +interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l _ _ a). + +notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 +for @{ 'And_elim_r_ko_1 $ab $a }. +interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a = + (show a (cast _ _ (And_elim_r _ _ ab))). + +notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 +for @{ 'And_elim_r_ko_2 $ab $a }. +interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a = + (cast _ _ (show a (cast _ _ (And_elim_r _ _ ab)))). + +notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))" with precedence 19 +for @{ 'And_elim_r_ok_1 $ab $a }. +interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a = + (show a (And_elim_r _ _ ab)). + +notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19 +for @{ 'And_elim_r_ok_2 $ab $a }. +interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a = + (cast _ _ (show a (And_elim_r _ _ ab))). + +notation > "∧_'e_r' term 90 ab" with precedence 19 +for @{ 'And_elim_r (show $ab ?) }. +interpretation "And_elim_r KO" 'And_elim_r a = (And_elim_r _ _ (cast (And unit _) _ a)). +interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r _ _ a). + +notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19 +for @{ 'Or_intro_l_ok_1 $a $ab }. +interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab = + (show ab (Or_intro_l _ _ a)). + +notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 +for @{ 'Or_intro_l_ok_1 $a $ab }. +interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = + (cast _ _ (show ab (Or_intro_l _ _ a))). + +notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 +for @{ 'Or_intro_l_ko_1 $a $ab }. +interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab = + (show ab (cast _ _ (Or_intro_l _ _ a))). + +notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 +for @{ 'Or_intro_l_ko_2 $a $ab }. +interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab = + (cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))). + +notation > "∨_'i_l' term 90 a" with precedence 19 +for @{ 'Or_intro_l (show $a ?) }. +interpretation "Or_intro_l KO" 'Or_intro_l a = (cast _ (Or _ unit) (Or_intro_l _ _ a)). +interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l _ _ a). + +notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" with precedence 19 +for @{ 'Or_intro_r_ok_1 $a $ab }. +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 }. +interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = + (cast _ _ (show ab (Or_intro_r _ _ a))). + +notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 +for @{ 'Or_intro_r_ko_1 $a $ab }. +interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab = + (show ab (cast _ _ (Or_intro_r _ _ a))). + +notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 +for @{ 'Or_intro_r_ko_2 $a $ab }. +interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab = + (cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))). + +notation > "∨_'i_r' term 90 a" with precedence 19 +for @{ 'Or_intro_r (show $a ?) }. +interpretation "Or_intro_r KO" 'Or_intro_r a = (cast _ (Or unit _) (Or_intro_r _ _ a)). +interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r _ _ a). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19 +for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }. +interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c = + (show c (Or_elim _ _ _ ab ac bc)). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19 +for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }. +interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c = + (cast _ _ (show c (Or_elim _ _ _ ab ac bc))). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19 +for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }. +interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc = + (show c (cast _ _ (Or_elim _ _ _ ab (cast _ _ ac) (cast _ _ bc)))). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19 +for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }. +interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c = + (cast _ _ (show c (cast _ _ (Or_elim _ _ _ ab (cast _ _ ac) (cast _ _ bc))))). + +definition unit_to ≝ λx:CProp.unit → x. + +notation > "∨_'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19 +for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) $cl $cr }. +interpretation "Or_elim KO" 'Or_elim ab ac bc c1 c2 = + (cast _ _ (Or_elim _ _ _ (cast (Or unit unit) _ ab) (cast (unit_to unit) (unit_to _) ac) (cast (unit_to unit) (unit_to _) bc))). +interpretation "Or_elim OK" 'Or_elim ab ac bc c1 c2 = (Or_elim _ _ _ ab ac bc). + +notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19 +for @{'Top_intro_ko_1}. +interpretation "Top_intro_ko_1" 'Top_intro_ko_1 = (show _ (cast _ _ Top_intro)). + +notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19 +for @{'Top_intro_ok_1}. +interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro). + +notation > "⊤_'i'" with precedence 19 for @{ 'Top_intro }. +interpretation "Top_intro KO" 'Top_intro = (cast _ _ Top_intro). +interpretation "Top_intro OK" 'Top_intro = Top_intro. + +notation < "\infrule b a (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ok_1 $a $b}. +interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b = + (show a (Bot_elim a b)). + +notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ko_1 $a $b}. +interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b = + (show a (Bot_elim a (cast _ _ b))). + +notation > "⊥_'e' term 90 b" with precedence 19 +for @{ 'Bot_elim (show $b ?) }. +interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)). +interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a). + +notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19 +for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }. +interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b = + (show ab (cast _ _ (Not_intro _ (cast _ _ b)))). + +notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19 +for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }. +interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b = + (cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))). + +notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub\i \emsp ident H) " with precedence 19 +for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }. +interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b = + (show ab (Not_intro _ b)). + +notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub\i \emsp ident H) " with precedence 19 +for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }. +interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b = + (cast _ _ (show ab (Not_intro _ b))). + +notation > "¬_'i' [ident H] term 90 b" with precedence 19 +for @{ 'Not_intro (λ${ident H}.show $b ?) }. +interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a))). +interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub\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 +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))). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub\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 (Not_elim _ (cast _ _ ab) a)). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub\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 (Not_elim _ (cast _ _ ab) a))). + +notation > "¬_'e' term 90 ab term 90 a" with precedence 19 +for @{ 'Not_elim (show $ab ?) (show $a ?) }. +interpretation "Not_elim KO" 'Not_elim ab a = (Not_elim _ (cast _ _ ab) a). +interpretation "Not_elim OK" 'Not_elim ab a = (Not_elim _ ab a). + +notation < "\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)" with precedence 19 +for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn = + (show Pn (Raa _ Px)). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19 +for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn = + (cast _ _ (show Pn (Raa _ Px))). + +notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19 +for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn = + (show Pn (Raa _ (cast _ _ Px))). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19 +for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn = + (cast _ _ (show Pn (Raa _ (cast _ _ Px)))). + +notation > "'RAA' [ident H] term 90 b" with precedence 19 +for @{ 'Raa (λ${ident H}.show $b ?) }. +interpretation "RAA KO" 'Raa p = (Raa _ (cast _ (unit_to _) p)). +interpretation "RAA OK" 'Raa p = (Raa _ p). + +(*DOCBEGIN +Templates for rules +⇒_i […] (…) +∧_i (…) (…) +∨_i_l (…) +∨_i_r (…) +¬_i […] (…) +⊤_i +⇒_e (…) (…) +∧_e_l (…) +∧_e_r (…) +∨_e (…) […] (…) […] (…) +¬_e (…) (…) +⊥_e (…) +prove (…) +RAA […] (…) +DOCEND*) + + + +