+++ /dev/null
-(* 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*)
-
-
-
-
--- /dev/null
+(* 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*)
+
+
+
+
projects / helm.git / commitdiff