Library CFML.CFTactics

cfml_find_hprop_at X returns the hprop X ~> T that appears in the pre-condition.

Auxiliary tactic for obtaining a boolean answer to the question "is E an evar?". TODO: move to TLC

cfml_postcondition_is_evar tt returns a boolean indicating whether the post-condition of the current goal is an evar.

xcur is a convenient way to obtain the current precondition. Syntax is: let H := xcur in .... Example: let H := xcur in xif (\[= 3] \*+ H) .

xclean is a tactic that performs some clean up throughout the goal by taking care of:

• rewriting facts such as true = isTrue P into P
• simplifying partially applied equality, e.g. (= 3) n to n = 3.

See reflect_clean tt from the Shared.v file. Remark: this tactic is automatically called by xpull.

xauto is a specialized version of auto that works well in program verification.

• it will not attempt any work if the head of the goal has a tag (i.e. if it is a characteristif formula),
• it is able to conclude a goal using xok
• it calls substs to substitute all equalities before trying to call automation.

Tactics xauto, xauto~ and xauto* can be configured independently. xsimpl~ is equivalent to xsimpl; xauto~. xsimpl* is equivalent to xsimpl; xauto*.

DEPRECATED Extensions for hsimpl to use xauto Tactic Notation "hsimpl" "~" constr(L) := hsimpl L; xauto~. Tactic Notation "hsimpl" "~" constr(X1) constr(X2) := hsimpl X1 X2; xauto~. Tactic Notation "hsimpl" "~" constr(X1) constr(X2) constr(X3) := hsimpl X1 X2 X3; xauto~.

xok proves a goal of the form H ==> ?H' or Q ===> ?Q' by unifying the right-hand-side with the left-hand-side. It also tries to call hsimpl to see if it solves the goal. TODO: is this last feature of xok useful?

xsimpl performs a heap entailement simplification using hsimpl, then calls the tactic xclean for clean up.

xlocal proves a goal of the form is_local F or is_local_pred F, by exploiting the fact that

• F may be of the form local F'
• is_local F may be an assumption
• is_local_pred S may be an assumption, with F = S x

xpre applies to a goal of the form F H Q and allows to strengthen the pre-condition H. It produces F ?H' Q and H ==> ?H' \* \GC, where Hexists HG, HG can be instantiated with garbage to collect.

xpost applies to a goal of the form F H Q and allows to weaken the pre-condition Q. It produces F H ?Q' and ?Q' ==> ?Q \* \GC. xpost Q' applies to a goal of the form F H Q and leaves the goals F H Q' and Q' ===> Q. xpost H' is a shorthand for xpost (#H').

xpull_check_not_needed tt applies to a goal of the form F H Q and raises an error if H contains existentials or pure propositions that could have been extracted using xpull

Auxiliary definitions for xpull.

xpull extracts existentials and pure propositions from the precondition H of a goal of the form F H Q, or from the left-hand-side H of a goal of the form H ==> H' or H ===> H'. It calls xclean which is useful for cleaning up

xpulls calls xpull, assumes that this call produces an equality at the head of the goal, and it then substitutes this equality away.

DEPRECATED xpull as I1 .. IN should now be written xpull. => I1 .. IN Tactic Notation "xpull" "as" simple_intropattern(I1) := xpull; intros I1; xclean. Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) := xpull; intros I1 I2; xclean. Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) simple_intropattern(I3) := xpull; intros I1 I2 I3; xclean. Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) := xpull; intros I1 I2 I3 I4; xclean. Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) := xpull; intros I1 I2 I3 I4 I5; xclean. Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) simple_intropattern(I6) := xpull; intros I1 I2 I3 I4 I5 I6; xclean. Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) simple_intropattern(I6) simple_intropattern(I7) := xpull; intros I1 I2 I3 I4 I5 I6 I7; xclean. Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) := xpull; intros I1 I2 I3 I4 I5 I6 I7 I8; xclean. Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) simple_intropattern(I9) := xpull; intros I1 I2 I3 I4 I5 I6 I7 I8 I9; xclean. Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) simple_intropattern(I9) simple_intropattern(I10) := xpull; intros I1 I2 I3 I4 I5 I6 I7 I8 I9 I10; xclean.

