Std#

Ltac2.Std

Applying theorems#

val assumption : ?e:bool -> unit -> unit Proofview.tactic

assumption () looks in the local context for a hypothesis whose type is convertible to the goal. If it is the case, the subgoal is proved. Otherwise, it fails.

  • parameter e default: false

    If e is true, behaves like eassumption instead, which is able to process goals and hypotheses with existential variables. It can also resolve existential variables, which assumption will not.

val apply : ?e:bool -> ?in_hyp_as:(ident * Syntax.simple Syntax.intropattern option) -> Syntax.constr_with_bindings list -> unit Proofview.tactic

apply ?e ts ?in_hyp_as uses unification to match the type of each t with the goal (to do backward reasoning) or with a hypothesis (to do forward reasoning). Specifying multiple constr_with_bindings is equivalent to giving each one serially, left to right, as separate apply tactics.

  • parameter e default: false

    If e is true, creates existential variables when Rocq is unable to deduce instantiations for variables, rather than failing.

  • parameter in_hyp_as default: None

    Which hypothesis to apply in. The second argument specifies the as intro pattern.

Managing the local context#

val intro : ?name:ident -> ?where:Syntax.move_location -> unit -> unit Proofview.tactic

intro ?name ?where () introduces an item in the context by removing certain constructs in the goal. If no item is found, the tactic fails.

  • parameter name default: None

    The name to give to the introduced item. If not given, Rocq uses the variable name from the forall or H for premises. If a name such as H is already in use, Rocq will consider using H0, H1, etc., until it finds a fresh name.

  • parameter where default: move_location.At_bottom

    Indicates where to place the introduced hypothesis: at the top or bottom of the context or before or after another specified hypothesis.

val intros : ?e:bool -> Syntax.any Syntax.intropattern list -> unit Proofview.tactic

intros ?e patterns introduces a list of new variables in the context using the patterns. If patterns is empty, the tactic introduces items until it reaches the head constant; it never fails and may leave the context unchanged.

  • parameter e default: false

    If true, an existential variable is created for any unresolved variable instead of failing. Typically, this happens when using a % intropattern.

val intros_until : Syntax.hypothesis -> unit Proofview.tactic

intros_until nat_or_hyp repeats intro until it has introduced a dependent premise with the given name, or has introduced the given number of premises.

We recommend explicitly naming items with intros instead of using intros_until (Nth_hyp n).

val revert : ident list -> unit Proofview.tactic

revert hyps moves the specified hypotheses and local definitions to the goal, if this respects dependencies. This is the inverse of intros.

move hyp where moves hyp and hypotheses that directly or indirectly refer to hyp that appear between hyp and where.

val clear : ident list -> unit Proofview.tactic

clear hyps erases unneeded hypotheses in hyps from the context of the current goal. "Unneeded" means that the unselected hypotheses and the goal don't refer directly or indirectly to the erased hypotheses. That means the hypotheses will no longer appear in the context and therefore can't be used in subsequent proof steps. Note that erasing an unneeded hypothesis may turn a goal that was provable into an unprovable goal.

val keep : ident list -> unit Proofview.tactic

keep hyps is the converse of clear, keeping only needed hypotheses in hyps.

val clearbody : ident list -> unit Proofview.tactic

clearbody hyps clears the body of the given hyps in the context of the current goal.

val rename : (ident * ident) list -> unit Proofview.tactic

rename l simultaneously renames hypotheses from the first name to the second.

val set : ?e:bool -> ?where:Syntax.clause -> Names.Name.t -> constr -> unit Proofview.tactic

set ?e name t ?where adds a new local definition name := t and replaces the body expression with the new variable name in the goal, or as specified by where.

  • parameter e default: false

    If e is true, generates existential variables for uninstantiated variables instead of failing. In practice, this is relevant only when eset is used as a synonym of epose, i.e., when the term does not occur in the goal.

val remember : ?e:bool -> ?as_name:ident -> ?eqn:Syntax.naming Syntax.intropattern -> ?where:Syntax.clause -> constr -> unit Proofview.tactic

remember ?e t ?as_name ?eqn ?where is similar to set ?e as_name t ?where but creates a hypothesis using Leibniz equality to remember the relation between the introduced variable and the term rather than creating a local definition. If as_name is not specified, a fresh name is used. Use eqn to name the new equation.

  • parameter e default: false

    If e is true, generates existential variables for uninstantiated variables instead of failing.

  • parameter eqn default: (??)

    Specifies how to name the introduced equation.

