Syntax

Ltac2.Syntax

Hypotheses

type hypothesis = private ..

Type of hypothesis target.

type hypothesis +=

1. | Named_hyp of ident
   (*

   Named_hyp h selects hypothesis h.

   *)
2. | Nth_hyp of int
   (*

   Nth_hyp n selects the n-th hypothesis.

   *)

Bindings

• see Reference manual, "Bindings"

type bindings = private ..

Type of term bindings.

type bindings +=

1. | No_bindings
   (*

   An empty list of bindings.

   *)
2. | Implicit of constr list
   (*

   Implicit [t₁; …; tₙ] binds free variables in left-to-right order of their first appearance in the relevant term.

   *)
3. | Explicit of (hypothesis * constr) list
   (*

   Explicit [(h₁, t₁); …; (hₙ, tₙ)] binds variables hᵢ to tᵢ.

   *)

type constr_with_bindings = {

1. t : constr;
2. bindings : bindings;

}

A term with bindings.

val term : constr -> constr_with_bindings

term t adds default bindings to t.

Expected usage: { (term t) with bindings = … }.

Intropatterns

type +'a intropattern

An intropattern lets you specify the name to assign to variables and hypotheses introduced by tactics.

The type variable is used for statically distinguishing subtypes of intropatterns.

type naming = [

1. | `Naming

]

Tag for intropatterns used for naming hypotheses (e.g., in eqn: clauses).

type or_and = [

1. | `Or_and

]

Tag for intropatterns that split conjunctions/disjunctions, sometimes used in as clauses.

type orientation = [

1. | `Orientation

]

Tag for intropatterns that are used as rewrite orientations (i.e., (-->) and (<--)).

type equality = [

1. | orientation
2. | `Equality

]

Tag for equality intropatterns.

type simple = [

1. | naming
2. | or_and
3. | equality

]

Tag for simple intropatterns.