xgc H' applies to a goal of the form F H Q and substracts H' from H. xgc_but H' substracts everything but H' from H. xgc_all substracts everything from H, leaving F \[] Q. It is equivalent to xgc_but \[]. xgc_post applied to the goal F H Q replaces the goal with F H ?Q' and Q' ===> Q \*+ \GC, which allows to perform garbage collection. xgc x is same as xgc (x ~> T) where T is read in the pre-condition. TODO: xgc with several arguments, or a list of arguments.

xframe H' applies to a goal of the form F H Q and substracts H' from both H and Q. xframe_but H' substracts everything but H'.

xframe_on p applies to a goal of the form F H Q and calls xframe (p ~> M), where M is guessed from the occurence of p ~> M that can be found in the pre-condition H. Variants: xframe_on p1 p2 and xframe_on p1 p2 p3.

xapply E applies a lemma E modulo frame/weakening. It applies to a goal of the form F H Q, and replaces it with F ?H' ?Q', applies E to the goal, then produces the side condition H ==> ?H' and,

• if Q is instantiated, then leaves ?Q' ===> Q \* \GC
• otherwise instantiates Q with Q'.

xapplys E is like xapply E but also attemps to simplify the subgoals.

xchange E applies to a goal of the form F H Q and to a lemma E of type H1 ==> H2 or H1 = H2. It replaces the goal with F H' Q, where H' is computed by replacing H1 with H2 in H. The substraction is computed by solving H ==> H1 \* ?H' with hsimpl. If you need to solve this implication by hand, use xchange_no_simpl E instead. xchange <- E is useful when E has type H2 = H1 instead of H1 = H2. xchange_show E is useful to visualize the instantiation of the lemma used to implement xchange.

xopen is a tactic for applying xchange without having to explicitly specify the name of a focusing lemma. xopen p applies to a goal of the form F H Q or H ==> H' or Q ===> Q'. It first searches for the pattern p ~> T in the pre-condition, then looks up in a database for the focus lemma E associated with the form T, and then calls xchange E. xopen_show p shows the lemma found, it is useful for debugging. Example for registering a focusing lemma: Hint Extern 1 (RegisterOpen (Tree _)) => Provide tree_open. See Demo_proof.v for examples. Then, use: xopen p. Variants:

• xopenx t is short for xopen t; xpull
• xopenxs t is short for xopen t; xpulls // EXPERIMENTAL
• xopen2 p to perform xopen p twice. Only applies when there is no existentials to be extracted after the first xopen.

xclose is the symmetrical of xopen. It works in the same way, except that it looks for an unfocusing lemma. xclose p applies to a goal of the form F H Q or H ==> H' or Q ===> Q'. It first searches for the pattern p ~> T in the pre-condition, then looks up in a database for the unfocus lemma E associated with the form T, and then calls xchange E. xclose_show p shows the lemma found, it is useful for debugging. Example for registering a focusing lemma: Hint Extern 1 (RegisterClose (Ref Id (MNode _ ))) => Provide tree_node_close. Then, use: xclose p. Variants:

• xclose p1 .. pn is short for xclose p1; ..; xclose pn
• xclose2 p to perform xclose p twice.
• xclose (>> p X Y) where the extra arguments are used to provide explicit arguments to instantiate the "closing" lemma.

xgen E applies to a goal of the form H ==> H', where H contains occurences of E in the sense H = J E, and it abstract E from H, turning the goal into (Hexists X, J X) ==> H'.

xlet is used to reason on a let node, i.e. on a goal of the form (Let x := F1 in F2) H Q. Use xlet Q to provide a postcondition for F1. Use xlet as y to rename x into y. Use xlet Q as y to do both.

DEPRECATED xlets Tactic Notation "xlets" constr(Q) := xlet Q; | intro_subst .

xlet_poly is used to reason on a let node, i.e. on a goal of the form (LetPoly {A1} x := F1 in F2) H Q. Variants:

• xlet_poly P H to describe the pure postcondition and the final state.
• xlet_poly_keep P to provide a pure postcondition and use the current pre-condition as final state.
• xlet_poly P to provide a pure postcondition and introduce a unification variable for the imperative state.
• xlet_poly as y to rename x into y.
• xlet_poly P H as y.