val pose : Names.Name.t -> constr -> unit Proofview.tactic

pose name t is similar to set name t, but does not perform any replacements.

Note: this version of pose does not fail on uninstantiated existential variables. To make it behave like Ltac's pose, use Control.with_holes.

Controlling the proof flow#

val assert_ : ?as_pattern:Syntax.simple Syntax.intropattern -> ?by:unit Proofview.tactic -> constr -> unit Proofview.tactic

assert_ t ?as_pattern ?by adds a new hypothesis to the current subgoal and a new subgoal before it to prove the hypothesis.

Note: this version of assert does not fail on uninstantiated existential variables. To make it behave like Ltac's assert, use Control.with_holes.

val enough : ?as_pattern:Syntax.simple Syntax.intropattern -> ?by:unit Proofview.tactic -> constr -> unit Proofview.tactic

enough t ?as_pattern ?by adds a new hypothesis to the current subgoal and a new subgoal after it to prove the hypothesis.

val cut : constr -> unit Proofview.tactic

cut P transforms the current goal G into two subgoals: P -> G and P. This is the cut rule: to prove G, it suffices to prove that P implies G and that P itself holds.

This tactic is generally considered obsolete but it is still widely used in old scripts.

specialize t ?as_pattern specializes t (typically a hypothesis or lemma) by applying arguments to it.

val generalize : (constr * int Syntax.occurrences * Names.Name.t) list -> unit Proofview.tactic

generalize [(t, where, x)] replaces the goal G with forall (x: T), G', where t is a subterm of G of type T, and G' is obtained by replacing all occurrences of t with x within G. Specifying multiple t is equivalent to generalize t₁; …; generalize tₙ.

val absurd : constr -> unit Proofview.tactic

absurd P applies False elimination, that is, it deduces the current goal from False, and generates as subgoals ~P and P. It is very useful in proofs by cases, where some cases are impossible. In most cases, P or ~P is one of the hypotheses of the local context.

val contradiction : ?witness:Syntax.constr_with_bindings -> unit -> unit Proofview.tactic

contradiction ?witness () tries to prove the current goal by finding a contradiction.

If witness is not provided (the most common use case), the tactic first does an intros. The tactic then proves the goal if

  • The updated context has a pair of hypotheses where one is the negation of the other (e.g., P and ~P), or
  • There is a hypothesis with an empty inductive type (e.g., False), or
  • There is a hypothesis ~P where P is a singleton inductive type (e.g., True or x=x) provable by constructor.
  • parameter witness default: None

    If witness is provided, its type must be a negation, such as ~P, or an empty inductive type, such as False. If the type is a negation and P is a hypothesis in the context, the goal is proven. If the type is a negation and P is not in the context, the goal is replaced with P. If the type is False or another empty inductive type, the goal is proven. Otherwise the tactic fails.

val exfalso : unit Proofview.tactic

Implements the "ex falso quodlibet" logical principle: an elimination of False is performed on the current goal, and the user is then required to prove that False is indeed provable in the current context.

val admit : unit Proofview.tactic

Admits the current goal. This marks the current goal as an axiom and closes it, leaving the proof incomplete. Useful for debugging or for temporarily accepting unprovable goals.

Performance-oriented tactic variants#

val exact_no_check : constr -> unit Proofview.tactic

For advanced usage. exact_no_check t is similar to exact t, but as an optimization, it skips checking that t has the goal's type, relying on the kernel check instead.

val vm_cast_no_check : constr -> unit Proofview.tactic

For advanced usage. vm_cast_no_check t is similar to exact_no_check t, but additionally instructs the kernel to use vm_compute to compare the goal's type with t's type.

val native_cast_no_check : constr -> unit Proofview.tactic

For advanced usage. native_cast_no_check t is similar to exact_no_check t, but additionally instructs the kernel to use native_compute to compare the goal's type with t's type.

Reasoning with equalities#

Tactics for simple equalities#

val reflexivity : unit Proofview.tactic

After doing an intros, if the resulting goal is in the form t = u in which t and u are definitionally equal, the tactic proves the goal (by applying eq_refl). If not, it fails.

val symmetry : ?where:Syntax.clause -> unit -> unit Proofview.tactic

Changes a goal that has the form forall x₀ … xₙ, t = u into u = t.

  • parameter where default: default_on_conclusion

    Controls where to apply the change, i.e., in the selected hypotheses and/or the conclusion.

val transitivity : constr -> unit Proofview.tactic

