Tutorial: Interactive Proofs

This tutorial teaches you how to develop proofs interactively using the VS Code goal state viewer. Instead of writing a complete proof tactic and hoping it works, you'll build proofs step by step, observing how each tactic transforms the proof state.

The interactive workflow

The key insight: you don't need to write a complete proof all at once. Instead:

State the theorem without a tactic annotation
Open the goal state viewer to see what needs to be proved
Add tactics one at a time, observing their effect
Iterate until all subgoals are closed

Setting up

Let's work through a concrete example. Create a file with these definitions:

let rec rev = function
  | [] -> []
  | x :: xs -> rev xs @ [x]
 
let k x = x + 1 - 1
 
lemma k_eq x = k x = x [@@rw]
 
lemma rev_len x =
  List.length (List.rev x) = List.length x
[@@by auto] [@@rw]
 
lemma len_append x y =
  List.length (x @ y) = List.length x + List.length y
[@@by auto] [@@rw]
 
lemma add_commutes x y =
  x + y = y + x
[@@by auto] [@@rw] [@@perm]

Now let's prove this theorem interactively:

theorem foo x y =
  k (List.length (List.rev (x @ y))) = (List.length (y @ x))

Step 1: See the initial goal

Click on the theorem in VS Code. The goal state viewer shows:

Goal:
  k (List.length (List.rev (x @ y))) = List.length (y @ x)

No hypotheses yet — this is a universally quantified statement.

Step 2: Try simplification with specific rules

Add a tactic and observe:

theorem foo x y =
  k (List.length (List.rev (x @ y))) = (List.length (y @ x))
[@@by [%simp_only rev_len]]

After [%simp_only rev_len], the goal becomes:

Goal:
  k (List.length (x @ y)) = List.length (y @ x)

The rev has been eliminated using the rev_len rewrite rule.

Step 3: Apply more rules

Extend the tactic:

[@@by [%simp_only rev_len]
   @> [%simp_only len_append, k]]

After applying len_append and unfolding k, the goal becomes:

Goal:
  List.length x + List.length y = List.length y + List.length x

Step 4: Close with arithmetic

This is just commutativity of addition. The add_commutes permutative rule handles it, or arith can close it directly:

[@@by [%simp_only rev_len]
   @> [%simp_only len_append, k]]

In fact, [%simp rev_len, len_append] handles the entire proof in one step because it uses all available rules including add_commutes:

theorem foo x y =
  k (List.length (List.rev (x @ y))) = (List.length (y @ x))
[@@by [%simp rev_len, len_append]]

Working with subgoals

When induction or case splits generate multiple subgoals, the goal state viewer shows each one. Let's see this with a more complex example:

let rec square_sum xs =
  match xs with
  | [] -> 0
  | x :: xs -> x * x + square_sum xs
 
theorem square_sum_non_neg xs =
  square_sum xs >= 0

Attempt 1: Try auto

[@@by auto]

If auto doesn't succeed immediately, we can try a manual approach.

Attempt 2: Induction + manual

[@@by induction ()
  @>| [
    (* Base case: xs = [] *)
    [%norm square_sum xs] @> arith;
 
    (* Inductive step: xs = a :: xs' *)
    [%norm square_sum xs]
     @> [%use square_psd (List.hd xs)]
     @> arith
  ]]

Where square_psd is a helper:

lemma square_psd x = x * x >= 0

The goal state viewer shows each subgoal after induction ():

Subgoal 1 (base case):

Goal: square_sum [] >= 0

After [%norm square_sum xs]: 0 >= 0, closed by arith.

Subgoal 2 (inductive step):

Hypotheses:
  IH: square_sum (List.tl xs) >= 0

Goal: square_sum xs >= 0

After normalizing and using square_psd, the goal becomes arithmetic over non-negative values, which arith handles.

(* Instead of proving this inline... *)
theorem big_theorem x y z = complex_property x y z
[@@by (* long tactic that's getting unwieldy *)]
 
(* Extract the hard part as a lemma *)
lemma helper x = tricky_part x
[@@by auto] [@@rw]
 
(* Now the main theorem is easier *)
theorem big_theorem x y z = complex_property x y z
[@@by auto]

Use `[%use ...]` liberally

When you can see that a known fact would close the goal but the simplifier isn't applying it, use [%use ...] to add it explicitly.

Read the error messages

When a tactic fails, the error message often tells you exactly what went wrong. Common situations:

"No matching rewrite rule" — the rule you expected isn't firing; check the pattern
"Subgoal not closed" — the tactic didn't fully prove the goal; you need additional steps
"Induction failed" — the chosen scheme doesn't match the problem; try a different one

What you've learned

The interactive proof development workflow: state → observe → add tactic → iterate
How to use the VS Code goal state viewer to understand proof states
Step-by-step tactic application and observing transformations
When to extract lemmas from complex proofs
Debugging proofs when tactics don't succeed