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