Strategy#

Ltac2.Rewrite.Strategy

Module for rewrite strategies used by Rewrite.rewrite_strat.

val fail : t

Failure.

val id : t

Success without progress.

val refl : t

Success with progress.

val progress : t -> t

Applies the argument and fails if no progress was made.

val seq : t -> t -> t

seq left right applies left, and then right if left succeeded.

val seqs : t list -> t

Equivalent to List.fold_left seq id.

val choice : t -> t -> t

choice left right applies left, and then right if left failed.

val choices : t list -> t

Equivalent to List.fold_left choice fail.

val try_ : t -> t

try_ t is equivalent to choice t id.

val fix : (t -> t) -> t

Fixed point operation for recursive strategies. fix (fun f -> s) evaluates to s [f / fix (fun f -> s)]. The function provided in the argument is executed only once when the strategy is constructed — it cannot be used to dynamically manage the rewriting.

val any : t -> t

Applies the argument until it fails.

val repeat : t -> t

repeat s is equivalent to seq s (any s).

val subterm : t -> t

Applies the argument to the leftmost immediate subterm of the considered term on which progress can be made.

val subterms : t -> t

Applies the argument to all immediate subterms of the considered term, left-to-right.

val bottomup : t -> t

Traverses the term bottom-up, left-to-right and applies the argument at each step as many times as possible.

val topdown : t -> t

Traverses the term top-down, left-to-right and applies the argument at each step as many times as possible.

val innermost : t -> t

Traverses the term bottom-up, left-to-right until the argument makes progress.

val outermost : t -> t

Traverses the term top-down, left-to-right until the argument makes progress.

val hints : ident -> t

Applies hints from the rewrite hint database.

val old_hints : ident -> t
val term : preterm -> ltr:bool -> t

Unifies one side of the lemma with the current subterm and on success rewrites it to the other side. If ltr is true, rewrites left-to-right; otherwise, rewrites right-to-left.

val terms : preterm list -> t

terms l is equivalent to choices (List.map (fun c -> one_lemma c ~ltr:true) l).

val fold : constr -> t

Replaces the term under consideration with the argument if they unify.

val eval : Redexpr.red_expr -> t

Converts the term under consideration.

val matches : pattern -> t

The identity if the pattern matching succeeds, fails otherwise.

  • since 9.3
val tactic : (constr -> constr -> constr option -> Rewrite.Result.t Proofview.tactic) -> t

The tactic f strategy applies f to arguments ty, lhs and rel, where lhs is the subterm being rewritten, of type ty, and an optional relation constraint rel is given.

The tactic is applied to a single goal of type unit whose context corresponds to the context of the term to rewrite (i.e., the context of the goal at the start of the Rewrite.rewrite_strat call extended with the binders that were traversed to attain this subterm). The tactic should return a Rewrite.Result.t indicating success, failure or no progress and should not solve the goal. Solving the goal is an error that aborts the Rewrite.rewrite_strat call. The success record contains the chosen relation rel, new right-hand side rhs and a proof prf of rel t rhs.

If the proof prf is syntactically eq_refl _, then the witness of the rewriting is simply a conversion requiring no explicit proof and no congruence lemmas for the context of the rewrite.

  • since 9.3