xseq is used to reason on a seq node, i.e. on a goal of the form (F1 ;; F2) H Q. Use xseq H' to provide a post-condition for F1, where H' may be of type hprop or of type unit->hprop. Use xseq_no_xpull H' to prevent xpull from being called automatically after xseq H'.

xval is used to reason on a let-value node, i.e. on a goal of the form (Val x := v in F1) H Q. It produces an equality x = v. Use xval as y to rename x into y. Use xval as y E to rename x into y and name E the equality y=v.

xvals is like xval but it immediately substitutes the equality x = v produced by xval.

xval_st P is used to assign an abstract specification to the value. Instead of producing x = v as hypothesis, it produces P x as hypothesis, and issues P v as subgoal. Use xval_st P as y to rename x into y. Use xval_st P as y Hy to rename x into y and specify the name of the hypothesis P y.

xind_skip allows to assume the current goal to be already true. It is useful to test a proof before justifying termination. It applies to a goal G and turns it into G -> G. Typical usage: xind_skip ;=> IH. Use it for development purpose only. Variant: xind_skip as IH, equivalent to xind_skip ;=> IH.

xfun applies to a goal of the form (LetFunc f := H in F) H Q. The tactic introduces an hypothesis describing the most-general specification of f, and leaves F H Q as goal.

• xfun as f can be used to name the function.
• xfun as f Hf can be used to name the function and its specification.
• xfun P can be used to give a specification for f, proved with respect to the most-general specification. Here, P should take the form fun f => spec_of_f. When this tactic fails, try xfun_no_simpl P as f Sf. intros. xapp_types. apply Sf.
• xfun_ind R P is a shorthand for proving a recursive function by well-founded induction on the first argument quantified in P. It is similar to xfun_no_simpl P, followed by intros n and induction_wf IH: R n, and then exploiting the characteristic formula. The binary relation R needs to be shown well-founded. Typical relation includes downto 0 and upto n for induction on the type int. TODO: show a demo when R is a measure.
• xfun_no_simpl P is like xfun P but does not attempt to automatically exploit the most general specification for proving the special specification. Use xapp or apply to continue the proof.
• xfun_ind_no_simpl R P is like xfun_ind R P but does not attempt to automatically exploit the most general specification for proving the special specification. Use xapp or apply to continue the proof.
• xfun_ind_skip P is a development tactic used to skip the need to justify termination.
• Also available: xfun P as f xfun P as f Hf xfun_no_simpl P as f xfun_no_simpl P as f Hf xfun_ind R P as IH xfun_ind_no_simpl R P as IH xfun_ind_skip_no_simpl P

xret applies to a goal of the form (Ret v) H Q, (or, more generally, on goals of the from (Let x := (Ret V) in F) H Q in which case xlet is called first). It changes the goal to H ==> Q v \* \GC, where \GC can be instantiated with garbage. Use xret_no_gc to only produce the goal H ==> Q v. Note that xret automatically calls xclean then xpull. Variants:

• xret_no_clean may be used to disable xclean and xpull.
• xret_no_pull may be used to disable xpull.
• xret_no_gc can be used to not introduce an existentially- quantified heap for garbage collection.
• xrets has a different behavior depending on the goal:
  • If the goal is Ret v, then it is short for xret; xsimpl.
  • If the goal is Let .., then it is short for xret; xpull; try intro_subst.
• xret Q is like xret but assigns the post-condition of the formula Ret v to Q.
• xrets Q is like xrets but assigns the post-condition of the formula Ret v to Q.

