The equation compiler and WellFoundedRelation #

To define functions and proofs recursively you can use the equation compiler, if you have a well founded relation on that type

For example the definition of gcd on naturals uses well founded recursion

def gcd (m n : Nat) : Nat :=
  if m = 0 then
    n
  else
    gcd (n % m) m
  termination_by m
  decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption

Because < is a well founded relation on naturals, and because ¬m = 0 → n % m < m this recursive function is well-founded.

Whenever you use the equation compiler, there will be a default well founded relation on the type being recursed on (given by the WellFoundedRelation instance) and the equation compiler will automatically attempt to prove the function is well founded under said relation.

When the equation compiler fails, there are two main causes.

  1. It could not find a decreasing measure.
  2. It has failed to prove the required inequality.

Proving required inequality #

If we modify the gcd example above, by removing the termination_by & decreasing_by, we get an error.

def gcd (m n : Nat) : Nat :=
  if m = 0 then
    n
  else
    gcd (n % m) m

fail to show termination for
  Nat.gcd
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    (n % m).gcd m

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    (n % m).gcd m

structural recursion cannot be used

Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
           m n
1) 93:4-18 ? ?
Please use `termination_by` to specify a decreasing measure.

The error message says us to use termination_by to specify decreasing measure, so we use m as a decreasing measure, but we get an another error.

def gcd (m n : Nat) : Nat :=
  if m = 0 then
    n
  else
    gcd (n % m) m
  termination_by m

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
m n : ℕ
h✝ : ¬m = 0
⊢ n % m < m

We specified the correct decreasing measure, so our options are to use have-expressions or to use decreasing_by. Here, we use decreasing_by tactics to prove the termination of this function. At the first, let's placeholder by sorry to show the goal.

def gcd (m n : Nat) : Nat :=
  if m = 0 then
    n
  else
    gcd (n % m) m
  termination_by m
  decreasing_by sorry

m n : ℕ
h✝ : ¬m = 0
⊢ (invImage (fun x ↦ PSigma.casesOn x fun m n ↦ m) instWellFoundedRelationOfSizeOf).1 ⟨n % m, m⟩ ⟨m, n⟩

This goal is compiler-generated so difficult to read, so we simplify the goal with simp_wf.

def gcd (m n : Nat) : Nat :=
  if m = 0 then
    n
  else
    gcd (n % m) m
  termination_by m
  decreasing_by simp_wf; sorry

m n : ℕ
h✝ : ¬m = 0
⊢ n % m < m

By the way, where the hypothesis h✝ : ¬m = 0 come from? Indeed, during a proof of termination, if p then t else f is rewritten into if h : p then t else f, so the hypothesis p becomes available.

The remained task is only to prove this goal:

def gcd (m n : Nat) : Nat :=
  if m = 0 then
    n
  else
    gcd (n % m) m
  termination_by m
  decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption

For your information, if we use the option to use have-expressions, the function is the following form:

def gcd (m n : Nat) : Nat :=
  if h : m = 0 then
    n
  else
    have := mod_lt n (zero_lt_of_ne_zero h)
    gcd (n % m) m

But the have-expressions may be an obstacle when we use the equation lemma.

Another example is the following function in Data.Multiset.Basic.

def strongInductionOn {p : Multiset α → Sort*} (s : Multiset α) (ih : ∀ s, (∀ t < s, p t) → p s) :
    p s :=
    (ih s) fun t _h =>
      strongInductionOn t ih
termination_by card s
decreasing_by exact card_lt_card _h

This example uses card s as a decreasing measure instead of the argument itself.

WellFoundedRelation instance #

We can specify not only an Nat value but also any types with WellFoundedRelation as a decreasing measure, as you can see in Data.List.Defs:

def permutationsAux.rec {C : List α → List α → Sort v} (H0 : ∀ is, C [] is)
    (H1 : ∀ t ts is, C ts (t :: is) → C is [] → C (t :: ts) is) : ∀ l₁ l₂, C l₁ l₂
  | [], is => H0 is
  | t :: ts, is =>
      H1 t ts is (permutationsAux.rec H0 H1 ts (t :: is)) (permutationsAux.rec H0 H1 is [])
  termination_by ts is => (length ts + length is, length ts)
  decreasing_by all_goals (simp_wf; omega)

This example uses an Nat × Nat value as a decreasing measure. The WellFoundedRelation on this type is a lexicographical order on natural numbers, defined by the following instance in Init.WF:

instance [ha : WellFoundedRelation α] [hb : WellFoundedRelation β] : WellFoundedRelation (α × β) :=
  lex ha hb