The Waterfall

The inductive waterfall is the core of ImandraX's automated proof engine. When you write [@@by auto], you invoke the waterfall — a sophisticated pipeline that combines multiple proof strategies into a synergizing whole.

The waterfall is deeply inspired by the pioneering work of Boyer and Moore on automated induction. ImandraX lifts the Boyer-Moore waterfall to a typed, higher-order setting, extending it with modern decision procedures and ImandraX-specific innovations.

Overview

The waterfall transforms top-level goals into clauses that flow through a sequence of stages. Each stage attempts to simplify, refute, or restructure clauses:

The Inductive Waterfall

Three outcomes are possible at each stage:

  1. Clause evaporates — It's been proved! Processing continues with remaining clauses.
  2. Clause is refuted — A counterexample is found. The waterfall stops.
  3. Clause is transformed — New, simpler clauses re-enter the pool at the top.

If a clause passes through all stages unchanged, the waterfall reports failure and suggests checkpoint hints.

Stage 1: Simplification

The most consequential stage. The full simplifier is applied, using:

  • All enabled rewrite rules (left-to-right term rewriting)
  • All enabled forward-chaining rules (deriving new facts from hypotheses)
  • Decision procedures for algebraic datatypes and arithmetic
  • Case-splitting when conditionals appear in the goal

Most proofs succeed entirely through simplification. Making good use of rewrite rules to control simplification is perhaps the most powerful tool ImandraX gives you.

See Simplification for details on rewrite rules and forward chaining.

Stage 2: Unrolling check

After simplification stabilizes (no more rewrites fire), a lightweight unrolling check is applied. This uses bounded verification with a small depth limit to:

  • Find contradictions in the current goal (proving it)
  • Validate candidate generalizations and cross-fertilizations
  • Discover counterexamples to the current subgoal

This stage does not produce modified clauses — it either solves the goal or passes it through.

Stage 3: Destructor elimination

This stage transforms clauses that use destructor terms (functions that decompose values) into equivalent clauses using constructor terms (functions that build values).

For example, if a clause mentions List.hd x and List.tl x with the hypothesis x <> [], destructor elimination introduces fresh variables a and b, replaces x with a :: b, List.hd x with a, and List.tl x with b.

This cleanup makes goals more amenable to simplification and induction.

Stage 4: Fertilization

Fertilization uses equalities in the hypotheses to simplify the conclusion. When an inductive hypothesis gives us f(smaller) = g(smaller), fertilization substitutes one side for the other in the conclusion.

Cross-fertilization (the preferred form) is more disciplined: it restricts substitution to use the inductive hypothesis in a way that "crosses" between the two sides, avoiding trivial applications.

Stage 5: Generalization

Applied only during active induction attempts, generalization strengthens the goal to make it more amenable to induction.

When common subterms appear across multiple parts of the goal, ImandraX replaces them with fresh variables. This can turn a specialized statement into a general one that admits a cleaner induction.

For example, if the goal mentions f (g x) in several places, generalization might replace g x with a fresh variable y, producing a stronger (but potentially provable) goal.

Safety check

Not all generalizations are valid — the generalized goal might be false even when the original is true. ImandraX validates candidate generalizations using unrolling: if a counterexample to the generalized goal is found, the generalization is abandoned.

Generalization rules

Constrain generalizations with [@@gen]:

lemma square_gen n =
  (n * n [@trigger]) >= 0
[@@by auto] [@@gen]

When n * n is generalized to a fresh variable v, this rule adds v >= 0 as a hypothesis, preventing unsound generalization.

Stage 6: Induction

The final stage applies an induction scheme to the goal. ImandraX synthesizes schemes from the recursive functions in the goal (see Induction):

  1. The goal is instantiated into the induction scheme's structure
  2. Base cases and inductive steps are generated
  3. Each subgoal re-enters the waterfall from the top

This recursive structure is what makes the waterfall so powerful: induction generates subgoals, which are then simplified, which may trigger further induction, and so on.

The waterfall in practice

Once you've used bounded verification to confirm no counterexamples exist (see Counterexamples), most proofs require just [@@by auto]:

theorem insertion_sort_sorts xs =
  is_sorted (insert_sort xs)
[@@by auto]

When auto doesn't succeed, you typically:

  1. Add rewrite lemmas that help simplification
  2. Use [%use ...] to supply key facts the waterfall can't find on its own
  3. Guide induction with a specific scheme via induction ~id:[%id f] ()
  4. Break the proof into smaller lemmas

Example: Building up to a proof

(* Helper: insert preserves sortedness *)
theorem insert_invariant a x =
  is_sorted x ==> is_sorted (insert a x)
[@@by auto] [@@rw]
 
(* Main theorem: insertion sort produces sorted output *)
theorem insert_sort_sorts x =
  is_sorted (insert_sort x)
[@@by auto]
 
(* Helper: insert preserves element counts *)
theorem lemma_1 x a =
  num_occurs a (insert a x) = num_occurs a x + 1
[@@by auto] [@@rw]
 
theorem lemma_2 x a b =
  a <> b ==> num_occurs b (insert a x) = num_occurs b x
[@@by auto] [@@rw]
 
(* Main theorem: insertion sort preserves elements *)
theorem insert_sort_elements a (x : int list) =
  num_occurs a x = num_occurs a (insert_sort x)
[@@by auto]

The rewrite lemmas insert_invariant, lemma_1, and lemma_2 are installed as [@@rw] rules. When auto processes the main theorems, the simplifier uses these rules automatically, and the waterfall handles the induction.

Philosophy

The waterfall embodies a key design principle:

Most useful theorems should be provable by simplification alone. Induction should only be applied as a last resort.

This is why the waterfall tries simplification first, then destructor elimination, fertilization, and generalization — all before resorting to induction. When induction is needed, the resulting subgoals re-enter the waterfall, where simplification usually finishes the job.

Previous← Induction
NextCounterexamples →