RFC: Overlapping matches and termination proofs

The issue

A user might expect to be able to write this function, and be able to proof it terminating (or even have the default decreasing_tactic prove it terminating):

def foo : Nat → Nat
  | 0 => 0
  | n => foo (n - 1)
termination_by foo n => n
decreasing_by …

Alas, that does not work: As it stands, in the context of the recursive call, we no longer know that n ≠ 0. If we knew that, we could proceed:

def foo : Nat → Nat
  | 0 => 0
  | n =>
    have h : n ≠ 0 := sorry
    foo (n - 1)
termination_by foo n => n
decreasing_by
  · simp_wf
    apply Nat.sub_lt
    apply Nat.zero_lt_of_ne_zero h
    apply Nat.zero_lt_one

We could

• live with the status quo, requiring the user to rewrite the second case as n+1
• provide this assumption automatically in the termination proof
• provide syntax to add this assumption manually

I am not yet proposing one of these (and maybe there are more options); opening this RFC to have a place to note down these thoughts and discuss.

Approach 1: Status quo

We can leave things as they are, of course.

In this case not bad (n+1 doesn’t hurt, and Nat.sub isn’t great anyways), but can be quite bad in other cases (imagine many constructors, and only one is excluded).

Approach 2: Automatic hypotheses

I believe we can automatically add these assumptions. Internally, the function is represented as

def foo : Nat → Nat :=
WellFounded.fix foo.proof_1 fun a a_1 =>
  foo.match_1 (fun x => ((y : Nat) → (invImage (fun a => a) instWellFoundedRelation).1 y x → Nat) → Nat) a
    (fun a x => 0) (fun n x => x (n - 1) _) a_1

with

foo.match_1.{u_1} (motive : Nat → Sort u_1) (x✝ : Nat) (h_1 : Unit → motive 0) (h_2 : (n : Nat) → motive n) : motive x✝

Along this matcher function, Lean generates a “splitter”, which is essentially the same, but with extra hypotheses:

foo.match_1.splitter.{u_1} (motive : Nat → Sort u_1) (x✝ : Nat) (h_1 : motive 0)
  (h_2 : (n : Nat) → (n = 0 → False) → motive n) : motive x✝

It should be possible replace foo.match_1 with foo.match_1.splitter (just like we replace ite with dite here) and thus get the right assumptions into scope for the termination proof obligations, without affecting much else (the user only sees the foo._eq_N and foo._unfold lemmas, which would be unchanged).

The extra assumption would have an inaccessible name, so there is a usability problem in manual termination proofs.

Implementation-wise the part that proves foo.unfold would probably learn to relate a matcher application with an application of that matcher’s splitter, or maybe it suffices to define equations for the splitter, analogously to those for the matcher.

Approach 3: Explicit hypotheses

Instead of bringing these hypotheses into scope implicitly and automatically just for the termination proof, we could plausible invent a surface syntax, for example

def foo : Nat → Nat
  h0 : | 0 => 0
       | n => foo (n - 1)

which adds h0 : n ≠ 0 to all (overlapped) cases.

This may be useful independently of termination proofs, e.g. when the RHS has dependent terms where you need the extra information. This RFC isn’t the place to hash out details of such syntax (of which I am sure are many); the question here is mostly: In case we decide we want explicit hypotheses, would we still want to pursue the implicit approach in addition.

Tangent: Inductive principles from function definitions

This discussion touches upon the goal of having inductive principles from function definitions. My little naive experimental implementation produces

foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive (n - 1) → motive n) (x : Nat) :
  motive x

but that isn’t great, because this doesn't work as it should:

theorem foo_eq_0 (n : Nat) : foo n = 0 := by
  induction n using foo.induct with
  | case1 => simp [foo]
  | case2 n IH => 
      simp [foo] -- does not make progress without `n ≠ 0`
      exact IH

The induction principle we would want is

axiom foo.induct_better (motive : Nat → Prop) (case1 : motive 0)
  (case2 : ∀ (n : Nat), n ≠ 0 → motive (n - 1) → motive n) (x : Nat) : motive x

where in each case, simp [foo] successfully apply one of foo’s equations:

theorem foo_eq_0 (n : Nat) : foo n = 0 := by
  induction n using foo.induct_better with
  | case1 => simp [foo]
  | case2 n h0 IH => simp [foo]; exact IH

If we go via approach 2, then these assumptions are already present in foo’s definition and could be picked up there by the code that creates the induction.

If we go via approach 1 or 3, then that code has to deal with splitting.

Update: The FunInd code in #3432 now adds the necessary splits.

Community Feedback

(None yet.)

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start with src/Lean/Elab/PreDefinition/WF/Main.lean, especially the matcher/splitter handling referenced near the ite/dite replacement, and review the FunInd work in #3432. Compare the automatic and explicit-hypothesis approaches described in the RFC; done means an agreed design and implementation plan for overlapping-match hypotheses and their effect on termination and induction proofs.