From 3fab56d1663ba3d5aeb9207612279e0bb0edbb8c Mon Sep 17 00:00:00 2001 From: Andrea Berlingieri Date: Tue, 23 Apr 2019 13:20:09 +0200 Subject: [PATCH] Changes to declarative tactics, implementation of equality chain Fix type for RewritingStep, add a type for Print Stack (a debug tool) Fix PP for RewritingStep, generalized just_to_tactic_just for the type [>`Auto of auto_params | `Term of NotationPt.term] Add parsing rule for print_stack, fix parsing rules for obtain, conclude e = Fix indentation for declarative.ml Change mk_just to return a tactic (instead of a lowtactic) Modify extract_first_goal_from_status to take the first goal from the stack, instead of the metasenv Change assume, suppose, andelim and existselim to use distribute_tac Add a mustdot function to check whether there's the need to call the dot_tactic at the end. The dot tactic is used to focus on a single goal at the time when there are multiple open goals Change bydone to use the dot tactic to switch between multiple goals Modify we_need_to_prove to use the dot_tac to focus on a single goal Add a type_of_tactic_term function to extract the type of a tactic_term (used in RewritingStep) Implement rewritingstep, which covers conclude and =; obtain is in the works Implement print_stack, for debug purposes (prints the stack to stderr) Modify declarative's signature to add the new functions Add firs_tac to nTactic's signature Change auto_lowtac's signature to return a tactic Correct natural_deduction.ma for the new version. Had to change some \forall with \Pi --- matita/components/grafite/grafiteAst.ml | 4 +- matita/components/grafite/grafiteAstPp.ml | 2 +- .../grafite_engine/grafiteEngine.ml | 15 +- .../grafite_parser/grafiteParser.ml | 34 +- matita/components/ng_tactics/declarative.ml | 652 +++++++------ matita/components/ng_tactics/declarative.mli | 5 + matita/components/ng_tactics/nTactics.ml | 2 +- matita/components/ng_tactics/nTactics.mli | 1 + matita/components/ng_tactics/nnAuto.ml | 2 +- matita/components/ng_tactics/nnAuto.mli | 2 +- .../matita/lib/didactic/natural_deduction.ma | 863 ++++++++++++++++++ 11 files changed, 1304 insertions(+), 278 deletions(-) create mode 100644 matita/matita/lib/didactic/natural_deduction.ma diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index c15414df5..27f3830b6 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -90,10 +90,12 @@ type ntactic = | AndElim of loc * just * nterm * string * nterm * string | RewritingStep of loc * (string option * nterm) option * nterm * - [ `Term of nterm | `Auto of (string*string) list + [ `Term of nterm | `Auto of auto_params | `Proof | `SolveWith of nterm ] * bool (* last step*) | Thesisbecomes of loc * nterm * nterm option + (* This is a debug tactic to print the stack to stdout, can be safely removed *) + | PrintStack of loc type nmacro = | NCheck of loc * nterm diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 9e08fb3b5..a333dccfc 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -147,7 +147,7 @@ let rec pp_ntactic status ~map_unicode_to_tex = ^ "=" ^ NotationPp.pp_term status term1 ^ (match term2 with - | `Auto params -> pp_auto_params (None,params) status + | `Auto params -> pp_auto_params params status | `Term term2 -> " exact " ^ NotationPp.pp_term status term2 | `Proof -> " proof" | `SolveWith term -> " using " ^ NotationPp.pp_term status term) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 387468f19..c0faf6102 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -413,6 +413,7 @@ let eval_ng_tac tac = | None -> `Auto (None,params) | Some l -> `Auto (Some (List.map (fun t -> (text,prefix_len,t)) l),params) ) + | _ -> assert false in let rec aux f (text, prefix_len, tac) = match tac with @@ -508,10 +509,18 @@ let eval_ng_tac tac = text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2 | GrafiteAst.Thesisbecomes (_, t1, t2) -> Declarative.thesisbecomes (text,prefix_len,t1) (match t2 with None -> None | Some t2 -> (Some (text,prefix_len,t2))) - (* | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) -> - Declarative.rewritingstep termine (text,prefix_len,t1) t2 cont - *) + Declarative.rewritingstep (match termine with None -> None + | Some (s,t) -> Some (s, (text,prefix_len,t))) + (text,prefix_len,t1) + (match t2 with + `Term t -> just_to_tacstatus_just t2 text prefix_len + | `Auto params -> just_to_tacstatus_just t2 text prefix_len + |`Proof -> `Proof + |`SolveWith t -> `SolveWith (text,prefix_len,t) + ) + cont + | GrafiteAst.PrintStack (_) -> Declarative.print_stack in aux aux tac (* trick for non uniform recursion call *) ;; diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 714cb4826..1b60e9902 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -272,6 +272,7 @@ EXTEND | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term ; t2 = OPT [IDENT "or"; IDENT "equivalently"; t2 = tactic_term -> t2] -> G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)]) + | IDENT "print_stack" -> G.NTactic (loc,[G.PrintStack loc]) (* DO NOT FACTORIZE with the two following, camlp5 sucks*) | IDENT "conclude"; termine = tactic_term; @@ -281,7 +282,16 @@ EXTEND [ IDENT "using"; t=tactic_term -> `Term t | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term | IDENT "proof" -> `Proof - | params = auto_params -> let _,params = params in `Auto params]; + | params = auto_params -> `Auto + ( + let just,params = params in + match just with + | None -> (None,params) + | Some (`Univ univ) -> (Some univ,params) + (* `Trace behaves exaclty like None for the moment being *) + | Some (`Trace) -> (None,params) + ) + ]; cont = rewriting_step_continuation -> G.NTactic (loc,[G.RewritingStep(loc, Some (None,termine), t1, t2, cont)]) | IDENT "obtain" ; name = IDENT; @@ -292,7 +302,16 @@ EXTEND [ IDENT "using"; t=tactic_term -> `Term t | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term | IDENT "proof" -> `Proof - | params = auto_params -> let _,params = params in `Auto params]; + | params = auto_params -> `Auto + ( + let just,params = params in + match just with + | None -> (None,params) + | Some (`Univ univ) -> (Some univ,params) + (* `Trace behaves exaclty like None for the moment being *) + | Some (`Trace) -> (None,params) + ) + ]; cont = rewriting_step_continuation -> G.NTactic(loc,[G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)]) | SYMBOL "=" ; @@ -301,7 +320,16 @@ EXTEND [ IDENT "using"; t=tactic_term -> `Term t | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term | IDENT "proof" -> `Proof - | params = auto_params -> let _,params = params in `Auto params]; + | params = auto_params -> `Auto + ( + let just,params = params in + match just with + | None -> (None,params) + | Some (`Univ univ) -> (Some univ,params) + (* `Trace behaves exaclty like None for the moment being *) + | Some (`Trace) -> (None,params) + ) + ]; cont = rewriting_step_continuation -> G.NTactic(loc,[G.RewritingStep(loc, None, t1, t2, cont)]) ] diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml index ac521186a..3a700ba96 100644 --- a/matita/components/ng_tactics/declarative.ml +++ b/matita/components/ng_tactics/declarative.ml @@ -1,14 +1,14 @@ (* Copyright (C) 2019, HELM Team. - * + * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. - * + * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. - * + * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the @@ -18,327 +18,445 @@ * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. - * + * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. - *) +*) +open Continuationals.Stack module Ast = NotationPt open NTactics open NTacStatus type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ] -let mk_just = - function - `Auto (l,params) -> distribute_tac (fun status goal -> NnAuto.auto_lowtac - ~params:(l,params) status goal) - | `Term t -> apply_tac t +let mk_just status goal = + function + `Auto (l,params) -> NnAuto.auto_lowtac ~params:(l,params) status goal + | `Term t -> apply_tac t exception NotAProduct exception FirstTypeWrong exception NotEquivalentTypes +let extract_first_goal_from_status status = + let s = status#stack in + match s with + | [] -> fail (lazy "There's nothing to prove") + | (g1, _, k, tag1) :: tl -> + let goals = filter_open g1 in + let (loc::tl) = goals in + let goal = goal_of_loc (loc) in + goal ;; + (* + let (_,_,metasenv,_,_) = status#obj in + match metasenv with + | [] -> fail (lazy "There's nothing to prove") + | (hd,_) :: tl -> hd + *) + let extract_conclusion_type status goal = - let gty = get_goalty status goal in - let ctx = ctx_of gty in - let status,gty = term_of_cic_term status gty ctx in - gty + let gty = get_goalty status goal in + let ctx = ctx_of gty in + let status,gty = term_of_cic_term status gty ctx in + gty ;; let same_type_as_conclusion ty t status goal = - let gty = get_goalty status goal in - let ctx = ctx_of gty in - let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in - let (_,_,metasenv,subst,_) = status#obj in - let status,ty = term_of_cic_term status cicterm ctx in - if NCicReduction.alpha_eq status metasenv subst ctx t ty then - true - else - false + let gty = get_goalty status goal in + let ctx = ctx_of gty in + let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in + let (_,_,metasenv,subst,_) = status#obj in + let status,ty = term_of_cic_term status cicterm ctx in + if NCicReduction.alpha_eq status metasenv subst ctx t ty then + true + else + false ;; let are_convertible ty1 ty2 status goal = - let gty = get_goalty status goal in - let ctx = ctx_of gty in - let status,cicterm1 = disambiguate status ctx ty1 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in - let status,cicterm2 = disambiguate status ctx ty2 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in - NTacStatus.are_convertible status ctx cicterm1 cicterm2 + let gty = get_goalty status goal in + let ctx = ctx_of gty in + let status,cicterm1 = disambiguate status ctx ty1 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in + let status,cicterm2 = disambiguate status ctx ty2 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in + NTacStatus.are_convertible status ctx cicterm1 cicterm2 (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that -the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with -\lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ? + the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with + \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ? *) let lambda_abstract_tac id t1 t2 status goal = - match extract_conclusion_type status goal with - | NCic.Prod (_,t,_) -> - if same_type_as_conclusion t1 t status goal then - match t2 with - | None -> - let (_,_,t1) = t1 in - exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit - `JustOne)))) status goal - - | Some t2 -> - let status,res = are_convertible t1 t2 status goal in - if res then - let (_,_,t2) = t2 in - exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit - `JustOne)))) status goal - else - raise NotEquivalentTypes + match extract_conclusion_type status goal with + | NCic.Prod (_,t,_) -> + if same_type_as_conclusion t1 t status goal then + match t2 with + | None -> + let (_,_,t1) = t1 in + exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit + `JustOne))) (*status*) + | Some t2 -> + let status,res = are_convertible t1 t2 status goal in + if res then + let (_,_,t2) = t2 in + exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit + `JustOne))) (*status*) else - raise FirstTypeWrong - | _ -> raise NotAProduct + raise NotEquivalentTypes + else + raise FirstTypeWrong + | _ -> raise NotAProduct -let assume name ty eqty = - distribute_tac (fun status goal -> - try lambda_abstract_tac name ty eqty status goal - with - | NotAProduct -> fail (lazy "You can't assume without an universal quantification") - | FirstTypeWrong -> fail (lazy "The assumed type is wrong") - | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent") - ) +let assume name ty eqty (*status*) = +(* let goal = extract_first_goal_from_status status in *) + distribute_tac (fun status goal -> + try exec (lambda_abstract_tac name ty eqty status goal) status goal + with + | NotAProduct -> fail (lazy "You can't assume without an universal quantification") + | FirstTypeWrong -> fail (lazy "The assumed type is wrong") + | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent") + ) ;; -let suppose t1 id t2 = - distribute_tac (fun status goal -> - try lambda_abstract_tac id t1 t2 status goal - with - | NotAProduct -> fail (lazy "You can't suppose without a logical implication") - | FirstTypeWrong -> fail (lazy "The supposed proposition is different from the premise") - | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent") - ) +let suppose t1 id t2 (*status*) = +(* let goal = extract_first_goal_from_status status in *) + distribute_tac (fun status goal -> + try exec (lambda_abstract_tac id t1 t2 status goal) status goal + with + | NotAProduct -> fail (lazy "You can't suppose without a logical implication") + | FirstTypeWrong -> fail (lazy "The supposed proposition is different from the premise") + | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent") + ) ;; let assert_tac t1 t2 status goal continuation = - let t = extract_conclusion_type status goal in - if same_type_as_conclusion t1 t status goal then - match t2 with - | None -> exec continuation status goal - | Some t2 -> - let status,res = are_convertible t1 t2 status goal in - if res then - exec continuation status goal - else - raise NotEquivalentTypes + let t = extract_conclusion_type status goal in + if same_type_as_conclusion t1 t status goal then + match t2 with + | None -> continuation + | Some t2 -> + let status,res = are_convertible t1 t2 status goal in + if res then continuation + else + raise NotEquivalentTypes + else + raise FirstTypeWrong + +let mustdot status = + let s = status#stack in + match s with + | [] -> fail (lazy "No goals to dot") + | (_, _, k, _) :: tl -> + if List.length k > 0 then + true else - raise FirstTypeWrong + false -let we_need_to_prove t id t1 = - distribute_tac (fun status goal -> - match id with - | None -> - ( - match t1 with - | None -> (* We need to prove t *) - ( - try - assert_tac t None status goal id_tac - with - | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") - ) - | Some t1 -> (* We need to prove t or equivalently t1 *) - ( - try - assert_tac t (Some t1) status goal (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t1) - with - | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") - | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") - ) - ) - | Some id -> - ( - match t1 with - | None -> (* We need to prove t (id) *) - exec (block_tac [cut_tac t; branch_tac ~force:false; shift_tac; intro_tac id; - (*merge_tac*)]) status goal - | Some t1 -> (* We need to prove t (id) or equivalently t1 *) - exec (block_tac [cut_tac t; branch_tac ~force:false; change_tac ~where:("",0,(None,[],Some Ast.UserInput)) - ~with_what:t1; shift_tac; intro_tac id; merge_tac]) status goal - ) - ) +let bydone just status = + let goal = extract_first_goal_from_status status in + let mustdot = mustdot status in +(* + let goal,mustdot = + let s = status#stack in + match s with + | [] -> fail (lazy "Invalid use of done") + | (g1, _, k, tag1) :: tl -> + let goals = filter_open g1 in + let (loc::tl) = goals in + let goal = goal_of_loc (loc) in + if List.length k > 0 then + goal,true + else + goal,false + in + + *) +(* + let goals = filter_open g1 in + let (loc::tl) = goals in + let goal = goal_of_loc (loc) in + if tag1 == `BranchTag then + if List.length (shift_goals s) > 0 then (* must simply shift *) + ( + prerr_endline (pp status#stack); + prerr_endline "Head goals:"; + List.map (fun goal -> prerr_endline (string_of_int goal)) (head_goals status#stack); + prerr_endline "Shift goals:"; + List.map (fun goal -> prerr_endline (string_of_int goal)) (shift_goals status#stack); + prerr_endline "Open goals:"; + List.map (fun goal -> prerr_endline (string_of_int goal)) (open_goals status#stack); + if tag2 == `BranchTag && g2 <> [] then + goal,true,false,false + else if tag2 == `BranchTag then + goal,false,true,true + else + goal,false,true,false + ) + else + ( + if tag2 == `BranchTag then + goal,false,true,true + else + goal,false,true,false + ) + else + goal,false,false,false (* It's a strange situation, there's is an underlying level on the + stack but the current one was not created by a branch? Should be + an error *) + | (g, _, _, tag) :: [] -> + let (loc::tl) = filter_open g in + let goal = goal_of_loc (loc) in + if tag == `BranchTag then +(* let goals = filter_open g in *) + goal,false,true,false + else + goal,false,false,false + in + *) + let l = [mk_just status goal just] in + let l = + if mustdot then List.append l [dot_tac] else l + in + (* + let l = + if mustmerge then List.append l [merge_tac] else l + in + let l = + if mustmergetwice then List.append l [merge_tac] else l + in + *) + block_tac l status +(* + let (_,_,metasenv,subst,_) = status#obj in + let goal,last = + match metasenv with + | [] -> fail (lazy "There's nothing to prove") + | (_,_) :: (hd,_) :: tl -> hd,false + | (hd,_) :: tl -> hd,true + in + if last then + mk_just status goal just status + else + block_tac [ mk_just status goal just; shift_tac ] status +*) ;; -let by_just_we_proved just ty id ty' = - distribute_tac (fun status goal -> - let just = mk_just just in - match id with - | None -> - (match ty' with - | None -> (* just we proved P done *) - ( - try - assert_tac ty None status goal just - with - | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") - | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") - ) - | Some ty' -> (* just we proved P that is equivalent to P' done *) - ( - try - assert_tac ty' (Some ty) status goal (block_tac [change_tac - ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; just]) - with - | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion") - | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") - ) - ) - | Some id -> - ( - match ty' with - | None -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac - id; merge_tac ]) status goal - | Some ty' -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac - id; change_tac ~where:("",0,(None,[id,Ast.UserInput],None)) - ~with_what:ty'; merge_tac]) status goal - ) +let we_need_to_prove t id t1 status = + let goal = extract_first_goal_from_status status in + match id with + | None -> + ( + match t1 with + | None -> (* We need to prove t *) + ( + try assert_tac t None status goal (id_tac status) + with + | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") + ) + | Some t1 -> (* We need to prove t or equivalently t1 *) + ( + try assert_tac t (Some t1) status goal (change_tac ~where:("",0,(None,[],Some + Ast.UserInput)) ~with_what:t1 status) + with + | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") + | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") + ) + ) + | Some id -> + ( + match t1 with + (* We need to prove t (id) *) + | None -> block_tac [cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; + dot_tac + ] status + (* We need to prove t (id) or equivalently t1 *) + | Some t1 -> block_tac [cut_tac t; branch_tac ; change_tac ~where:("",0,(None,[],Some + Ast.UserInput)) + ~with_what:t1; shift_tac; intro_tac id; merge_tac; + dot_tac + ] + status ) ;; -let thesisbecomes t1 t2 = we_need_to_prove t1 None t2 ;; +let by_just_we_proved just ty id ty' (*status*) = + distribute_tac (fun status goal -> + let wrappedjust = just in + let just = mk_just status goal just in + match id with + | None -> + (match ty' with + | None -> (* just we proved P done *) + ( + try + assert_tac ty None status goal (exec (bydone wrappedjust) status goal) + with + | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") + | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") + ) + | Some ty' -> (* just we proved P that is equivalent to P' done *) + ( + try + assert_tac ty' (Some ty) status goal (exec (block_tac [change_tac + ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; bydone + wrappedjust]) status goal) + with + | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion") + | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent") + ) + ) + | Some id -> + ( + match ty' with + | None -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac + id; merge_tac ]) status goal + | Some ty' -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac + id; change_tac ~where:("",0,(None,[id,Ast.UserInput],None)) + ~with_what:ty'; merge_tac]) status goal + ) + ) +;; -let bydone just = - mk_just just +let thesisbecomes t1 t2 status = we_need_to_prove t1 None t2 status ;; -let existselim just id1 t1 t2 id2 = +let existselim just id1 t1 t2 id2 (*status*) = + distribute_tac (fun status goal -> let (_,_,t1) = t1 in let (_,_,t2) = t2 in - let just = mk_just just in - block_tac [ - cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident - (id1,None), Some t1),t2)])); - branch_tac ~force:false; - just; - shift_tac; - case1_tac "_"; - intros_tac ~names_ref:(ref []) [id1;id2]; - merge_tac - ] + let just = mk_just status goal just in + exec (block_tac [ + cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident + (id1,None), Some t1),t2)])); + branch_tac ~force:false; + just; + shift_tac; + case1_tac "_"; + intros_tac ~names_ref:(ref []) [id1;id2]; + merge_tac + ]) status goal + ) +;; -let andelim just t1 id1 t2 id2 = +let andelim just t1 id1 t2 id2 (*status*) = +(* let goal = extract_first_goal_from_status status in *) + distribute_tac (fun status goal -> let (_,_,t1) = t1 in let (_,_,t2) = t2 in - let just = mk_just just in - block_tac [ - cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2])); - branch_tac ~force:false; - just; - shift_tac; - case1_tac "_"; - intros_tac ~names_ref:(ref []) [id1;id2]; - merge_tac - ] + let just = mk_just status goal just in + exec (block_tac [ + cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2])); + branch_tac ~force:false; + just; + shift_tac; + case1_tac "_"; + intros_tac ~names_ref:(ref []) [id1;id2]; + merge_tac + ]) status goal + ) ;; +let type_of_tactic_term status ctx t = + let status,cicterm = disambiguate status ctx t `XTNone in + let (_,cicty) = typeof status ctx cicterm in + cicty - -let rewritingstep lhs rhs just last_step = fail (lazy "Not implemented"); - (* - let aux ((proof,goal) as status) = - let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in - let _,context,gty = CicUtil.lookup_meta goal metasenv in - let eq,trans = - match LibraryObjects.eq_URI () with - None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command")) - | Some uri -> - Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[]) - in - let ty,_ = - CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.oblivion_ugraph in - let just' = - match just with +let rewritingstep lhs rhs just last_step status = + let goal = extract_first_goal_from_status status in + let cicgty = get_goalty status goal in + let ctx = ctx_of cicgty in + let _,gty = term_of_cic_term status cicgty ctx in + let cicty = type_of_tactic_term status ctx rhs in + let _,ty = term_of_cic_term status cicty ctx in + let just' = (* Extraction of the ""justification"" from the ad hoc justification *) + match just with `Auto (univ, params) -> - let params = - if not (List.exists (fun (k,_) -> k = "timeout") params) then + let params = + if not (List.mem_assoc "timeout" params) then ("timeout","3")::params - else params - in - let params' = - if not (List.exists (fun (k,_) -> k = "paramodulation") params) then + else params + in + let params' = + if not (List.mem_assoc "paramodulation" params) then ("paramodulation","1")::params - else params - in - if params = params' then - Tactics.auto ~dbd ~params:(univ, params) ~automation_cache - else - Tacticals.first - [Tactics.auto ~dbd ~params:(univ, params) ~automation_cache ; - Tactics.auto ~dbd ~params:(univ, params') ~automation_cache] - | `Term just -> Tactics.apply just - | `SolveWith term -> - Tactics.demodulate ~automation_cache ~dbd - ~params:(Some [term], - ["all","1";"steps","1"; "use_context","false"]) - | `Proof -> - Tacticals.id_tac + else params + in + if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal + else + first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac + ~params:(univ, params') status goal] + | `Term just -> apply_tac just + | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"]) + | `Proof -> id_tac in - let plhs,prhs,prepare = + let plhs,prhs,prepare = match lhs with - None -> - let plhs,prhs = - match gty with - Cic.Appl [_;_;plhs;prhs] -> plhs,prhs - | _ -> assert false - in - plhs,prhs, - (fun continuation -> - ProofEngineTypes.apply_tactic continuation status) - | Some (None,lhs) -> - let plhs,prhs = - match gty with - Cic.Appl [_;_;plhs;prhs] -> plhs,prhs - | _ -> assert false - in - (*CSC: manca check plhs convertibile con lhs *) - plhs,prhs, - (fun continuation -> - ProofEngineTypes.apply_tactic continuation status) - | Some (Some name,lhs) -> - let newmeta = CicMkImplicit.new_meta metasenv [] in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in - let plhs = lhs in - let prhs = Cic.Meta(newmeta,irl) in - plhs,prhs, - (fun continuation -> - let metasenv = (newmeta, context, ty)::metasenv in - let mk_fresh_name_callback = - fun metasenv context _ ~typ -> - FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context + None -> (* = E2 *) + let plhs,prhs = + match gty with (* Extracting the lhs and rhs of the previous equality *) + NCic.Appl [_;_;plhs;prhs] -> plhs,prhs + | _ -> fail (lazy "You are not building an equaility chain") + in + plhs,prhs, + (fun continuation -> continuation status) + | Some (None,lhs) -> (* conclude *) + let plhs,prhs = + match gty with + NCic.Appl [_;_;plhs;prhs] -> plhs,prhs + | _ -> fail (lazy "You are not building an equaility chain") + in + (*TODO*) + (*CSC: manca check plhs convertibile con lhs *) + plhs,prhs, + (fun continuation -> continuation status) + | Some (Some name,lhs) -> (* obtain *) + fail (lazy "Not implemented") + (* + let plhs = lhs in + let prhs = Cic.Meta(newmeta,irl) in + plhs,prhs, + (fun continuation -> + let metasenv = (newmeta, ctx, ty)::metasenv in + let mk_fresh_name_callback = + fun metasenv ctx _ ~typ -> + FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv ctx (Cic.Name name) ~typ - in - let proof = curi,metasenv,_subst,proofbo,proofty, attrs in - let proof,goals = - ProofEngineTypes.apply_tactic - (Tacticals.thens + in + let proof = curi,metasenv,_subst,proofbo,proofty, attrs in + let proof,goals = + ProofEngineTypes.apply_tactic + (Tacticals.thens ~start:(Tactics.cut ~mk_fresh_name_callback - (Cic.Appl [eq ; ty ; lhs ; prhs])) + (Cic.Appl [eq ; ty ; lhs ; prhs])) ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal) - in - let goals = - match just,goals with - `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1] - | _, [g1;g2] -> [g2;newmeta;g1] - | _, l -> - prerr_endline (String.concat "," (List.map string_of_int l)); - prerr_endline (CicMetaSubst.ppmetasenv [] metasenv); - assert false - in - proof,goals) - in - let continuation = - if last_step then + in + let goals = + match just,goals with + `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1] + | _, [g1;g2] -> [g2;newmeta;g1] + | _, l -> + prerr_endline (String.concat "," (List.map string_of_int l)); + prerr_endline (CicMetaSubst.ppmetasenv [] metasenv); + assert false + in + proof,goals) + *) + in + let continuation = + if last_step then (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*) - just' - else - Tacticals.thens - ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs])) - ~continuations:[just' ; Tacticals.id_tac] - in - prepare continuation - in - ProofEngineTypes.mk_tactic aux + let todo = [just'] in + let todo = if mustdot status then List.append todo [dot_tac] else todo + in + block_tac todo + else + let (_,_,rhs) = rhs in + block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs; + rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac] + in + prepare continuation ;; - *) + +let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;; + +(* vim: ts=2: sw=0: et: + * *) diff --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli index d96a8fd73..5b154382f 100644 --- a/matita/components/ng_tactics/declarative.mli +++ b/matita/components/ng_tactics/declarative.mli @@ -36,3 +36,8 @@ NTacStatus.tactic val existselim : just -> string -> NTacStatus.tactic_term -> NTacStatus.tactic_term -> string -> 's NTacStatus.tactic val thesisbecomes : NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic +val rewritingstep : (string option * NTacStatus.tactic_term) option -> NTacStatus.tactic_term -> + [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params + | `Proof | `SolveWith of NTacStatus.tactic_term ] -> + bool (* last step *) -> 's NTacStatus.tactic +val print_stack : 's NTacStatus.tactic diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 3ef2dbe5b..ed98b6d1e 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -53,7 +53,7 @@ let branch_tac ?(force=false) status = | (g, t, k, tag) :: s -> match init_pos g with (* TODO *) | [] -> fail (lazy "empty goals") - | [_] when (not force) -> fail (lazy "too few goals to branch") + | [_] when (not force) -> fail (lazy "too few goals to branch") | loc :: loc_tl -> ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s in diff --git a/matita/components/ng_tactics/nTactics.mli b/matita/components/ng_tactics/nTactics.mli index fd5916c8d..250b26991 100644 --- a/matita/components/ng_tactics/nTactics.mli +++ b/matita/components/ng_tactics/nTactics.mli @@ -92,3 +92,4 @@ val inversion_tac: 's NTacStatus.tactic val exact_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic +val first_tac: 's NTacStatus.tactic list -> 's NTacStatus.tactic diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index d0ff9c082..21f1e42e8 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -1915,7 +1915,7 @@ let auto_lowtac ~params:(univ,flags) status goal = let gty = get_goalty status goal in let ctx = ctx_of gty in let candidates = candidates_from_ctx univ ctx status in - NTactics.exec (auto_tac' candidates ~local_candidates:false ~use_given_only:true flags) status goal + auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref:(ref []) let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = let candidates = candidates_from_ctx univ [] status in diff --git a/matita/components/ng_tactics/nnAuto.mli b/matita/components/ng_tactics/nnAuto.mli index b0d724379..d77d32085 100644 --- a/matita/components/ng_tactics/nnAuto.mli +++ b/matita/components/ng_tactics/nnAuto.mli @@ -28,7 +28,7 @@ val auto_tac: ?trace_ref:NotationPt.term list ref -> 's NTacStatus.tactic -val auto_lowtac: params:auto_params -> NTacStatus.lowtac_status -> int -> NTacStatus.lowtac_status +val auto_lowtac: params:auto_params -> #NTacStatus.pstatus -> int -> 's NTacStatus.tactic val keys_of_type: (#NTacStatus.pstatus as 'a) -> diff --git a/matita/matita/lib/didactic/natural_deduction.ma b/matita/matita/lib/didactic/natural_deduction.ma new file mode 100644 index 000000000..45ce24f91 --- /dev/null +++ b/matita/matita/lib/didactic/natural_deduction.ma @@ -0,0 +1,863 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +(* Logic system *) + +include "basics/pts.ma". +include "hints_declaration.ma". + +inductive Imply (A,B:Prop) : Prop ≝ +| Imply_intro: (A → B) → Imply A B. + +definition Imply_elim ≝ λA,B:Prop.λf:Imply A B. λa:A. + match f with [ Imply_intro g ⇒ g a]. + +inductive And (A,B:Prop) : Prop ≝ +| 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:Prop) : Prop ≝ +| Or_intro_l: A → Or A B +| Or_intro_r: B → Or A B. + +definition Or_elim ≝ λA,B,C:Prop.λ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 : Prop := +| Top_intro : Top. + +inductive Bot : Prop := . + +definition Bot_elim ≝ λP:Prop.λx:Bot. + match x in Bot return λx.P with []. + +definition Not := λA:Prop.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 Discharge := λA:Prop.λa:A. + a. + +axiom Raa : ∀A.(Not A → Bot) → A. + +axiom sort : Type[0]. + +inductive Exists (A:Type[0]) (P:A→Prop) : Prop ≝ + Exists_intro: ∀w:A. P w → Exists A P. + +definition Exists_elim ≝ + λA:Type[0].λP:A→Prop.λC:Prop.λc:Exists A P.λH:(Πx.P x → C). + match c with [ Exists_intro w p ⇒ H w p ]. + +inductive Forall (A:Type[0]) (P:A→Prop) : Prop ≝ + Forall_intro: (∀n:A. P n) → Forall A P. + +definition Forall_elim ≝ + λA:Type[0].λP:A→Prop.λn:A.λf:Forall A P.match f with [ Forall_intro g ⇒ g n ]. + +(* Dummy proposition *) +axiom unit : Prop. + +(* 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. +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 : Prop. +axiom B : Prop. +axiom C : Prop. +axiom D : Prop. +axiom E : Prop. +axiom F : Prop. +axiom G : Prop. +axiom H : Prop. +axiom I : Prop. +axiom J : Prop. +axiom K : Prop. +axiom L : Prop. +axiom M : Prop. +axiom N : Prop. +axiom O : Prop. +axiom x: sort. +axiom y: sort. +axiom z: sort. +axiom w: sort. + +(* Every formula user provided annotates its proof: + `A` becomes `(show A ?)` *) +definition show : ΠA.A→A ≝ λA:Prop.λa:A.a. + +(* When something does not fit, this daemon is used *) +axiom cast: ΠA,B:Prop.B → A. + +(* begin a proof: draws the root *) +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 ?). + +(* Leaves *) +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 ? ? (show a t)). + +(* discharging *) +notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 +for @{ 'discharge_ko_1 $a $H }. +interpretation "discharge_ko_1" 'discharge_ko_1 a H = + (show a (cast ? ? (Discharge ? H))). +notation < "[ mstyle color #ff0000 (a) ] \sup mstyle color #ff0000 (H)" with precedence 19 +for @{ 'discharge_ko_2 $a $H }. +interpretation "discharge_ko_2" 'discharge_ko_2 a H = + (cast ? ? (show a (cast ? ? (Discharge ? H)))). + +notation < "[ a ] \sup H" with precedence 19 +for @{ 'discharge_ok_1 $a $H }. +interpretation "discharge_ok_1" 'discharge_ok_1 a H = + (show a (Discharge ? H)). +notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 +for @{ 'discharge_ok_2 $a $H }. +interpretation "discharge_ok_2" 'discharge_ok_2 a H = + (cast ? ? (show a (Discharge ? H))). + +notation > "'discharge' [H]" with precedence 19 +for @{ 'discharge $H }. +interpretation "discharge KO" 'discharge H = (cast ? ? (Discharge ? H)). +interpretation "discharge OK" 'discharge H = (Discharge ? H). + +(* ⇒ introduction *) +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_2" 'Imply_intro_ko_2 ab \eta.b = + (cast ? ? (show ab (cast ? ? (Imply_intro ? ? b)))). + +notation < "maction (\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) ) (\vdots)" 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). + +(* ⇒ elimination *) +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 ? ? (cast ? ? ab) (cast ? ? 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 ? ? (cast ? ? ab) (cast ? ? a))))). + +notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) ) (\vdots)" 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). + +(* ∧ introduction *) +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 < "maction (\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)) (\vdots)" 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). + +(* ∧ elimination *) +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 ? ? (cast ? ? 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 ? ? (cast ? ? ab))))). + +notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))) (\vdots)" 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 = (cast ? ? (And_elim_l ? ? (cast (And unit 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 ? ? (cast ? ? 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 ? ? (cast ? ? ab))))). + +notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))) (\vdots)" 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 = (cast ? ? (And_elim_r ? ? (cast (And unit unit) ? a))). +interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r ? ? a). + +(* ∨ introduction *) +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 < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))) (\vdots)" 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_2 $a $ab }. +interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = + (cast ? ? (show ab (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 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 < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))) (\vdots)" 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_2 $a $ab }. +interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = + (cast ? ? (show ab (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). + +(* ∨ elimination *) +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 ? ? ? (cast ? ? 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 ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc))))). + +notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)) (\vdots)" 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))). + +definition unit_to ≝ λx:Prop.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 ?) }. +interpretation "Or_elim KO" 'Or_elim ab ac bc = + (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 = (Or_elim ? ? ? ab ac bc). + +(* ⊤ introduction *) +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 mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19 +for @{'Top_intro_ko_2}. +interpretation "Top_intro_ko_2" 'Top_intro_ko_2 = + (cast ? ? (show ? (cast ? ? Top_intro))). + +notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19 +for @{'Top_intro_ok_1}. +interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show ? Top_intro). + +notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19 +for @{'Top_intro_ok_2 }. +interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast ? ? (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. + +(* ⊥ introduction *) +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 ? (cast ? ? b))). + +notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19 +for @{'Bot_elim_ko_2 $a $b}. +interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b = + (cast ? ? (show a (Bot_elim ? (cast ? ? b)))). + +notation < "maction (\infrule b a (⊥\sub\e)) (\vdots)" 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 ? b)). + +notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19 +for @{'Bot_elim_ok_2 $a $b}. +interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b = + (cast ? ? (show a (Bot_elim ? 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). + +(* ¬ introduction *) +notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\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(\emsp\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 < "maction (\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) ) (\vdots)" 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(\emsp\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). + +(* ¬ elimination *) +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19 +for @{ 'Not_elim_ko_1 $ab $a $b }. +interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b = + (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a)))). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19 +for @{ 'Not_elim_ko_2 $ab $a $b }. +interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b = + (cast ? ? (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a))))). + +notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) ) (\vdots)" 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(\emsp\e)) " with precedence 19 +for @{ 'Not_elim_ok_2 $ab $a $b }. +interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b = + (cast ? ? (show b (Not_elim ? ab a))). + +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 = + (cast ? ? (Not_elim unit (cast ? ? ab) (cast ? ? a))). +interpretation "Not_elim OK" 'Not_elim ab a = + (Not_elim ? ab a). + +(* RAA *) +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 (cast ? ? (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 (cast ? ? (Raa ? (cast ? ? Px))))). + +notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)) (\vdots)" 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 > "'RAA' [ident H] term 90 b" with precedence 19 +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). + +(* ∃ 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 < "maction (\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)) (\vdots)" 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 (λw.? w) (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 < "maction (\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)) (\vdots)" 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:sort → Prop.Πy:sort.unit → x y. +definition ex_concl_dummy := Πy:sort.unit → unit. +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 (λx.? x) (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_dummy (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 < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)) (\vdots)" 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 < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)) (\vdots)" 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). + +(* already proved lemma *) +definition hide_args : ΠA:Type[0].A→A := λA:Type[0].λa:A.a. +notation < "t" non associative with precedence 90 for @{'hide_args $t}. +interpretation "hide 0 args" 'hide_args t = (hide_args ? t). +interpretation "hide 1 args" 'hide_args t = (hide_args ? t ?). +interpretation "hide 2 args" 'hide_args t = (hide_args ? t ? ?). +interpretation "hide 3 args" 'hide_args t = (hide_args ? t ? ? ?). +interpretation "hide 4 args" 'hide_args t = (hide_args ? t ? ? ? ?). +interpretation "hide 5 args" 'hide_args t = (hide_args ? t ? ? ? ? ?). +interpretation "hide 6 args" 'hide_args t = (hide_args ? t ? ? ? ? ? ?). +interpretation "hide 7 args" 'hide_args t = (hide_args ? t ? ? ? ? ? ? ?). + +(* more args crashes the pattern matcher *) + +(* already proved lemma, 0 assumptions *) +definition Lemma : ΠA.A→A ≝ λA:Prop.λa:A.a. + +notation < "\infrule + (\infrule + (\emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma_ko_1 $p ($H : $_) }. +interpretation "lemma_ko_1" 'lemma_ko_1 p H = + (show p (cast ? ? (Lemma ? (cast ? ? H)))). + +notation < "\infrule + (\infrule + (\emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma_ko_2 $p ($H : $_) }. +interpretation "lemma_ko_2" 'lemma_ko_2 p H = + (cast ? ? (show p (cast ? ? + (Lemma ? (cast ? ? H))))). + + +notation < "\infrule + (\infrule + (\emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma_ok_1 $p ($H : $_) }. +interpretation "lemma_ok_1" 'lemma_ok_1 p H = + (show p (Lemma ? H)). + +notation < "\infrule + (\infrule + (\emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma_ok_2 $p ($H : $_) }. +interpretation "lemma_ok_2" 'lemma_ok_2 p H = + (cast ? ? (show p (Lemma ? H))). + +notation > "'lem' 0 term 90 l" non associative with precedence 19 +for @{ 'Lemma (hide_args ? $l : ?) }. +interpretation "lemma KO" 'Lemma l = + (cast ? ? (Lemma unit (cast unit ? l))). +interpretation "lemma OK" 'Lemma l = (Lemma ? l). + + +(* already proved lemma, 1 assumption *) +definition Lemma1 : ΠA,B. (A ⇒ B) → A → B ≝ + λA,B:Prop.λf:A⇒B.λa:A. + Imply_elim A B f a. + +notation < "\infrule + (\infrule + (\emsp a \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma1_ko_1 $a $p ($H : $_) }. +interpretation "lemma1_ko_1" 'lemma1_ko_1 a p H = + (show p (cast ? ? (Lemma1 ? ? (cast ? ? H) (cast ? ? a)))). + +notation < "\infrule + (\infrule + (\emsp a \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma1_ko_2 $a $p ($H : $_) }. +interpretation "lemma1_ko_2" 'lemma1_ko_2 a p H = + (cast ? ? (show p (cast ? ? + (Lemma1 ? ? (cast ? ? H) (cast ? ? a))))). + + +notation < "\infrule + (\infrule + (\emsp a \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma1_ok_1 $a $p ($H : $_) }. +interpretation "lemma1_ok_1" 'lemma1_ok_1 a p H = + (show p (Lemma1 ? ? H a)). + +notation < "\infrule + (\infrule + (\emsp a \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma1_ok_2 $a $p ($H : $_) }. +interpretation "lemma1_ok_2" 'lemma1_ok_2 a p H = + (cast ? ? (show p (Lemma1 ? ? H a))). + + +notation > "'lem' 1 term 90 l term 90 p" non associative with precedence 19 +for @{ 'Lemma1 (hide_args ? $l : ?) (show $p ?) }. +interpretation "lemma 1 KO" 'Lemma1 l p = + (cast ? ? (Lemma1 unit unit (cast (Imply unit unit) ? l) (cast unit ? p))). +interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 ? ? l p). + +(* already proved lemma, 2 assumptions *) +definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝ + λA,B,C:Prop.λf:A⇒B⇒C.λa:A.λb:B. + Imply_elim B C (Imply_elim A (B⇒C) f a) b. + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma2_ko_1 $a $b $p ($H : $_) }. +interpretation "lemma2_ko_1" 'lemma2_ko_1 a b p H = + (show p (cast ? ? (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b)))). + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma2_ko_2 $a $b $p ($H : $_) }. +interpretation "lemma2_ko_2" 'lemma2_ko_2 a b p H = + (cast ? ? (show p (cast ? ? + (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b))))). + + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma2_ok_1 $a $b $p ($H : $_) }. +interpretation "lemma2_ok_1" 'lemma2_ok_1 a b p H = + (show p (Lemma2 ? ? ? H a b)). + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma2_ok_2 $a $b $p ($H : $_) }. +interpretation "lemma2_ok_2" 'lemma2_ok_2 a b p H = + (cast ? ? (show p (Lemma2 ? ? ? H a b))). + +notation > "'lem' 2 term 90 l term 90 p term 90 q" non associative with precedence 19 +for @{ 'Lemma2 (hide_args ? $l : ?) (show $p ?) (show $q ?) }. +interpretation "lemma 2 KO" 'Lemma2 l p q = + (cast ? ? (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) ? l) (cast unit ? p) (cast unit ? q))). +interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 ? ? ? l p q). + +(* already proved lemma, 3 assumptions *) +definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝ + λA,B,C,D:Prop.λf:A⇒B⇒C⇒D.λa:A.λb:B.λc:C. + Imply_elim C D (Imply_elim B (C⇒D) (Imply_elim A (B⇒C⇒D) f a) b) c. + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma3_ko_1 $a $b $c $p ($H : $_) }. +interpretation "lemma3_ko_1" 'lemma3_ko_1 a b c p H = + (show p (cast ? ? + (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c)))). + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma3_ko_2 $a $b $c $p ($H : $_) }. +interpretation "lemma3_ko_2" 'lemma3_ko_2 a b c p H = + (cast ? ? (show p (cast ? ? + (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c))))). + + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma3_ok_1 $a $b $c $p ($H : $_) }. +interpretation "lemma3_ok_1" 'lemma3_ok_1 a b c p H = + (show p (Lemma3 ? ? ? ? H a b c)). + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma3_ok_2 $a $b $c $p ($H : $_) }. +interpretation "lemma3_ok_2" 'lemma3_ok_2 a b c p H = + (cast ? ? (show p (Lemma3 ? ? ? ? H a b c))). + +notation > "'lem' 3 term 90 l term 90 p term 90 q term 90 r" non associative with precedence 19 +for @{ 'Lemma3 (hide_args ? $l : ?) (show $p ?) (show $q ?) (show $r ?) }. +interpretation "lemma 3 KO" 'Lemma3 l p q r = + (cast ? ? (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) ? l) (cast unit ? p) (cast unit ? q) (cast unit ? r))). +interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 ? ? ? ? l p q r). -- 2.39.2