No functional induction on List.merge

Stream: lean4

[Shreyas Srinivas]

It seems fun_induction List.merge doesn't work. It throws the error : `No functional induction theorem for List.merge, or function is mutually recursive

[Shreyas Srinivas]

#check List.merge.induct throws an unknown identifier error. However I can immediately get the lemma if I copy-paste the definition into my file

[Shreyas Srinivas]

How do I get fun_induction working on List.merge?

[Aaron Liu]

this works in the web editor

/--
info: List.merge.induct.{u_1} {α : Type u_1} (le : α → α → Bool) (motive : List α → List α → Prop)
  (case1 : ∀ (ys : List α), motive [] ys) (case2 : ∀ (xs : List α), (xs = [] → False) → motive xs [])
  (case3 :
    ∀ (x : α) (xs : List α) (y : α) (ys : List α), le x y = true → motive xs (y :: ys) → motive (x :: xs) (y :: ys))
  (case4 :
    ∀ (x : α) (xs : List α) (y : α) (ys : List α), ¬le x y = true → motive (x :: xs) ys → motive (x :: xs) (y :: ys))
  (xs ys : List α) : motive xs ys
-/
#guard_msgs in
#check List.merge.induct

[Shreyas Srinivas]

I get an error in cslib#275

[Shreyas Srinivas]

Is this because of some module system thing?

[Aaron Liu]

the contents of List.merge isn't exposed

[Shreyas Srinivas]

I just need fun_induction List.merge to work

[Aaron Liu]

so if you're in a module that doesn't have access to the contents of List.merge then it will appear like an axiom to any tactics

[Aaron Liu]

module

/-- error: Unknown constant `List.merge.induct` -/
#guard_msgs in
#check List.merge.induct

[Shreyas Srinivas]

@Eric Wieser and @Chris Henson

[Shreyas Srinivas]

It's a module system issue. Core is setup to not allow us to access List.merge by default

[Shreyas Srinivas]

How do I bring it in scope?

[Aaron Liu]

you can import all Init.Data.List.Sort.Basic

[Edward van de Meent]

It would be nice if the lemma is generated either way, though...

[Edward van de Meent]

Or, if it were as available as its type

[Shreyas Srinivas]

I think the lemma gets generated and is just hidden by the module system

[Henrik Böving]

Given that the lemma for functional induction is in essence a complete description of the function body having it exposed for a non exposed function would kind of defeat the whole point of the module system. The lemma would change on basically any modification to the function body that would be made which is akin to just putting @[expose] on the definition.

[Shreyas Srinivas]

Then we should probably just import all everything in core downstream in CSLib if we want to prove stuff about basic definitions. This sounds like pushing the module system rules to an extreme

[Kim Morrison]

What theorems are you missing?

[Shreyas Srinivas]

Being able to use fun_induction to prove that my monadic program evaluates identically to List.merge

[Shreyas Srinivas]

And then use this equality for any theorem about the evaluation of the program.

[Shreyas Srinivas]

This is a concrete example : https://github.com/leanprover/cslib/pull/275/changes#diff-f5c3e3be8e076ae58f336c517a22edece9330a5f7f33820be47324c3137c3ad4R68

[Shreyas Srinivas]

But essentially I advocate this strategy for all algorithms in upstream libraries, where the recursive structure matches that of the algorithm. It simplifies correctness proofs immensely.

[Eric Wieser]

I guess the argument could be made that while the generated induction lemma is an implementation detail, an induction principle that shows the API lemmas are exhaustive should also itself be part of the API

[Sebastian Ullrich]

And using the fun induction principle of your local merge doesn't work? I haven't tried

[Eric Wieser]

In this particular case the local merge has a weaker fun_induction principle that requires some extra manual case splitting (due to the branch condition being abstracted out); though not enough to be a major concern

[Joachim Breitner]

Another workaround is to have your own copy of List.merge (or even a function returning Unit with the same branching and recursive call), and use that function’s induction principle. I will be the identical to that of List.merge. (Ok, granted, that trick does not work if you want to use the unfolding functional induction principle.)

[Shreyas Srinivas]

I already tried that. But it is duplication of code in a downstream library then. So it cannot pass review.

[Shreyas Srinivas]

Broadly : There might be a case to be made for allowing localised replication of non-exported definitions. This is especially the case when the local copy and upstream copy have orthogonal purposes which might clash at some point. Even though it means more code to fix when a breaking change happens, the errors are localised and decoupled from each other. So core can change List.merge as it likes for its intended uses (maybe it is meant to be efficient). It wouldn’t affect other use cases. Localising errors and keeping code stable over upstream changes can be good enough reasons to duplicate non-exposed defs (maybe as private) which have different primary purposes. For example, if List.merge hypothetically had a different recursion structure tomorrow for performance reasons, this could cause a severe breakage in our use case, which is to simplify correctness proofs. And indeed the module system setup for this file clearly intends to discourage such uses.

But that’s a discussion that is almost certainly not going to affect this PR.