module FStar.Tactics.Derived

fsdoc: no-summary-found

fsdoc: no-comment-found

let ((_cur_goal ()):(Tac goal)):match goals () with []  -> fail "no more goals" | (Prims.Cons g _)  -> g

Return the current goal, not its type. (Ignores SMT goals)

let ((cur_env ()):(Tac env)):goal_env (_cur_goal ())

[cur_env] returns the current goal's environment

let ((cur_goal ()):(Tac typ)):goal_type (_cur_goal ())

[cur_goal] returns the current goal's type

let ((cur_witness ()):(Tac term)):goal_witness (_cur_goal ())

[cur_witness] returns the current goal's witness

let ((cur_goal_safe ()):(TacH goal ((requires ((fun ps -> ~((==(goals_of ps, (Prims.Nil )))))))) ((ensures ((fun ps0 r -> exists g.{:pattern } ==(r, (Success g ps0)))))))):match goals_of (get ()) with (Prims.Cons g _)  -> g

[cur_goal_safe] will always return the current goal, without failing. It must be statically verified that there indeed is a goal in order to call it.

let ((cur_binders ()):(Tac binders)):binders_of_env (cur_env ())

[cur_binders] returns the list of binders in the current goal.

let ((with_policy pol (f:Unidentified product: [unit] (Tac 'a))):(Tac 'a)):let  old_pol = get_guard_policy () in set_guard_policy pol; let  r = f () in set_guard_policy old_pol; r

Set the guard policy only locally, without affecting calling code

let ((dismiss ()):(Tac unit)):match goals () with []  -> fail "dismiss: no more goals" | (Prims.Cons _ gs)  -> set_goals gs

Ignore the current goal. If left unproven, this will fail after the tactic finishes.

let ((flip ()):(Tac unit)):let  gs = goals () in match goals () with []|
 [_]  -> fail "flip: less than two goals" | (Prims.Cons g1 (Prims.Cons g2 gs))  -> set_goals ((Prims.Cons g2 (Prims.Cons g1 gs)))

Flip the order of the first two goals.

let ((qed ()):(Tac unit)):match goals () with []  -> () | _  -> fail "qed: not done!"

Succeed if there are no more goals left, and fail otherwise.

let ((debug (m:string)):(Tac unit)):if debugging () then print m else ()

[debug str] is similar to [print str], but will only print the message if the [--debug] option was given for the current module AND [--debug_level Tac] is on.

let ((smt ()):(Tac unit)):match (FStar.Pervasives.Native.Mktuple2 goals () smt_goals ()) with ([], _)  -> fail "smt: no active goals" | ((Prims.Cons g gs), gs')  -> set_goals gs; set_smt_goals ((Prims.Cons g gs'))

[smt] will mark the current goal for being solved through the SMT. This does not immediately run the SMT: it just dumps the goal in the SMT bin. Note, if you dump a proof-relevant goal there, the engine will later raise an error.

let ((later ()):(Tac unit)):match goals () with (Prims.Cons g gs)  -> set_goals (@(gs, (Prims.Cons g (Prims.Nil )))) | _  -> fail "later: no goals"

Push the current goal to the back.

let ((exact (t:term)):(Tac unit)):with_policy SMT ((fun () -> t_exact true false t))

[exact e] will solve a goal [Gamma |- w : t] if [e] has type exactly [t] in [Gamma].

let ((exact_with_ref (t:term)):(Tac unit)):with_policy SMT ((fun () -> t_exact true true t))

[exact_with_ref e] will solve a goal [Gamma |- w : t] if [e] has type [t'] where [t'] is a subtype of [t] in [Gamma]. This is a more flexible variant of [exact].

let ((apply (t:term)):(Tac unit)):t_apply true false t

[apply f] will attempt to produce a solution to the goal by an application of [f] to any amount of arguments (which need to be solved as further goals). The amount of arguments introduced is the least such that [f a_i] unifies with the goal's type.

let ((apply_raw (t:term)):(Tac unit)):t_apply false false t

[apply_raw f] is like [apply], but will ask for all arguments regardless of whether they appear free in further goals. See the explanation in [t_apply].

let ((exact_guard (t:term)):(Tac unit)):with_policy Goal ((fun () -> t_exact true false t))

Like [exact], but allows for the term [e] to have a type [t] only under some guard [g], adding the guard as a goal.

let ((divide (n:int) (l:Unidentified product: [unit] (Tac 'a)) (r:Unidentified product: [unit] (Tac 'b))):(Tac (*('a, 'b)))):if <(n, 0) then fail "divide: negative n" else (); let  (gs, sgs) = (FStar.Pervasives.Native.Mktuple2 goals () smt_goals ()) in let  (gs1, gs2) = List.Tot.splitAt n gs in set_goals gs1; set_smt_goals (Prims.Nil ); let  x = l () in let  (gsl, sgsl) = (FStar.Pervasives.Native.Mktuple2 goals () smt_goals ()) in set_goals gs2; set_smt_goals (Prims.Nil ); let  y = r () in let  (gsr, sgsr) = (FStar.Pervasives.Native.Mktuple2 goals () smt_goals ()) in set_goals (@(gsl, gsr)); set_smt_goals (@(sgs, @(sgsl, sgsr))); ((FStar.Pervasives.Native.Mktuple2 x y))

[divide n t1 t2] will split the current set of goals into the [n] first ones, and the rest. It then runs [t1] on the first set, and [t2] on the second, returning both results (and concatenating remaining goals).

let ((focus (t:Unidentified product: [unit] (Tac 'a))):(Tac 'a)):match goals () with []  -> fail "focus: no goals" | (Prims.Cons g gs)  -> let  sgs = smt_goals () in set_goals (Prims.Cons g (Prims.Nil )); set_smt_goals (Prims.Nil ); let  x = t () in set_goals (@(goals (), gs)); set_smt_goals (@(smt_goals (), sgs)); x

[focus t] runs [t ()] on the current active goal, hiding all others and restoring them at the end.

let (dump1 (m:string)):focus ((fun () -> dump m))

Similar to [dump], but only dumping the current goal.

let ((seq (f:Unidentified product: [unit] (Tac unit)) (g:Unidentified product: [unit] (Tac unit))):(Tac unit)):focus ((fun () -> f (); iterAll g))

Runs tactic [t1] on the current goal, and then tactic [t2] on each subgoal produced by [t1]. Each invocation of [t2] runs on a proofstate with a single goal (they're "focused").

let ((ngoals ()):(Tac int)):List.length (goals ())

[ngoals ()] returns the number of goals

let ((ngoals_smt ()):(Tac int)):List.length (smt_goals ())

[ngoals_smt ()] returns the number of SMT goals

let (join_all_smt_goals ()):let  (gs, sgs) = (FStar.Pervasives.Native.Mktuple2 goals () smt_goals ()) in set_smt_goals (Prims.Nil ); set_goals sgs; repeat' join; let  sgs' = goals () in set_goals gs; set_smt_goals sgs'

Join all of the SMT goals into one. This helps when all of them are expected to be similar, and therefore easier to prove at once by the SMT solver. TODO: would be nice to try to join them in a more meaningful way, as the order can matter.

let ((is_guard ()):(Tac bool)):Tactics.Types.is_guard (_cur_goal ())

[is_guard] returns whether the current goal arised from a typechecking guard

let ((rewrite' (b:binder)):(Tac unit)):(<|>(<|>(((fun () -> rewrite b)), ((fun () -> binder_retype b; apply_lemma ((`(__eq_sym))); rewrite b))), ((fun () -> fail "rewrite' failed")))) ()

Like [rewrite], but works with equalities [v == e] and [e == v]

let ((l_to_r (lems:list term)):(Tac unit)):let  ((first_or_trefl ()):(Tac unit)) = fold_left ((fun k l () -> or_else ((fun () -> apply_lemma l)) k)) trefl lems () in pointwise first_or_trefl

Rewrites left-to-right, and bottom-up, given a set of lemmas stating equalities. The lemmas need to prove propositional equalities, that is, using [==].

let ((grewrite_eq (b:binder)):(Tac unit)):match term_as_formula (type_of_binder b) with (Comp (Eq _) l r)  -> grewrite l r; iseq (Prims.Cons idtac (Prims.Cons ((fun () -> exact (binder_to_term b))) (Prims.Nil ))) | _  -> fail "failed in grewrite_eq"

A wrapper to [grewrite] which takes a binder of an equality type

let ((branch_on_match ()):(Tac unit)):focus ((fun () -> let  x = get_match_body () in let  _ = t_destruct x in iterAll ((fun () -> let  bs = repeat intro in let  b = last bs in grewrite_eq b; norm (Prims.Cons iota (Prims.Nil ))))))

When the goal is [match e with | p1 -> e1 ... | pn -> en], destruct it into [n] goals for each possible case, including an hypothesis for [e] matching the correposnding pattern.