Proof mode

The symbol command followed by begin 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).

General tactics, tactics on equality and tacticals (tactic combinators) can be used 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.

One can quit the proof mode by using the following commands:

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.

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;