transitivity x changes a goal that has the form forall x₀ … xₙ, t = u into the two subgoals t = x and x = u.

val etransitivity : unit Proofview.tactic

etransitivity behaves like transitivity, using a fresh evar instead of a concrete term.

val f_equal : unit Proofview.tactic

For a goal with the form f a₁ … aₙ = g b₁ … bₙ, creates subgoals f = g and aᵢ = bᵢ for the n arguments. Subgoals that can be proven by reflexivity or congruence are solved automatically.

Rewriting with Leibniz and setoid equality#

val rewrite : ?e:bool -> ?where:Syntax.clause -> ?by:unit Proofview.tactic -> Syntax.oriented_rewriter list -> unit Proofview.tactic

rewrite rs ?e ?where ?by replaces subterms with other subterms that have been proven to be equal or logically equivalent.

  • parameter e default: false

    If e is true, turns unresolved bindings, if any, into existential variables instead of failing.

setoid_rewrite ?orient ?in_hyp c occs rewrites an occurrence of the term matched by c in the goal or the specified hypothesis using a setoid equality. Unlike rewrite, this tactic works with relations registered through the generalized rewriting framework.

  • parameter orient default: (-->)

    The rewrite orientation. If (-->) (left-to-right), rewrites from the LHS to the RHS of the equation. If (<--), rewrites right-to-left.

  • parameter in_hyp default: None

    The name of the hypothesis in which to rewrite. If not provided, rewrites in the goal.

val subst : ?hyps:ident list -> unit -> unit Proofview.tactic

subst ?hyps substitutes each hypothesis id : x = t (or t = x) in the goal, replacing x by t everywhere. Only hypotheses of the form x = t or t = x where x is a variable are considered.

If hyps is not specified, performs substitution of all known equalities in the goal.

val change : ?pattern:pattern -> ?where:Syntax.clause -> (constr Names.Id.Map.t -> constr) -> unit Proofview.tactic

change ?pattern f cl finds subterms matching pattern in the selected hypotheses and/or conclusion specified by cl, and replaces them with f args where args are the matched subterms.

  • parameter pattern default: None

    Specifies the pattern of terms that are replaced. If not specified, then f replaces the conclusion and/or the hypotheses, as specified by where.

  • parameter where default: default_on_conclusion

    Where to apply the replacement.

Applying conversion rules#

module Red : sig ... end
val eval_in : Red.t -> Syntax.clause -> unit Proofview.tactic

eval_in red cl performs the reduction specified by red in the selected hypotheses and/or conclusion specified by cl.

eval red c reduces the term c using the specified reduction red and returns the resulting term, without modifying the goal.

Reasoning with inductive types#

Applying constructors#

val constructor : ?e:bool -> ?n:int -> ?with_:Syntax.bindings -> unit -> unit Proofview.tactic

constructor ?e ?n ?with_ () applies the n-th constructor, if specified, or the first matching constructor to prove the current goal. Fails if no constructor applies.

  • parameter e default: false

    If e is true, creates existential variables for uninstantiated variables instead of failing.

val split : ?e:bool -> ?with_:Syntax.bindings -> unit -> unit Proofview.tactic

split ?e ?with_ () proves a conjunction A /\ B or an iff A <-> B by splitting it into subgoals. For conjunction, the left conjunct becomes the first subgoal. Any bindings are applied to the constructor.

  • parameter e default: false

    If e is true, creates existential variables for uninstantiated variables instead of failing.

val left : ?e:bool -> ?with_:Syntax.bindings -> unit -> unit Proofview.tactic

left ?e ?with_ () proves a disjunctive goal A \/ B by selecting the left disjunct A, generating a subgoal for A. Any bindings are applied to the constructor.

  • parameter e default: false

    If e is true, creates existential variables for uninstantiated variables instead of failing.

val right : ?e:bool -> ?with_:Syntax.bindings -> unit -> unit Proofview.tactic

right ?e ?with_ () proves a disjunctive goal A \/ B by selecting the right disjunct B, generating a subgoal for B. Any bindings are applied to the constructor.

  • parameter e default: false

    If e is true, creates existential variables for uninstantiated variables instead of failing.

Case analysis#

val destruct : ?e:bool -> ?using:Syntax.constr_with_bindings -> Syntax.Induction_clause.t list -> unit Proofview.tactic

destruct clauses ?e ?using performs case analysis on each clause in clauses, generating a subgoal for each of the constructors of the inductive type.

  • parameter e default: false

    If e is true, creates existential variables for uninstantiated variables instead of failing.

  • parameter using default: None

    The elimination principle to use instead of the default one.

