Proof tactics

The symbol command allows the user to enter an interactive mode to solve typing goals of the form x₁:A₁, …, xₙ:Aₙ ?M : U (find a term of a given type materialized by a metavariable ?M) and unification goals of the form x₁:A₁, …, xₙ:Aₙ U V (prove that two terms are equivalent modulo the user-defined rewriting rules).

The following tactics help users to refine typing goals and transform unification goals step by step. A tactic application may generate new goals/metavariables.

Except for the solve tactic which applies to all the unification goals at once, all the other tactics applies to the first goal only, which is called the focused goal, and this focused goal must be a typing goal.

The proof is complete only when all generated goals have been solved.

Proof scripts must be structured. The general rule is: when a tactic generates several subgoals, the proof of each subgoal must be enclosed between curly brackets:

opaque symbol ≤0 [x] : π(x ≤ 0 ⇒ x = 0) ≔
begin
  have l : Π x y, π(x ≤ y ⇒ y = 0 ⇒ x = 0)
  { // subproof of l
    refine ind_≤ _ _ _
    { /* case 0 */ reflexivity }
    { /* case s */ assume x y xy h a; apply ⊥ₑ; apply s≠0 _ a }
  };
  assume x h; apply l _ _ h _; reflexivity
end;

Reminder: the BNF grammar of tactics is in lambdapi.bnf.

begin

Start a proof.

end

Exit the proof mode when all goals have been solved. It then adds in the environment the symbol declaration or definition the proof is about.

abort

Exit the proof mode without changing the environment.

admitted

Add axioms in the environment to solve the remaining goals and exit of the proof mode.

apply

If t is a term of type Π x₁:T₁, …, Π xₙ:Tₙ,U, then apply t refines the focused typing goal with t _ _ (with n underscores).

assume

If the focused typing goal is of the form Π x₁ xₙ,T, then assume h₁ hₙ replaces it by T with xᵢ replaced by hᵢ.

remove

remove h₁ hₙ erases the hypotheses h₁ hₙ from the context of the current goal. The remaining hypotheses and the goal must not depend directly or indirectly on the erased hypotheses. The order of removed hypotheses is not relevant.

generalize

If the focused goal is of the form x₁:A₁, …, xₙ:Aₙ, y₁:B₁, …, yₚ:Bₚ ?₁ : U, then generalize y₁ transforms it into the new goal x₁:A₁, …, xₙ:Aₙ ?₂ : Π y₁:B₁, …, Π yₚ:Bₚ, U.

have

have x: t generates a new goal for t and then let the user prove the focused typing goal assuming x: t.

induction

If the focused goal is of the form Π x:I …, with I an inductive type, then induction refines it by applying the induction principle of I.

refine

The tactic refine t tries to instantiate the focused goal by the term t. t can contain references to other goals by using ?n where n is a goal name. t can contain underscores _ or new metavariable names ?n as well. The type-checking and unification algorithms will then try to instantiate some of the metavariables. The new metavariables that cannot be solved are added as new goals.

simplify

With no argument, simpl normalizes the focused goal with respect to β-reduction and the user-defined rewriting rules.

If f is a non-opaque symbol having a definition (introduced with ), then simpl f replaces in the focused goal every occurrence of f by its definition.

If f is a symbol identifier having rewriting rules, then simpl f applies these rules bottom-up on every occurrence of f in the focused goal.

solve

Simplify unification goals as much as possible.

try

If T is a tactic, then try T is a tactic that applies T to the focused goal. If the application of T fails in the focused goal, it catches the error and leaves the goal unchanged.

why3

The tactic why3 calls a prover (using the why3 platform) to solve the current goal. The user can specify the prover in two ways :

  • globally by using the command prover described in Queries

  • locally by the tactic why3 "<prover_name>" if the user wants to change the prover inside an interactive mode.

If no prover name is given, then the globally set prover is used (Alt-Ergo by default).

A set of symbols should be defined in order to use the why3 tactic. The user should define those symbols using builtins as follows :

builtin "T"   ≔ … // : U → TYPE
builtin "P"   ≔ … // : Prop → TYPE
builtin "bot" ≔ … // : Prop
builtin "top" ≔ … // : Prop
builtin "imp" ≔ … // : Prop → Prop → Prop
builtin "and" ≔ … // : Prop → Prop → Prop
builtin "or"  ≔ … // : Prop → Prop → Prop
builtin "not" ≔ … // : Prop → Prop
builtin "all" ≔ … // : Π x: U, (T x → Prop) → Prop
builtin "ex"  ≔ … // : Π x: U, (T x → Prop) → Prop

Important note: you must run why3 config detect to make Why3 know about the available provers.

admit

Adds in the environment new symbols (axioms) proving the focused goal.

fail

Always fails. It is useful when developing a proof to stop at some particular point.

Tactics on equality

The tactics reflexivity, symmetry and rewrite assume the existence of terms with approriate types mapped to the builtins T, P, eq, eqind and refl thanks to the following builtin declarations:

builtin "T"     ≔ … // : U → TYPE
builtin "P"     ≔ … // : Prop → TYPE
builtin "eq"    ≔ … // : Π [a], T a → T a → Prop
builtin "refl"  ≔ … // : Π [a] (x:T a), P(x = x)
builtin "eqind" ≔ … // : Π [a] x y, P(x = y) → Π p:T a → Prop, P(p y) → P(p x)

reflexivity

Solves a goal of the form Π x₁, …, Π xₙ, P (t = u) when t u.

symmetry

Replaces a goal of the form P (t = u) by the goal P (u = t).

rewrite

The rewrite tactic takes as argument a term t of type Π x₁ xₙ,P(l = r) prefixed by an optional left (to indicate that the equation should be used from right to left) and an optional rewrite pattern in square brackets prefixed by a dot, following the syntax and semantics of SSReflect rewrite patterns:

<rw_patt> ::=
  | <term>
  | "in" <term>
  | "in" <ident> "in" <term>
  | <ident> "in" <term>
  | <term> "in" <ident> "in" <term>
  | <term> "as" <ident> "in" <term>

See examples in rewrite1.lp and A Small Scale Reflection Extension for the Coq system, by Georges Gonthier, Assia Mahboubi and Enrico Tassi, INRIA Research Report 6455, 2016, section 8, p. 48, for more details.

In particular, if u is a subterm of the focused goal matching l, that is, of the form l with x₁ replaced by u₁, …, xₙ replaced by uₙ, then the tactic rewrite t replaces in the focused goal all occurrences of u by the term r with x₁ replaced by u₁, …, xₙ replaced by uₙ.