RFC: Overlapping matches and termination proofs

nomeata commented 10 months ago

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 :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

digama0 commented 10 months ago

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

Regarding this point, have you tried this in more complex cases? If case1 has several arguments, the hypothesis from the match splitter and in the equation lemma is something like \forall a b, n = case1 a b -> False and simp is not really able to use this as a hypothesis for the conditional rewrite because it gets lost in the structure of the hypothesis and/or tries to simplify something in it.

nomeata commented 10 months ago

Thanks for the heads-up! No, I haven't yet. Should the idiom be rwa [foo] then, rather than simp [foo] (Probably safer anyways if the goal is to unfold once)? Or how else to unfold a complex function definition with overlapping cases?

leanprover / lean4