val case : ?e:bool -> Syntax.constr_with_bindings -> unit Proofview.tactic

case c ?e is an older, more basic tactic to perform case analysis without recursion. We recommend using destruct instead where possible. case only modifies the goal; it does not modify the local context.

  • parameter e default: false

    If e is true, creates existential variables for uninstantiated variables instead of failing.

Induction#

val induction : ?e:bool -> ?using:Syntax.constr_with_bindings -> Syntax.Induction_clause.t list -> unit Proofview.tactic

induction clauses ?e ?using applies induction principles to each clause in clauses, left to right.

  • parameter e default: false

    If e is true, creates existential variables for uninstantiated variables instead of failing.

  • parameter using default: None

    The induction principle to use instead of the default one.

elim c ?e ?using is an older, more basic induction tactic. Unlike induction, elim only modifies the goal; it does not modify the local context. We recommend using induction instead where possible.

  • parameter e default: false

    If e is true, creates existential variables for uninstantiated variables instead of failing.

  • parameter using default: None

    The induction principle to use instead of the default one.

val fix : ident -> int -> unit Proofview.tactic

fix f n is a primitive tactic that starts a proof by induction. Generally, higher-level tactics such as induction or elim are easier to use.

val cofix : ident -> unit Proofview.tactic

cofix f starts a proof by coinduction.

Equality of inductive types#

val discriminate : ?e:bool -> ?arg:Syntax.Induction_arg.t -> unit -> unit Proofview.tactic

discriminate ?e ?arg () proves the current goal by discriminating an equality between two constructors of the same inductive type. The argument arg specifies which hypothesis or term to discriminate.

  • parameter e default: false

    If e is true, creates existential variables for uninstantiated variables instead of failing.

  • parameter arg default: None

    The induction argument specifying what to discriminate. If not provided, the current goal's hypotheses are checked.

val injection : ?e:bool -> ?arg:Syntax.Induction_arg.t -> ?as_patterns:Syntax.simple Syntax.intropattern list -> unit -> unit Proofview.tactic

injection ?e ?as_patterns ?arg () exploits the property that constructors of inductive types are injective, i.e., that if c is a constructor of an inductive type, then c t1 = c t2 implies t1 = t2.

  • parameter e default: false

    If e is true, creates existential variables for uninstantiated variables instead of failing.

  • parameter arg default: None

    The induction argument specifying what to inject. If not provided, the current goal's hypotheses are used.

  • parameter as_patterns default: None

    Intro patterns for naming the injected equalities. If not provided, fresh names are generated.

val inversion : ?kind:Syntax.inversion_kind -> ?as_pattern:Syntax.or_and Syntax.intropattern -> ?in_hyps:ident list -> Syntax.Induction_arg.t -> unit Proofview.tactic

inversion ?kind arg ?as_pattern ?in_hyps performs inversion on the given term arg using the specified kind of inversion. Inversion generates equations for all constructors of the inductive type of arg and proves the goal by case analysis.

  • parameter kind default: Full

    The inversion depth: Simple does not clear hypotheses, Full clears trivially equal hypotheses, and Full_clear additionally clears inverted hypotheses.

  • parameter as_pattern default: None

    An intro pattern for naming the generated hypotheses.

  • parameter in_hyps default: None

    If specified, performs a generalize in_hyps as the initial step.

Solvers for logic and equality#

val congruence : ?n:int -> ?hints:constr list -> unit -> unit Proofview.tactic

congruence ?n ?hints () solves the current goal using the congruence closure algorithm, which reasons about equations between constructors and function applications.

  • parameter n default: None

    An optional depth limit for the search.

  • parameter hints default: None

    Additional equations to use, provided as a list of terms.

val simple_congruence : ?n:int -> ?hints:constr list -> unit -> unit Proofview.tactic

simple_congruence ?n ?hints () behaves like congruence but does not unfold definitions.

  • parameter n default: None

    An optional depth limit for the search.

  • parameter hints default: None

    Additional equations to use, provided as a list of terms.

Misc#

val resolve_tc : constr -> unit Proofview.tactic

resolve_tc c resolves the existential variables appearing in the constr whose types are typeclasses. Fails if they cannot be resolved. Does not focus.

val unify : constr -> constr -> unit Proofview.tactic

unify x y checks that x and y are convertible (definitionally equal) in the current context. Fails if they are not unifiable.