type other = [

1. | `Other

]

Tag for other intropatterns.

type any = [

1. | simple
2. | other

]

Top tag for all intropatterns.

Useful in error messages.

Naming patterns

val name : ident -> [> naming ] intropattern

name ident uses the specified name.

val (??) : [> naming ] intropattern

(??) lets Rocq generate a fresh name.

val (?:) : ident -> [> naming ] intropattern

?:ident lets Rocq generate a fresh name that begins with ident.

Splitting patterns

val (&) : simple intropattern -> simple intropattern -> [> or_and ] intropattern

p1 & p2 splits a hypothesis of the form A /\ B into p1: A and p2: B. Right-associative.

val and_pattern : simple intropattern list -> [> or_and ] intropattern

and_pattern [p₁; …; pₙ] is equivalent to p₁ & … & pₙ.

val or_pattern : any intropattern list list -> [> or_and ] intropattern

or_pattern [[p₁₁; …; p₁ₘ]; …; [pₙ₁; …; pₙₖ]] destructs a hypothesis whose inductive type has n constructors (e.g., A₁ ∨ … ∨ Aₙ) into n subgoals. In the i-th subgoal, the arguments of the i-th constructor are named by the patterns of the i-th inner list. Corresponds to [p₁₁ … p₁ₘ | … | pₙ₁ … pₙₖ] in Ltac.

Equality patterns

These patterns can be used when the hypothesis is an equality.

val (-->) : [> orientation ] intropattern

Replaces the LHS of the hypothesis with the RHS in the conclusion of the goal.

val (<--) : [> orientation ] intropattern

Replaces the RHS of the hypothesis with the LHS in the conclusion of the goal.

val (@=) : any intropattern list -> [> equality ] intropattern

Applies either Std.injection or Std.discriminate.

Other patterns

val __ : [> simple ] intropattern

Wildcard intropattern that discards the matched pattern (unless it is required by another hypothesis).

val (@*) : [> other ] intropattern

Introduces one or more dependent premises from the result until there are no more.

val (@**) : [> other ] intropattern

Introduces one or more dependent or non-dependent premises from the result until there are no more premises.

val (%) : simple intropattern -> constr -> [> simple ] intropattern

pattern%term first applies term with the Std.apply tactic on the hypothesis to be introduced, then it uses pattern.

Occurrences

type _ occurrences = private ..

An occurrence is a subterm of a goal or hypothesis that matches a pattern.

type occurrences +=

1. | At : 'a list -> 'a occurrences
   (*

   At l selects the specified occurrences.

   *)
2. | Everywhere : 'a occurrences
   (*

   Everywhere selects every occurrence (similar to Ltac's *).

   *)
3. | Everywhere_but : int list -> int occurrences
   (*

   Everywhere_but l selects every occurrence that is not in l (similar to Ltac's at -l).

   *)
4. | Nowhere : 'a occurrences
   (*

   Nowhere selects no occurrence.

   *)

Clauses

type hypothesis_selector = private ..

Selects whether an occurrence should apply to the type or value of the hypothesis.

type hypothesis_selector +=

1. | Hyp of ident
   (*

   Applies to the whole hypothesis.

   *)
2. | Type_of of ident
   (*

   Selects the type part of the hypothesis.

   *)
3. | Value_of of ident
   (*

   Selects the value part of the hypothesis.

   *)

type clause

A clause selects a subset of occurrences in the hypothesis and the goal.

val (|-) : (hypothesis_selector * int occurrences) occurrences -> int occurrences -> clause

hyps_occs |- goal_occs creates a clause that selects occurrences in the hypotheses according to hyps_occs, and occurrences in the goal according to goal_occs.

Examples:

• Everywhere |- Everywhere corresponds to * |- *.
• Nowhere |- Everywhere corresponds to |- *.
• Nowhere |- Nowhere corresponds to |-.
• At [(Type_of h, Everywhere)] |- (At [1; 2]) corresponds to (type of h) |- * at 1 2.

Move locations

type move_location = private ..

Specifies where to move a hypothesis for the Std.move tactic.

type move_location +=

1. | At_top
   (*

   at top

   *)
2. | At_bottom
   (*

   at bottom

   *)
3. | Before of ident
   (*

   before h

   *)
4. | After of ident
   (*

   after h

   *)

Inversion kinds

type inversion_kind = private ..

Type of inversion performed.

type inversion_kind +=

1. | Simple
   (*

   Behaves like Ltac's simple inversion.

   *)
2. | Full
   (*

   Behaves like Ltac's inversion.

   *)
3. | Full_clear
   (*

   Behaves like Ltac's inversion_clear.

   *)

Rewrites

type multiplicity = private ..

Specifies the number of rewrites to perform.

type multiplicity +=

1. | Exactly of int
   (*

   Exactly n performs a rewrite exactly n times.

   *)
2. | At_most of int
   (*

   At_most n performs a rewrite at most n times (?n in Ltac).

   *)
3. | Star
   (*

   Star performs a rewrite as many times as possible, possibly zero.

   *)
4. | Plus
   (*

   Plus performs a rewrite as many times as possible and at least once.

   *)

type oriented_rewriter

Type of rewriters for the Std.rewrite tactic.

val (==>) : ?n:multiplicity -> ?with_:bindings -> constr -> oriented_rewriter

(==>) ?n e ?with_ rewrites using equality or equivalence e, of the form forall …, term₁ = term₂ or forall …, term₁ EQ term₂ for some equivalence relation EQ, by replacing term₁ with term₂.

• parameter n default: Exactly 1

  Number of rewrites to perform.

• parameter with_ default: bindings.No_bindings

  Bindings to use.

val (<==) : ?n:multiplicity -> ?with_:bindings -> constr -> oriented_rewriter

(<==) ?n e ?with_ rewrites using equality or equivalence e, of the form forall …, term₁ = term₂ or forall …, term₁ EQ term₂ for some equivalence relation EQ, by replacing term₂ with term₁.

• parameter n default: Exactly 1

  Number of rewrites to perform.

• parameter with_ default: bindings.No_bindings

  Bindings to use.

Induction clauses

• see Reference manual, "Case analysis"

module Induction_arg : sig ... end

module Induction_clause : sig ... end