fun_induction for mutually recursive functions?

Stream: new members

[aron]

I'm trying to use fun_induction on mutually inductive functions but apparently that isn't supported?

No functional induction theorem for `decEq`, or function is mutually recursive

Is there a different way to prove theorems about mutually recursive functions or what do I do here?

[David Thrane Christiansen]

Typically you would write two theorems in a mutual block that explicitly refer to each other recursively. Example:

mutual
def add (n k : Nat) : Nat :=
  if n = 0 then k else add' (n-1) k
def add' (n k : Nat) : Nat :=
  1 + add n k
end

mutual
theorem add_correct : add n k = n + k :=
  match n with
  | 0 => by simp [add]
  | n' + 1 => by
    rw [add, add'_correct]
    grind

theorem add'_correct : add' n k = 1 + n + k := by
  simp [add']
  rw [add_correct]
  grind
end

You have to be a bit careful when working this way, because some tactics generate terms that the well-founded recursion system won't recognize easily.

Adding termination_by? clauses to the definitions and theorems can be a nice way to see what's going on.