RFC: WF proofs should add match lemmas to context

Stream: lean4

[Jakub Nowak]

In the example below _ : has to be manually added to match for termination checker to succeed. Should we include match and ifs lemmas in the context? This would be useful for termination proofs that are dispatched automatically. When explicit proofs is passed though, this would result in adding some unnamed hypotheses to the context. There is already a precedence, fun_induction does that. Although, the important difference is that it might be impossible to change the definition when using fun_induction, while with termination proof one can always change the definition and explicitly name match lemmas. We could choose to only add match lemmas when no explicit proof term is present.

structure Foo where
  n : Nat

@[simp]
instance : SizeOf Foo where
  sizeOf | ⟨n⟩ => n

/--
error: fail to show termination for
  func
with errors
failed to infer structural recursion:
Cannot use parameter x:
  the type Foo does not have a `.brecOn` recursor


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
x : Foo
n : Nat
⊢ n < x.n
-/
#guard_msgs in
def func (x : Foo) : Nat :=
  match x.n with
  | 0 => 0
  | n + 1 =>
    func ⟨n⟩

def func' (x : Foo) : Nat :=
  match _ : x.n with
  | 0 => 0
  | n + 1 =>
    func' ⟨n⟩

[Mirek Olšák]

Absolutely agree, I had a similar RFC a while ago, without much attention so far: https://github.com/leanprover/lean4/issues/10977#issuecomment-3517049923

[Mirek Olšák]

I think the situation is similar to handling if. In the case of if, the lemmas are not seen in the context on their own, but are captured by decreasing_by. I don't see a reason why match should work differently.

[Jakub Nowak]

Looks like if lemmas also aren't included:
nvm, that example was wrong

[Henrik Böving]

They aren't included automatically because whether you want to include them or not changes the whole elaboration process. the h : isn't just an anotation, it makes the difference between using ite or dite, similarly the h : in match tells the match elaborator to do a completely different thing.

[Mirek Olšák]

Interesting, apparently this is some corner-case where it is not captured. Usually, it is

def func (x : Nat) : Nat :=
  if x > 5 ∧ x < 3 then
    func (x+1)
  else
    0

[Mirek Olšák]

Henrik Böving said:

They aren't included automatically because whether you want to include them or not changes the whole elaboration process. the h : isn't just an anotation, it makes the difference between using ite or dite, similarly the h : in match tells the match elaborator to do a completely different thing.

As far as I understand, ite gets replaced with dite if needed for termination (as in my func example)

[Jakub Nowak]

Henrik Böving said:

They aren't included automatically because whether you want to include them or not changes the whole elaboration process. the h : isn't just an anotation, it makes the difference between using ite or dite, similarly the h : in match tells the match elaborator to do a completely different thing.

Why is it a problem to always use dite?

[Jakub Nowak]

And anyway, we don't have to change ite do dite in the body of a function. We can e.g. rewrite using ite_eq_dite inside termination checker. Or do the same thing that fun_induction is doing.

[Jakub Nowak]

Actually, what you said would suggest, that we should make it possible to use match lemmas inside explicit decreasing_by proof without being forced to change ite do dite. Because currently that's the only option (apart from using recursors manually), even though it could be avoided.

[Aaron Liu]

Jakub Nowak said:

Actually, your comment would suggest, that we should make it possible to use match lemmas inside explicit decreasing_by proof without being forced to change ite do dite. Because currently that's the only option (apart from using recursors manually), even though it could be avoided.

Sorry, I don't quite understand what you are suggesting here

[Jakub Nowak]

Which part?

[Aaron Liu]

how would this happen?

[Jakub Nowak]

Hmm, I see, you're right. This is quite different from fun_induction which operates on existing definition. The match lemma is required to make a recursive call inside recursor, so modifying body of the definition is necessary. Sorry, I did not grasp that before.

[Mirek Olšák]

My suggestion is to make decreasing_by work with match work the same way as with if. I don't fully understand the details, but can see that it automatically performs the change for the dependent variant.

[Aaron Liu]

With if it's a lot simpler because it's a single definition docs#ite being changed to docs#dite

[Aaron Liu]

but match generates new matchers every time you create another match that doesn't match anything earlier in that file

[Aaron Liu]

the lemma for if is docs#ite_eq_dite, you can see it's tagged @[wf_preprocess]

[Jakub Nowak]

Can't match just always generate dependant matcher?

[Aaron Liu]

same reason we have both ite and dite

[Jakub Nowak]

Which is?

[Aaron Liu]

I think it's because it would clutter your context with unnecessary hypotheses

[Jakub Nowak]

We could strip them in delabolator.

[Jakub Nowak]

That would require analyzing expression for whether the hypothesis is used or not, but it's possible.

[Jakub Nowak]

Hmm, and I guess tactic like split would also have to do this analysis to know whether to introduce the hypothesis or not.

[Jakub Nowak]

Nvm, looks like a bad idea. .-.

[Jakub Nowak]

So, it's not possible to change non-dependant match to dependant one with wf_preprocessor?

[Aaron Liu]

Jakub Nowak said:

We could strip them in delabolator.

What about the infoview?

[Robin Arnez]

You could also add the proof to the motive; but that would be a propositional rewrite; I guess you could squeeze it as a simproc into wf_preprocess though?

def test (n : Nat) : Nat :=
  match n with
  | 0 => n
  | k + 1 => k - 3

theorem test.match_1.attach (motive : Nat → Sort u_1) (n : Nat) (h_1 : Unit → motive 0)
    (h_2 : (k : Nat) → motive k.succ) :
    test.match_1 motive n h_1 h_2 =
      test.match_1 (fun m => n = m → motive m) n (fun a _ => h_1 a) (fun k _ => h_2 k) rfl := by
  refine test.match_1.splitter (fun n =>
    test.match_1 motive n h_1 h_2 =
      test.match_1 (fun m => n = m → motive m) n (fun a _ => h_1 a) (fun k _ => h_2 k) rfl) n ?_ ?_
  · intro a
    refine Eq.rec ?_ (test.match_1.eq_1 motive h_1 h_2).symm
    refine Eq.rec ?_ (test.match_1.eq_1 (fun m => 0 = m → motive m) (fun a _ => h_1 a) (fun k _ => h_2 k)).symm
    rfl
  · intro k
    refine Eq.rec ?_ (test.match_1.eq_2 motive k h_1 h_2).symm
    refine Eq.rec ?_ (test.match_1.eq_2 (fun m => k + 1 = m → motive m) k (fun a _ => h_1 a) (fun k _ => h_2 k)).symm
    rfl

example (n : Nat) : test n = sorry := by
  unfold test
  rw [test.match_1.attach]
  conv =>
    enter [1, 3, a, ha]; rw [ha]
  rw [← test.match_1.attach]
  sorry