justification, conclusion, identifier, eqconcl *)
| We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
identifier, equivnewcon *)
+ | BetaRewritingStep of loc * nterm
| Bydone of loc * just
| ExistsElim of loc * just * string * nterm * nterm * string
| AndElim of loc * just * nterm * string * nterm * string
| By_just_we_proved (_, just, term1, ident, term2) -> pp_just status just ^ "we proved" ^
NotationPp.pp_term status term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ (match
term2 with None -> " " | Some term2 -> " that is equivalent to " ^ NotationPp.pp_term status term2)
- | We_need_to_prove (_,term,ident,term1) -> "we need to prove" ^ NotationPp.pp_term status term ^
- (match ident with None -> " " | Some id -> "(" ^ id ^ ")") ^ (match term1 with None -> " " | Some t1
- -> "or equivalently" ^ NotationPp.pp_term status t1)
+ | We_need_to_prove (_,term,ident,t) -> "we need to prove" ^ NotationPp.pp_term status term ^
+ (match ident with None -> " " | Some id -> "(" ^ id ^ ")") ^ (match t with None -> "" | Some t ->
+ " or equivalently " ^ (NotationPp.pp_term status t))
+ | BetaRewritingStep (_,t) -> "or equivalently " ^ (NotationPp.pp_term status t)
| Bydone (_, just) -> pp_just status just ^ "done"
| ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ":"
^ NotationPp.pp_term status term ^ "such that " ^ NotationPp.pp_term status term1 ^ "(" ^ ident1 ^ ")"
| AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ "we have " ^
NotationPp.pp_term status term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ NotationPp.pp_term status term2
^ " (" ^ ident2 ^ ")"
- | Thesisbecomes (_, term1, term2) -> "the thesis becomes " ^ NotationPp.pp_term status term1 ^ (match
- term2 with None -> " " | Some term2 -> NotationPp.pp_term status term2)
+ | Thesisbecomes (_, t, t1) -> "the thesis becomes " ^ NotationPp.pp_term status t ^
+ (match t1 with None -> "" | Some t1 -> " or equivalently " ^
+ NotationPp.pp_term status
+ t1)
| RewritingStep (_, rhs, just, cont) ->
"=" ^
NotationPp.pp_term status rhs ^
| `Proof -> " proof"
| `SolveWith t -> " using " ^ NotationPp.pp_term status t)
^ (if cont then " done" else "")
-(*
- | RewritingStep (_, term, term1, term2, cont) ->
- (match term with
- | None -> " "
- | Some (None,term) -> "conclude " ^ NotationPp.pp_term status term
- | Some (Some name,term) ->
- "obtain (" ^ name ^ ") " ^ NotationPp.pp_term status term)
- ^ "=" ^
- NotationPp.pp_term status term1 ^
- (match term2 with
- | `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)
- ^ (if cont then " done" else "")
-*)
| Obtain (_,id,t1) -> "obtain (" ^ id ^ ")" ^ NotationPp.pp_term status t1
| Conclude (_,t1) -> "conclude " ^ NotationPp.pp_term status t1
| We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ NotationPp.pp_term status term ^ "to prove" ^ NotationPp.pp_term status term1
|GrafiteAst.By_just_we_proved (_,j,t1,s,t2) -> Declarative.by_just_we_proved
(just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s (match t2 with None -> None |
Some t2 -> (Some (text,prefix_len,t2)))
- |GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove (text,prefix_len,t) id
- (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2))
+ |GrafiteAst.We_need_to_prove (_, t, id, t1) -> Declarative.we_need_to_prove (text,prefix_len,t) id
+ (match t1 with None -> None | Some t1 -> Some (text,prefix_len,t1))
+ |GrafiteAst.BetaRewritingStep (_, t) -> Declarative.beta_rewriting_step (text,prefix_len,t)
| GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len)
| GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) ->
Declarative.existselim (just_to_tacstatus_just just text prefix_len) id1 (text,prefix_len,t1)
| GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> Declarative.andelim (just_to_tacstatus_just just
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)))
+ (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2))
| GrafiteAst.RewritingStep (_,rhs,just,cont) ->
Declarative.rewritingstep (text,prefix_len,rhs)
(match just with
| BYC_wehaveand (id1,t1,id2,t2) ->
G.AndElim (loc, just, t1, id1, t2, id2))
])
- | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id =
+IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term ->
+t']->
G.NTactic (loc,[G.We_need_to_prove (loc, t, id, t1)])
+ | IDENT "or"; IDENT "equivalently"; t = tactic_term -> G.NTactic(loc,[G.BetaRewritingStep (loc,t)])
| IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term ; t2 = OPT [IDENT "or"; IDENT
- "equivalently"; t2 = tactic_term -> t2] ->
+"equivalently"; t2 = tactic_term -> t2] ->
G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)])
| IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
G.NTactic (loc,[G.We_proceed_by_cases_on (loc, t, t1)])
type goal = int
+type parameters = (string * string) list
+
module Stack =
struct
type switch = Open of goal | Closed of goal
type locator = int * switch
type tag = [ `BranchTag | `FocusTag | `NoTag ]
- type entry = locator list * locator list * locator list * tag
+ type entry = locator list * locator list * locator list * tag * parameters
type t = entry list
- let empty = [ [], [], [], `NoTag ]
+ let empty = [ [], [], [], `NoTag , []]
let fold ~env ~cont ~todo init stack =
let rec aux acc depth =
function
| [] -> acc
- | (locs, todos, conts, tag) :: tl ->
+ | (locs, todos, conts, tag, p) :: tl ->
let acc = List.fold_left (fun acc -> env acc depth tag) acc locs in
let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in
let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in
let map ~env ~cont ~todo =
let depth = ref ~-1 in
List.map
- (fun (s, t, c, tag) ->
+ (fun (s, t, c, tag, p) ->
incr depth;
let d = !depth in
- env d tag s, todo d tag t, cont d tag c, tag)
+ env d tag s, todo d tag t, cont d tag c, tag, p)
let is_open = function _, Open _ -> true | _ -> false
let close = function n, Open g -> n, Closed g | l -> l
let rec find_goal =
function
| [] -> raise (Failure "Continuationals.find_goal")
- | (l :: _, _ , _ , _) :: _ -> goal_of_loc l
- | ( _ , _ , l :: _, _) :: _ -> goal_of_loc l
- | ( _ , l :: _, _ , _) :: _ -> goal_of_loc l
+ | (l :: _, _ , _ , _, _) :: _ -> goal_of_loc l
+ | ( _ , _ , l :: _, _, _) :: _ -> goal_of_loc l
+ | ( _ , l :: _, _ , _, _) :: _ -> goal_of_loc l
| _ :: tl -> find_goal tl
let is_empty =
function
| [] -> assert false
- | [ [], [], [], `NoTag ] -> true
+ | [ [], [], [], `NoTag , _] -> true
| _ -> false
let of_nmetasenv metasenv =
let goals = List.map (fun (g, _) -> g) metasenv in
- [ zero_pos goals, [], [], `NoTag ]
+ [ zero_pos goals, [], [], `NoTag , []]
let head_switches =
function
- | (locs, _, _, _) :: _ -> List.map switch_of_loc locs
+ | (locs, _, _, _, _) :: _ -> List.map switch_of_loc locs
| [] -> assert false
let head_goals =
function
- | (locs, _, _, _) :: _ -> List.map goal_of_loc locs
+ | (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs
| [] -> assert false
let head_tag =
function
- | (_, _, _, tag) :: _ -> tag
+ | (_, _, _, tag, _) :: _ -> tag
| [] -> assert false
let shift_goals =
function
- | _ :: (locs, _, _, _) :: _ -> List.map goal_of_loc locs
+ | _ :: (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs
| [] -> assert false
| _ -> []
let pp_loc (i, s) = string_of_int i ^ pp_switch s in
let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in
let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in
- let pp_stack_entry (env, todo, cont, tag) =
- sprintf "(%s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont)
- (pp_tag tag)
+ let pp_par = function [] -> "" | _ as l -> List.fold_left (fun acc (k,v) -> acc ^ "K: " ^ k ^ " V: " ^ v ^ "; ") "" l in
+ let pp_stack_entry (env, todo, cont, tag, parameters) =
+ sprintf "(%s, %s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont)
+ (pp_tag tag) (pp_par parameters)
in
String.concat " :: " (List.map pp_stack_entry stack)
end
let ostatus, stack =
match cmd, stack with
| _, [] -> assert false
- | Tactical tac, (g, t, k, tag) :: s ->
+ | Tactical tac, (g, t, k, tag, p) :: s ->
(* COMMENTED OUT TO ALLOW PARAMODULATION TO DO A
* auto paramodulation.try assumption.
* EVEN IF NO GOALS ARE LEFT OPEN BY AUTO.
debug_print (lazy ("closed: "
^ String.concat " " (List.map string_of_int gcn)));
let stack =
- (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
+ (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s
in
sn, stack
- | Dot, ([], _, [], _) :: _ ->
+ | Dot, ([], _, [], _, _) :: _ ->
(* backward compatibility: do-nothing-dot *)
new_stack stack
- | Dot, (g, t, k, tag) :: s ->
+ | Dot, (g, t, k, tag, p) :: s ->
(match filter_open g, k with
- | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag) :: s)
+ | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag, p) :: s)
| [], loc :: k ->
assert (is_open loc);
- new_stack (([ loc ], t, k, tag) :: s)
+ new_stack (([ loc ], t, k, tag, p) :: s)
| _ -> fail (lazy "can't use \".\" here"))
| Semicolon, _ -> new_stack stack
- | Branch, (g, t, k, tag) :: s ->
+ | Branch, (g, t, k, tag, p) :: s ->
(match init_pos g with
| [] | [ _ ] -> fail (lazy "too few goals to branch");
| loc :: loc_tl ->
new_stack
- (([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s))
- | Shift, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
+ (([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag,p) :: s))
+ | Shift, (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s ->
(match g' with
| [] -> fail (lazy "no more goals to shift")
| loc :: loc_tl ->
new_stack
- (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
- :: (loc_tl, t', k', tag) :: s))
+ (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p)
+ :: (loc_tl, t', k', tag, p') :: s))
| Shift, _ -> fail (lazy "can't shift goals here")
- | Pos i_s, ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+ | Pos i_s, ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s
when is_fresh loc ->
let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
new_stack
- ((l_js, t , [],`BranchTag)
- :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
+ ((l_js, t , [],`BranchTag, p)
+ :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s)
| Pos _, _ -> fail (lazy "can't use relative positioning here")
- | Wildcard, ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
+ | Wildcard, ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s
when is_fresh loc ->
new_stack
- (([loc] @+ g', t, [], `BranchTag)
- :: ([], t', k', tag) :: s)
+ (([loc] @+ g', t, [], `BranchTag, p)
+ :: ([], t', k', tag, p') :: s)
| Wildcard, _ -> fail (lazy "can't use wildcard here")
- | Merge, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
- new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
+ | Merge, (g, t, k,`BranchTag,_) :: (g', t', k', tag,p') :: s ->
+ new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag, p') :: s)
| Merge, _ -> fail (lazy "can't merge goals here")
| Focus [], _ -> assert false
| Focus gs, s ->
if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
fail (lazy (sprintf "goal %d not found (or closed)" g)))
gs;
- new_stack ((zero_pos gs, [], [], `FocusTag) :: deep_close gs s)
- | Unfocus, ([], [], [], `FocusTag) :: s -> new_stack s
+ new_stack ((zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s)
+ | Unfocus, ([], [], [], `FocusTag, _) :: s -> new_stack s
| Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open")
in
debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack)));
(** {2 Goal stack} *)
+(* Key value pairs *)
+type parameters = (string * string) list
+
module Stack:
sig
type switch = Open of goal | Closed of goal
type locator = int * switch
type tag = [ `BranchTag | `FocusTag | `NoTag ]
- type entry = locator list * locator list * locator list * tag
+ type entry = locator list * locator list * locator list * tag * parameters
type t = entry list
val empty: t
let s = status#stack in
match s with
| [] -> fail (lazy "There's nothing to prove")
- | (g1, _, k, tag1) :: tl ->
+ | (g1, _, k, tag1, _) :: tl ->
let goals = filter_open g1 in
- let (loc::tl) = goals in
- let goal = goal_of_loc (loc) in
- goal ;;
+ match goals with
+ [] -> fail (lazy "No goals under focus")
+ | loc::tl ->
+ let goal = goal_of_loc (loc) in
+ goal ;;
let extract_conclusion_type status goal =
let gty = get_goalty status goal in
let status,cicterm2 = disambiguate status ctx ty2 `XTNone in
NTacStatus.are_convertible status ctx cicterm1 cicterm2
+let clear_volatile_params_tac status =
+ match status#stack with
+ [] -> fail (lazy "Empty stack")
+ | (g,t,k,tag,p)::tl ->
+ let rec remove_volatile = function
+ [] -> []
+ | (k,v as hd')::tl' ->
+ let re = Str.regexp "volatile_.*" in
+ if Str.string_match re k 0 then
+ remove_volatile tl'
+ else
+ hd'::(remove_volatile tl')
+ in
+ let newp = remove_volatile p in
+ status#set_stack ((g,t,k,tag,newp)::tl)
+;;
+
(* 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. ?
match t2 with
| None ->
let (_,_,t1) = t1 in
- exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
- `JustOne))) (*status*)
+ block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
+ `JustOne))); clear_volatile_params_tac] 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*)
+ block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
+ `JustOne))); clear_volatile_params_tac] status
else
raise NotEquivalentTypes
else
raise FirstTypeWrong
| _ -> raise NotAProduct
-let assume name ty eqty =
- 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 assume name ty eqty status =
+ let goal = extract_first_goal_from_status status in
+ 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 suppose t1 id t2 =
- 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 suppose t1 id t2 status =
+ let goal = extract_first_goal_from_status status in
+ 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 assert_tac t1 t2 status goal continuation =
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
+let branch_dot_tac status =
+ match status#stack with
+ ([],t,k,tag,p) :: tl ->
+ if List.length t > 0 then
+ status#set_stack (([List.hd t],List.tl t,k,tag,p)::tl)
else
- false
+ status
+ | _ -> status
+;;
+
+let status_parameter key status =
+ match status#stack with
+ [] -> ""
+ | (g,t,k,tag,p)::_ -> try List.assoc key p with _ -> ""
+;;
+
+let beta_rewriting_step t status =
+ let ctx = status_parameter "volatile_context" status in
+ if ctx <> "beta_rewrite" then fail (lazy "Invalid use of 'or equivalently'")
+ else
+ change_tac ~where:("",0,(None,[],Some
+ Ast.UserInput)) ~with_what:t status
+;;
+
+let done_continuation status =
+ let rec continuation l =
+ match l with
+ [] -> []
+ | (_,t,_,tag,p)::tl ->
+ if tag = `BranchTag then
+ if List.length t > 0 then
+ let continue =
+ let ctx =
+ try List.assoc "context" p
+ with Not_found -> ""
+ in
+ ctx <> "induction" && ctx <> "cases"
+ in
+ if continue then [clear_volatile_params_tac;branch_dot_tac] else
+ [clear_volatile_params_tac]
+ else
+ [merge_tac] @ (continuation tl)
+ else
+ []
+ in
+ continuation status#stack
+;;
let bydone just status =
let goal = extract_first_goal_from_status status in
- let mustdot = mustdot status in
- let l = [mk_just status goal just] in
- let l =
- if mustdot then List.append l [dot_tac] else l
- in
+ let continuation = done_continuation status in
+ let l = [mk_just status goal just] @ continuation in
block_tac l status
;;
+let push_goals_tac status =
+ match status#stack with
+ [] -> fail (lazy "Error pushing goals")
+ | (g1,t1,k1,tag1,p1) :: (g2,t2,k2,tag2,p2) :: tl ->
+ if List.length g2 > 0 then
+ status#set_stack ((g1,t1 @+ g2,k1,tag1,p1) :: ([],t2,k2,tag2,p2) :: tl)
+ else status (* Nothing to push *)
+ | _ -> status
+
+let add_parameter_tac key value status =
+ match status#stack with
+ [] -> status
+ | (g,t,k,tag,p) :: tl -> status#set_stack ((g,t,k,tag,(key,value)::p)::tl)
+;;
+
let we_need_to_prove t id t1 status =
let goal = extract_first_goal_from_status status in
match id with
match t1 with
| None -> (* We need to prove t *)
(
- try assert_tac t None status goal (id_tac status)
+ try assert_tac t None status goal (add_parameter_tac "volatile_context" "beta_rewrite" 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)
+ try assert_tac t (Some t1) status goal (block_tac [change_tac ~where:("",0,(None,[],Some
+ Ast.UserInput))
+ ~with_what:t1;
+ add_parameter_tac "volatile_context"
+ "beta_rewrite"] status)
with
| FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
| NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
(
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
+ | None -> block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac;
+ push_goals_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
+ | Some t1 -> block_tac [clear_volatile_params_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
+ branch_tac; push_goals_tac
]
status
)
| Some id ->
(
match ty' with
- | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac ] status
+ | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac;
+ clear_volatile_params_tac ] status
| Some ty' -> 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
+ merge_tac; clear_volatile_params_tac] status
)
;;
-let existselim just id1 t1 t2 id2 =
- distribute_tac (fun status goal ->
- let (_,_,t1) = t1 in
- let (_,_,t2) = t2 in
- 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 existselim just id1 t1 t2 id2 status =
+ let goal = extract_first_goal_from_status status in
+ let (_,_,t1) = t1 in
+ let (_,_,t2) = t2 in
+ let just = mk_just status goal 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;
+ clear_volatile_params_tac
+ ]) status
;;
-let andelim just t1 id1 t2 id2 =
- distribute_tac (fun status goal ->
- let (_,_,t1) = t1 in
- let (_,_,t2) = t2 in
- 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 andelim just t1 id1 t2 id2 status =
+ let goal = extract_first_goal_from_status status in
+ let (_,_,t1) = t1 in
+ let (_,_,t2) = t2 in
+ let just = mk_just status goal 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;
+ clear_volatile_params_tac
+ ]) status
;;
let type_of_tactic_term status ctx t =
let gstatus =
match status#stack with
| [] -> assert false
- | (g,t,k,tag) :: s ->
+ | (g,t,k,tag,p) :: s ->
match g with
| (loc1) :: (loc2) :: tl ->
- ([loc2;loc1] @+ tl,t,k,tag) :: s
+ ([loc2;loc1] @+ tl,t,k,tag,p) :: s
| _ -> assert false
in
status#set_stack gstatus
-let thesisbecomes t1 t2 = we_need_to_prove t1 None t2
+let thesisbecomes t1 l = we_need_to_prove t1 None l
;;
let obtain id t1 status =
block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
`JustOne]));
swap_first_two_goals_tac;
- branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; dot_tac;
+ branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; branch_tac; push_goals_tac;
+ add_parameter_tac "volatile_context" "rewrite"
]
status
;;
-let conclude t1 =
- distribute_tac (fun status goal ->
- let cicgty = get_goalty status goal in
- let ctx = ctx_of cicgty in
- let _,gty = term_of_cic_term status cicgty ctx in
- match gty with
- NCic.Appl [_;_;plhs;_] ->
- if alpha_eq_tacterm_kerterm t1 plhs status goal then
- exec id_tac status goal
- else
- fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
- | _ -> fail (lazy "Your conclusion needs to be an equality")
- )
-;;
-
-let rewritingstep rhs just last_step status =
+let conclude t1 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.mem_assoc "timeout" params) then
- ("timeout","3")::params
- else params
+ match gty with
+ NCic.Appl [_;_;plhs;_] ->
+ if alpha_eq_tacterm_kerterm t1 plhs status goal then
+ add_parameter_tac "volatile_context" "rewrite" status
+ else
+ fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
+ | _ -> fail (lazy "Your conclusion needs to be an equality")
+;;
+
+let rewritingstep rhs just last_step status =
+ let ctx = status_parameter "volatile_context" status in
+ if ctx = "rewrite" then
+ (
+ 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.mem_assoc "timeout" params) then
+ ("timeout","3")::params
+ else params
+ in
+ let params' =
+ if not (List.mem_assoc "paramodulation" params) then
+ ("paramodulation","1")::params
+ 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 params' =
- if not (List.mem_assoc "paramodulation" params) then
- ("paramodulation","1")::params
- else params
+ let plhs,prhs,prepare =
+ match gty with (* Extracting the lhs and rhs of the previous equality *)
+ NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
+ | _ -> fail (lazy "You are not building an equaility chain")
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 =
- match gty with (* Extracting the lhs and rhs of the previous equality *)
- NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
- | _ -> fail (lazy "You are not building an equaility chain")
- in
- let continuation =
- if last_step then
- (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
- let todo = [just'] in
- let todo = if mustdot status then List.append todo [dot_tac] else todo
+ let continuation =
+ if last_step then
+ (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
+ let todo = [just'] @ (done_continuation status) 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
- 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
+ prepare continuation
+ )
+ else
+ fail (lazy "You are not building an equality chain")
;;
let rec pp_metasenv_names (metasenv:NCic.metasenv) =
let (_,_,metasenv,_,_) = status#obj in
prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status
+(* Useful as it does not change the order in the list *)
+let rec list_change_assoc k v = function
+ [] -> []
+ | (k',v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl)
+;;
+
let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =
- let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
- let rec remove_name_from_metaattrs mattrs =
- match mattrs with
- [] -> []
- | hd :: tl ->
- match hd with
- `Name n -> remove_name_from_metaattrs tl
- | _ as it -> it :: (remove_name_from_metaattrs tl)
+ let add_name_to_goal name goal metasenv =
+ let (mattrs,ctx,t as conj) = try List.assoc goal metasenv with _ -> assert false in
+ let mattrs = (`Name name) :: (List.filter (function `Name _ -> false | _ -> true) mattrs) in
+ let newconj = (mattrs,ctx,t) in
+ list_change_assoc goal newconj metasenv
+ in
+ let new_goals =
+ (* It's important that this tactic is called before branching and right after the creation of
+ * the new goals, when they are still under focus *)
+ match status#stack with
+ [] -> fail (lazy "Can not add names to an empty stack")
+ | (g,_,_,_,_) :: tl ->
+ let rec sublist n = function
+ [] -> []
+ | hd :: tl -> if n = 0 then [] else hd :: (sublist (n-1) tl)
+ in
+ List.map (fun _,sw -> goal_of_switch sw) (sublist (List.length !cl) g)
+ in
+ let rec add_names_to_goals g cl metasenv =
+ match g,cl with
+ [],[] -> metasenv
+ | hd::tl, (_,consname,_)::tl' ->
+ add_names_to_goals tl tl' (add_name_to_goal consname hd metasenv)
+ | _,_ -> fail (lazy "There are less goals than constructors")
in
+ let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+ let newmetasenv = add_names_to_goals new_goals !cl metasenv
+ in status#set_obj(olduri,oldint,newmetasenv,oldsubst,oldkind)
+;;
+(*
+ let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+ let remove_name_from_metaattrs =
+ List.filter (function `Name _ -> false | _ -> true) in
let rec add_names_to_metasenv cl metasenv =
- match cl with
- [] -> metasenv
- | hd :: tl ->
- let _,consname,_ = hd
- in match metasenv with
- [] -> []
- | mhd :: mtl ->
+ match cl,metasenv with
+ [],_ -> metasenv
+ | hd :: tl, mhd :: mtl ->
+ let _,consname,_ = hd in
let gnum,conj = mhd in
let mattrs,ctx,t = conj in
let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs)
let newconj = mattrs,ctx,t in
let newmeta = gnum,newconj in
newmeta :: (add_names_to_metasenv tl mtl)
+ | _,[] -> assert false
in
let newmetasenv = add_names_to_metasenv !cl metasenv in
status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind)
+*)
+
+let unfocus_branch_tac status =
+ match status#stack with
+ [] -> status
+ | (g,t,k,tag,p) :: tl -> status#set_stack (([],g @+ t,k,tag,p)::tl)
+;;
let we_proceed_by_induction_on t1 t2 status =
let goal = extract_first_goal_from_status status in
(match !sort with NCic.Sort x -> x | _ -> assert false))
in
let eliminator =
- let l = [Ast.Ident (name,None); Ast.Implicit `JustOne] in
- (* Generating as many implicits as open goals *)
- let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) ity.consno in
+ let l = [Ast.Ident (name,None)] in
+ (* Generating an implicit for each argument of the inductive type, plus one the
+ * predicate, plus an implicit for each constructor of the inductive type *)
+ let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) (ity.leftno+1+ity.consno) in
let _,_,t1 = t1 in
let l = l @ [t1] in
Ast.Appl l
in
cl := ity.cl;
exact_tac ("",0,eliminator) status);
- add_names_to_goals_tac cl; dot_tac] status)
+ add_names_to_goals_tac cl;
+ branch_tac;
+ push_goals_tac;
+ unfocus_branch_tac;
+ add_parameter_tac "context" "induction"
+ ] status)
with
| FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
;;
analyze_indty_tac ~what:npt1 indtyinfo;
cases_tac ~what:t1 ~where:("",0,(None,[],Some
Ast.UserInput));
- print_goals_names_tac "Pre Adding";
(
fun status ->
let ity = HExtlib.unopt !indtyinfo in
cl := ity.cl; add_names_to_goals_tac cl status
);
- print_goals_names_tac "Post Adding";
- dot_tac] status)
+ branch_tac; push_goals_tac;
+ unfocus_branch_tac;
+ add_parameter_tac "context" "cases"
+ ] status)
with
| FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
;;
else loc_of_goal goal tl
;;
+let has_focused_goal status =
+ match status#stack with
+ [] -> false
+ | ([],_,_,_,_) :: tl -> false
+ | _ -> true
+;;
+
let focus_on_case_tac case status =
- let goal = extract_first_goal_from_status status in
let (_,_,metasenv,_,_) = status#obj in
let rec goal_of_case case metasenv =
match metasenv with
let gstatus =
match status#stack with
[] -> fail (lazy "There is nothing to prove")
- | (g,t,k,tag) :: s ->
- let loc = loc_of_goal goal_to_focus k in
- let curloc = loc_of_goal goal g in
- (((g @- [curloc]) @+ [loc]),t,([curloc] @+ (k @- [loc])),tag) :: s
- in status#set_stack gstatus
+ | (g,t,k,tag,p) :: s ->
+ let loc =
+ try
+ loc_of_goal goal_to_focus t
+ with _ -> fail (lazy "The given case is not part of the current induction/cases analysis
+ context")
+ in
+ let curloc = if has_focused_goal status then
+ let goal = extract_first_goal_from_status status in
+ [loc_of_goal goal g]
+ else []
+ in
+ (((g @- curloc) @+ [loc]),(curloc @+ (t @- [loc])),k,tag,p) :: s
+ in
+ status#set_stack gstatus
+;;
let case id l status =
- let goal = extract_first_goal_from_status status in
- let (_,_,metasenv,_,_) = status#obj in
- let conj = NCicUtils.lookup_meta goal metasenv in
- let name = name_of_conj conj in
- let continuation =
- let rec aux l =
- match l with
- [] -> [id_tac]
- | (id,ty)::tl ->
- (try_tac (assume id ("",0,ty) None)) :: (aux tl)
- in
- aux l
- in
- if name = id then block_tac continuation status
- else block_tac ([focus_on_case_tac id] @ continuation) status
+ let ctx = status_parameter "context" status in
+ if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an
+ induction/cases analysis context")
+else
+ (
+ if has_focused_goal status then fail (lazy "Finish the current case before switching")
+ else
+ (
+(*
+ let goal = extract_first_goal_from_status status in
+ let (_,_,metasenv,_,_) = status#obj in
+ let conj = NCicUtils.lookup_meta goal metasenv in
+ let name = name_of_conj conj in
+*)
+ let continuation =
+ let rec aux l =
+ match l with
+ [] -> [id_tac]
+ | (id,ty)::tl ->
+ (try_tac (assume id ("",0,ty) None)) :: (aux tl)
+ in
+ aux l
+ in
+(* if name = id then block_tac continuation status *)
+(* else *)
+ block_tac ([focus_on_case_tac id] @ continuation) status
+ )
+ )
;;
let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;
val assume : string -> NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
val suppose : NTacStatus.tactic_term -> string -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
val we_need_to_prove : NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
+val beta_rewriting_step : NTacStatus.tactic_term -> 's NTacStatus.tactic
val bydone : just -> 's NTacStatus.tactic
val by_just_we_proved : just -> NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term
option -> 's NTacStatus.tactic
let gstatus =
match status#stack with
| [] -> assert false
- | ([], _, [], _) :: _ as stack ->
+ | ([], _, [], _, _) :: _ as stack ->
(* backward compatibility: do-nothing-dot *)
stack
- | (g, t, k, tag) :: s ->
+ | (g, t, k, tag, p) :: s ->
match filter_open g, k with
| loc :: loc_tl, _ ->
- (([ loc ], t, loc_tl @+ k, tag) :: s)
+ (([ loc ], t, loc_tl @+ k, tag, p) :: s)
| [], loc :: k ->
assert (is_open loc);
- (([ loc ], t, k, tag) :: s)
+ (([ loc ], t, k, tag, p) :: s)
| _ -> fail (lazy "can't use \".\" here")
in
status#set_stack gstatus
let gstatus =
match status#stack with
| [] -> assert false
- | (g, t, k, tag) :: s ->
+ | (g, t, k, tag, p) :: s ->
match init_pos g with (* TODO *)
| [] -> fail (lazy "empty goals")
| [_] when (not force) -> fail (lazy "too few goals to branch")
| loc :: loc_tl ->
- ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
+ ([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag, p) :: s
in
status#set_stack gstatus
;;
let shift_tac status =
let gstatus =
match status#stack with
- | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
+ | (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s ->
(match g' with
| [] -> fail (lazy "no more goals to shift")
| loc :: loc_tl ->
- (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
- :: (loc_tl, t', k', tag) :: s))
+ (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p)
+ :: (loc_tl, t', k', tag, p') :: s))
| _ -> fail (lazy "can't shift goals here")
in
status#set_stack gstatus
let gstatus =
match status#stack with
| [] -> assert false
- | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+ | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s
when is_fresh loc ->
let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
- ((l_js, t , [],`BranchTag)
- :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
+ ((l_js, t , [],`BranchTag, p)
+ :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s)
| _ -> fail (lazy "can't use relative positioning here")
in
status#set_stack gstatus
let gstatus =
match status#stack with
| [] -> assert false
- | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+ | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s
when is_fresh loc ->
let l_js =
List.filter
match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with
attrs,_,_ when List.mem (`Name lab) attrs -> true
| _ -> false) ([loc] @+ g') in
- ((l_js, t , [],`BranchTag)
- :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
+ ((l_js, t , [],`BranchTag, p)
+ :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s)
| _ -> fail (lazy "can't use relative positioning here")
in
status#set_stack gstatus
let gstatus =
match status#stack with
| [] -> assert false
- | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
+ | ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s
when is_fresh loc ->
- (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
+ (([loc] @+ g', t, [], `BranchTag, p) :: ([], t', k', tag, p') :: s)
| _ -> fail (lazy "can't use wildcard here")
in
status#set_stack gstatus
let gstatus =
match status#stack with
| [] -> assert false
- | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
- ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
+ | (g, t, k,`BranchTag, _) :: (g', t', k', tag, p) :: s ->
+ ((t @+ filter_open g @+ g' @+ k, t', k', tag, p) :: s)
| _ -> fail (lazy "can't merge goals here")
in
status#set_stack gstatus
if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
fail (lazy (sprintf "goal %d not found (or closed)" g)))
gs;
- (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
+ (zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s
in
status#set_stack gstatus
;;
let gstatus =
match status#stack with
| [] -> assert false
- | (g, [], [], `FocusTag) :: s when filter_open g = [] -> s
+ | (g, [], [], `FocusTag, _) :: s when filter_open g = [] -> s
| _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^
Continuationals.Stack.pp s))
in
let gstatus =
match status#stack with
| [] -> assert false
- | (gl, t, k, tag) :: s ->
+ | (gl, t, k, tag, p) :: s ->
let gl = List.map switch_of_loc gl in
if List.exists (function Open _ -> true | Closed _ -> false) gl then
fail (lazy "cannot skip an open goal")
else
- ([],t,k,tag) :: s
+ ([],t,k,tag,p) :: s
in
status#set_stack gstatus
;;
;;
let exec tac (low_status : #lowtac_status) g =
- let stack = [ [0,Open g], [], [], `NoTag ] in
+ let stack = [ [0,Open g], [], [], `NoTag, [] ] in
let status = change_stack_type low_status stack in
let status = tac status in
(low_status#set_pstatus status)#set_obj status#obj
let distribute_tac tac (status : #tac_status) =
match status#stack with
| [] -> assert false
- | (g, t, k, tag) :: s ->
+ | (g, t, k, tag, p) :: s ->
debug_print (lazy ("context length " ^string_of_int (List.length g)));
let rec aux s go gc =
function
debug_print (lazy ("closed: "
^ String.concat " " (List.map string_of_int gcn)));
let stack =
- (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
+ (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s
in
((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_pstatus sn
;;
let assert_tac seqs status =
match status#stack with
| [] -> assert false
- | (g,_,_,_) :: s ->
+ | (g,_,_,_,_) :: s ->
assert (List.length g = List.length seqs);
(match seqs with
[] -> id_tac
if level = 0 then []
else match gs with
| [] -> assert false
- | (g,_,_,_)::s ->
+ | (g,_,_,_,_)::s ->
let is_open = function
| (_,Continuationals.Stack.Open i) -> Some i
| (_,Continuationals.Stack.Closed _) -> None
cands, diff more_cands cands
;;
+let is_a_needed_uri s d =
+ prerr_endline ("DEBUG: " ^ d ^ ": "^ s);
+ s = "cic:/matita/basics/logic/eq.ind" ||
+ s = "cic:/matita/basics/logic/sym_eq.con" ||
+ s = "cic:/matita/basics/logic/trans_eq.con" ||
+ s = "cic:/matita/basics/logic/eq_f3.con" ||
+ s = "cic:/matita/basics/logic/eq_f2.con" ||
+ s = "cic:/matita/basics/logic/eq_f.con"
+
let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty =
let universe = status#auto_cache in
let _,_,metasenv,subst,_ = status#obj in
in
(* we now compute global candidates *)
let global_cands, smart_global_cands =
- if flags.local_candidates then
- let mapf s =
- let to_ast = function
- | NCic.Const r when true
- (*is_relevant statistics r*) -> Some (Ast.NRef r)
- (* | NCic.Const _ -> None *)
- | _ -> assert false in
- HExtlib.filter_map
- to_ast (NDiscriminationTree.TermSet.elements s) in
- let g,l =
- get_cands
- (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
- NDiscriminationTree.TermSet.diff
- NDiscriminationTree.TermSet.empty
- raw_gty raw_weak_gty in
- mapf g, mapf l
- else [],[] in
+ let mapf s =
+ let to_ast = function
+ | NCic.Const r when true
+ (*is_relevant statistics r*) -> Some (Ast.NRef r)
+ (* | NCic.Const _ -> None *)
+ | _ -> assert false in
+ HExtlib.filter_map
+ to_ast (NDiscriminationTree.TermSet.elements s) in
+ let g,l =
+ get_cands
+ (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
+ NDiscriminationTree.TermSet.diff
+ NDiscriminationTree.TermSet.empty
+ raw_gty raw_weak_gty in
+ mapf g, mapf l
+ in
+ let global_cands,smart_global_cands =
+ if flags.local_candidates then global_cands,smart_global_cands
+ else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
+ (NUri.string_of_uri
+ uri) "GLOBAL" | _ -> false)
+ in filter global_cands,filter smart_global_cands
+ in
(* we now compute local candidates *)
let local_cands,smart_local_cands =
- if flags.local_candidates then
let mapf s =
let to_ast t =
let _status, t = term_of_cic_term status t context
(fun ty -> search_in_th ty cache)
Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
mapf g, mapf l
- else [],[] in
+ in
+ let local_cands,smart_local_cands =
+ if flags.local_candidates then local_cands,smart_local_cands
+ else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
+ (NUri.string_of_uri
+ uri) "LOCAL" | _ -> false)
+ in filter local_cands,filter smart_local_cands
+ in
(* we now splits candidates in facts or not facts *)
let test = is_a_fact_ast status subst metasenv context in
let by,given_candidates =
NCicMetaSubst.mk_meta
metasenv ctx ~with_type:implication `IsType in
let status = status#set_obj (n,h,metasenv,subst,obj) in
- let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
+ let status = status#set_stack [([1,Open j],[],[],`NoTag,[])] in
try
let status = NTactics.intro_tac "foo" status in
let status =
let gstatus =
match status#stack with
| [] -> assert false
- | (goals, t, k, tag) :: s ->
+ | (goals, t, k, tag, p) :: s ->
let g = head_goals status#stack in
let sortedg =
(List.rev (MS.topological_sort g (deps status))) in
let sorted_goals =
List.map (fun i -> List.find (is_it i) goals) sortedg
in
- (sorted_goals, t, k, tag) :: s
+ (sorted_goals, t, k, tag, p) :: s
in
status#set_stack gstatus
;;
let gstatus =
match status#stack with
| [] -> assert false
- | (g, t, k, tag) :: s ->
+ | (g, t, k, tag, p) :: s ->
let is_open = function
| (_,Continuationals.Stack.Open _) -> true
| (_,Continuationals.Stack.Closed _) -> false
in
let g' = List.filter is_open g in
- (g', t, k, tag) :: s
+ (g', t, k, tag, p) :: s
in
status#set_stack gstatus
;;
if level = 0 then [],[],gs else
match gs with
| [] -> assert false
- | (g, t, k, tag) :: s ->
+ | (g, t, k, tag,p) :: s ->
let f,o,gs = slice (level-1) s in
let f1,o1 = List.partition in_focus g
in
- (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
+ (f1,[],[],`BranchTag, [])::f, (o1, t, k, tag, p)::o, gs
in
let gstatus =
let f,o,s = slice level status#stack in f@o@s
let move_to_side level status =
match status#stack with
| [] -> assert false
- | (g,_,_,_)::tl ->
+ | (g,_,_,_,_)::tl ->
let is_open = function
| (_,Continuationals.Stack.Open i) -> Some i
| (_,Continuationals.Stack.Closed _) -> None
let _ = debug_print (pptrace status trace) in
let stack =
match s#stack with
- | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
+ | (g,t,k,f,p) :: rest -> (filter_open g,t,k,f,p):: rest
| _ -> assert false
in
let s = s#set_stack stack in
let gty = get_goalty status goal in
let ctx = ctx_of gty in
let candidates = candidates_from_ctx univ ctx status in
- auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref:(ref [])
+ auto_tac' candidates ~local_candidates:false ~use_given_only:true flags ~trace_ref:(ref [])
let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
let candidates = candidates_from_ctx univ [] status in
<sect1 id="tac_assume">
<title>assume</title>
<titleabbrev>assume</titleabbrev>
- <para><userinput>assume x : t</userinput></para>
+ <para><userinput>assume x : T that is equivalent to T'</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">assume</emphasis> &id; <emphasis role="bold"> : </emphasis> &sterm;</para>
+ <para><emphasis role="bold">assume</emphasis> &id; <emphasis role="bold"> : </emphasis>
+ &sterm; [ <emphasis role="bold">that is equivalent to</emphasis> &term; ]</para>
</listitem>
</varlistentry>
<varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>It adds to the context of the current sequent to prove a new
- declaration <command>x : T </command>. The new conclusion becomes
- <command>P</command>.</para>
+ <para>It adds to the context of the current sequent to prove a new declaration <command>x : T
+ </command>. The new conclusion becomes <command>P</command>. Alternatively, if a type
+ <command>T'</command> is supplied and <command>T</command> and <command>T'</command> are beta equivalent the new declaration that is added to the context is
+ <command>x:T'</command>.</para>
</listitem>
</varlistentry>
<varlistentry>
</para>
</sect1>
- <sect1 id="tac_byinduction">
- <title>by induction hypothesis we know</title>
- <titleabbrev>by induction hypothesis we know</titleabbrev>
- <para><userinput>by induction hypothesis we know t (id)</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem><para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>To be used in a proof by induction to state the inductive
- hypothesis.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para> Introduces the inductive hypothesis. </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
+ <sect1 id="tac_suppose">
+ <title>suppose</title>
+ <titleabbrev>suppose</titleabbrev>
+ <para><userinput>suppose T (x) that is equivalent to T'</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
+ <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis> &term; ]</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>The conclusion of the current proof must be
+ <command>∀x:T.P</command> or
+ <command>T→P</command> where <command>T</command> is
+ a proposition (i.e. <command>T</command> has type
+ <command>Prop</command> or <command>CProp</command>).</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It adds to the context of the current sequent to prove a new declaration <command>x : T
+ </command>. The new conclusion becomes <command>P</command>. Alternatively, if a type
+ <command>T'</command> is supplied and <command>T</command> and <command>T'</command> are beta equivalent the new declaration that is added to the context is
+ <command>x:T'</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
- <sect1 id="tac_case">
- <title>case</title>
- <titleabbrev>case</titleabbrev>
- <para><userinput>case id (id1:t1) … (idn:tn)</userinput></para>
+<sect1 id="tac_let">
+ <title>letin</title>
+ <titleabbrev>letin</titleabbrev>
+ <para><userinput>let x := T </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">let</emphasis> &id; <emphasis role="bold"> = </emphasis> &term;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>None</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It adds a new local definition <command>x := T</command> to the context of the sequent to prove.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+ <sect1 id="tac_bytermweproved">
+ <title>we proved</title>
+ <titleabbrev>we proved</titleabbrev>
+ <para><userinput>justification we proved T (id) that is equivalent to T'</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">)</emphasis>] … </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>To be used in a proof by induction or by cases to start
- a new case</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>Starts the new case <command>id</command> declaring
- the local parameters <command>(id1:t1) … (idn:tn)</command></para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None</para>
+ <para>&justification; <emphasis role="bold">we proved</emphasis> &term;
+ <emphasis role="bold">(</emphasis> &id;
+ <emphasis role="bold">)</emphasis> [ <emphasis role="bold">that is equivalent to</emphasis> &term;] [ <emphasis role="bold">done</emphasis>]</para>
</listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para><command>T</command> must have type <command>Prop</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It derives <command>T</command>
+ using the justification and labels the conclusion with
+ <command>id</command>. Alternatively, if a proposition
+ <command>T'</command> is supplied and <command>T</command> and <command>T'</command> are beta equivalent the new hypothesis that is added to the context is
+ <command>id:T'</command>.
+
+ If the user does not supply a label and ends the command with <command>done</command> then if T is alpha equivalent to the conclusion of the current sequent then it closes it (if <command>T'</command> is supplied this must be alpha equivalent to the conclusion, but in this case <command>T</command> does not need to).
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
<sect1 id="tac_bydone">
<title>done</title>
</para>
</sect1>
-
- <sect1 id="tac_exitselim">
+ <sect1 id="tac_existselim">
<title>let such that</title>
<titleabbrev>let such that</titleabbrev>
<para><userinput>justification let x:t such that p (id)</userinput>
</para>
</sect1>
- <sect1 id="tac_obtain">
- <title>obtain</title>
- <titleabbrev>obtain</titleabbrev>
- <para><userinput>obtain H t1 = t2 justification</userinput></para>
+ <sect1 id="tac_andelim">
+ <title>we have</title>
+ <titleabbrev>we have</titleabbrev>
+ <para><userinput>justification we have t1 (id1) and t2 (id2)</userinput>
+ </para>
<para>
<variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">using once</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para><command>conclude</command> can be used only if the current
- sequent is stating an equality. The left hand side must be omitted
- in an equality chain.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>Starts or continues an equality chain. If the chain starts
- with <command>obtain H</command> a new subproof named
- <command>H</command> is started.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequent to prove:</term>
- <listitem>
- <para>If the chain starts
- with <command>obtain H</command> a nre sequent for
- <command>t2 = ?</command> is opened.
- </para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_suppose">
- <title>suppose</title>
- <titleabbrev>suppose</titleabbrev>
- <para><userinput>suppose t1 (x) that is equivalent to t2</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
- <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis> &term; ]</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>The conclusion of the current proof must be
- <command>∀x:T.P</command> or
- <command>T→P</command> where <command>T</command> is
- a proposition (i.e. <command>T</command> has type
- <command>Prop</command> or <command>CProp</command>).</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
+ <varlistentry role="tactic_synopsis">
+ <term>Synopsis:</term>
<listitem>
- <para>It adds to the context of the current sequent to prove a new
- declaration <command>x : T </command>. The new conclusion becomes
- <command>P</command>.</para>
+ <para>&justification; <emphasis role="bold">we have</emphasis> &term;
+ <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term;
+ <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para></para>
</listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It derives <command>t1∧t2</command> using the
+ <command>justification</command> then it introduces in the context
+ <command>t1</command> labelled with <command>id1</command> and
+ <command>t2</command> labelled with <command>id2</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
- <sect1 id="tac_thesisbecomes">
- <title>the thesis becomes</title>
- <titleabbrev>the thesis becomes</titleabbrev>
- <para><userinput>the thesis becomes t</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>The provided term <command>t</command> must be convertible with
- current sequent.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It changes the current goal to the one provided.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequent to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
<sect1 id="tac_weneedtoprove">
<title>we need to prove</title>
<titleabbrev>we need to prove</titleabbrev>
</para>
</sect1>
-
- <sect1 id="tac_andelim">
- <title>we have</title>
- <titleabbrev>we have</titleabbrev>
- <para><userinput>justification we have t1 (id1) and t2 (id2)</userinput>
- </para>
+ <sect1 id="tac_weproceedbyinduction">
+ <title>we proceed by induction on</title>
+ <titleabbrev>we proceed by induction on</titleabbrev>
+ <para><userinput>we proceed by induction on t to prove th</userinput></para>
<para>
<variablelist>
- <varlistentry role="tactic_synopsis">
+ <varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para>&justification; <emphasis role="bold">we have</emphasis> &term;
- <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term;
- <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
- </listitem>
+ <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
+ </listitem>
</varlistentry>
- <varlistentry>
+ <varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para></para>
+ <para><command>t</command> must inhabitant of an inductive type and
+ <command>th</command> must be the conclusion to be proved by induction.
+ </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
- <listitem>
- <para>It derives <command>t1∧t2</command> using the
- <command>justification</command> then it introduces in the context
- <command>t1</command> labelled with <command>id1</command> and
- <command>t2</command> labelled with <command>id2</command>.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequent to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
+ <listitem>
+ <para>It proceed by induction on <command>t</command>.</para>
+ </listitem>
</varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens one new sequent for each constructor of the
+ type of <command>t</command>.</para>
+ </listitem>
+ </varlistentry>
</variablelist>
</para>
</sect1>
</variablelist>
</para>
</sect1>
-
- <sect1 id="tac_weproceedbyinduction">
- <title>we proceed by induction on</title>
- <titleabbrev>we proceed by induction on</titleabbrev>
- <para><userinput>we proceed by induction on t to prove th</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para><command>t</command> must inhabitant of an inductive type and
- <command>th</command> must be the conclusion to be proved by induction.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It proceed by induction on <command>t</command>.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>It opens one new sequent for each constructor of the
- type of <command>t</command>.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_bytermweproved">
- <title>we proved</title>
- <titleabbrev>we proved</titleabbrev>
- <para><userinput>justification we proved t (id)</userinput></para>
+ <sect1 id="tac_case">
+ <title>case</title>
+ <titleabbrev>case</titleabbrev>
+ <para><userinput>case id (id1:t1) … (idn:tn)</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para>&justification; <emphasis role="bold">we proved</emphasis> &term;
- <emphasis role="bold">(</emphasis> &id;
- <emphasis role="bold">)</emphasis></para>
+ <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">)</emphasis>] … </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>To be used in a proof by induction or by cases to start
+ a new case</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Starts the new case <command>id</command> declaring
+ the local parameters <command>(id1:t1) … (idn:tn)</command></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None</para>
</listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+ <sect1 id="tac_byinduction">
+ <title>by induction hypothesis we know</title>
+ <titleabbrev>by induction hypothesis we know</titleabbrev>
+ <para><userinput>by induction hypothesis we know t (id)</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem><para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>To be used in a proof by induction to state the inductive
+ hypothesis.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para> Introduces the inductive hypothesis. </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+ <sect1 id="tac_thesisbecomes">
+ <title>the thesis becomes</title>
+ <titleabbrev>the thesis becomes</titleabbrev>
+ <para><userinput>the thesis becomes t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
+ </listitem>
</varlistentry>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para><command>t</command>must have type <command>Prop</command>.
- </para>
+ <para>The provided term <command>t</command> must be convertible with
+ current sequent.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>It derives <command>t</command>
- using the justification and labels the conclusion with
- <command>id</command>.
- </para>
+ <para>It changes the current goal to the one provided.</para>
</listitem>
</varlistentry>
<varlistentry>
</varlistentry>
</variablelist>
</para>
- </sect1>
+ </sect1>
+ <sect1 id="tac_obtain">
+ <title>conclude/obtain</title>
+ <titleabbrev>conclude/obtain</titleabbrev>
+ <para><userinput>conclude/obtain (H) t1 = t2 justification</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">using once</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para><command>conclude</command> can be used only if the current
+ sequent is stating an equality. The left hand side must be omitted
+ in an equality chain.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Starts or continues an equality chain. If the chain starts
+ with <command>obtain H</command> a new subproof named
+ <command>H</command> is started.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>If the chain starts
+ with <command>obtain H</command> a nre sequent for
+ <command>t2 = ?</command> is opened.
+ </para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+
+
+
+
+
+
</chapter>
projects / helm.git / commitdiff