xassert applies to a goal of the form (Assert F) H Q, (or, more generally, of the form (Seq_ (Assert F) ;; F') H Q, in which case xseq is called first.). It produces two subgoals: F H (fun (b:bool) => \[b = true] \* H) and H ==> Q tt. The second one is discharged automatically if Q is not instantiated---this is the case whenever.

xif is a tactic that applies to a goal of the form (If v Then F1 else F2) H Q. It leaves two subgoals F1 H Q under the assumption v=true and F2 H Q under the assumption v=false. xif also applies to a goal of the form (Let x = (If v Then F1 Else F2) in ...) H Q. In this case, it calls xlet first. If Q is not instantiated, it will automatically be instantiated with if v then ?Q1 else ?Q2. Without this behavior, when the post-condition is not instantiated, then the post-condition will be inferred when solving the first branch, and it will very likely not fit the second branch. Sometimes it is preferable to specify Q explicitly, calling xif Q. The tactic xif attemps to simplify or prove false from obvious contradictions. Variants:

• xif_no_simpl avoids proving false from obvious contradictions.
• xif_no_intros leaves the hypothesis in the goals.
• xif_no_simpl_no_intros combines the above two.
• xif Q' allows to specify the post-condition. It is useful when the post Q is an evar. Equivalent to xpost Q'; xif.
• xif as X allows to name X the hypothesis v=true or v=false.

Also available;

• xif Q' as X
• xif_no_simpl as X
• xif_no_simpl Q'
• xif_no_simpl Q' as X
• xif_no_intros Q'
• xif_no_simpl_no_intros Q'

xand applies to a goal of the form (And v1 `&&` F2) H Q, which is sugar for (If v1 Then F2 Else (Ret false)) H Q. It also applies to a goal of the form (Let x = (And v1 `&&` F2) in ...) H Q.

• xand is a shorthand for xif followed by xret in the second branch.
• xand as H is similar; it allows naming the hypothesis.
• xand Q is short for xlet Q followed by xand in the first branch.
• xands is similar, it calls xrets instead of xret.

Variants:

• xand Q as H
• xands Q
• xands Q as H
• All xif variants are also applicable directly.

xor applies to a goal of the form (Or v1 `||` F2) H Q, which is sugar for (If v1 Then (Ret true) Else F2) H Q. It also applies to a goal of the form (Let x = (Or v1 `||` F2) in ...) H Q.

• xor is a shorthand for xif followed by xret in the first branch.
• xor as H is similar; it allows naming the hypothesis.
• xor Q is short for xlet Q followed by xor in the first branch.
• xors is similar, it calls xrets instead of xret.

Variants:

• xor Q as H
• xors Q
• xors Q as H
• All xif variants are also applicable directly.

xfail simplifies a proof obligation of the form Fail H Q, which is in fact equivalent to False. It automatically calls xclean on the remaining goal, to help. Variants:

• xfail_no_clean prevents xclean from being called.
• xfail C is a shorthand for xfail; false C.

xwhile applies to a goal of the form (While F1 Do F2) H Q. It introduces an abstract local predicate S that denotes the behavior of the loop. The goal is S H Q. An assumption is provided to unfold the loop: forall H' Q', (If_ F1 Then (Seq_ F2 ;; S) Else (Ret tt)) H' Q' -> S H' Q'. After xwhile, the typical proof pattern is to generalize the goal by calling assert (forall X, S (Hof X) (Qof X) for some predicate Hof and Qof and then performing a well-founded induction on X w.r.t. wf relation. (Or, using xind_skip to skip the termination proof.) Alternatively, one can call one of the xwhile_inv tactics described below to automatically set up the induction. The use of an invariant makes the proof simpler but Forms:

• xwhile is the basic form, described above.
• xwhile as S is equivalent to xwhile; intros S LS HS.
• xwhile_inv I R where R is a well-founded relation on type A and then invariant I has the form fun (b:bool) (X:A) => H. Compared with xwhile, this tactic saves the need to set up the induction. However, this tactic does not allow calling the frame rule during the loop iterations.
• xwhile_inv_basic I R where R is a well-founded relation on type A and then invariant I has the form fun (b:bool) (X:A) => H. This tactic processes the loop so as to provide separate goals for the loop condition and for the loop body. However, this tactic should not be use when both the loop condition and the loop body require unfolding a representation predicate.
• xwhile_inv_basic_measure I where then invariant I has the form fun (b:bool) (m:int) => H, where b indicates whether the loop has terminated, and m gives the measure of H. It is just a special case of xwhile_inv_basic.
• xwhile_inv_skip I is similar to xwhile_inv, but the termination proof is not required. Here, I takes the form fun (b:bool) => H.
• xwhile_inv_basic_skip I is similar to xwhile_inv_basic, but the termination proof is not required. Here, I takes the form fun (b:bool) => H.