lean4#6544 : induction does not generalize instance argument

Stream: lean4

[Edward van de Meent]

in trying to write tests for my fix for lean4#4246, i've been repeatedly running into lean4#6544, so i decided to investigate, and it turns out that this is caused by the fact that docs#Lean.Meta.getFVarSetToGeneralize purposefully does not generalize instimplicit arguments. Can someone explain why this is?

[Edward van de Meent]

CC: @Leonardo de Moura who wrote this (4 years ago)?

[Edward van de Meent]

i imagine a fix might look like adding a second option argument for getFVarSetToGeneralize saying wether to ignore instance-implicit fvars, which is set to false in Lean.Elab.Tactic.generalizeVars (it's a private def) but true in docs#Lean.Meta.getFVarsToGeneralize

[Edward van de Meent]

update: this does run into issues...

[Edward van de Meent]

in particular, for some reason this causes the following to generate a goal Decidable P:

def casesTFOn {motive : Prop → Sort _} (P : Prop) [inst : Decidable P] : (T : motive True) → (F : motive False) → motive P :=
  λ ht hf => match inst with
  | isTrue H => eq_true H ▸ ht
  | isFalse H => eq_false H ▸ hf

example (P : Prop) [Decidable P] : ¬¬P → P := by
  induction P using casesTFOn
  admit
  admit

[Eric Wieser]

That's a bad induction principle

[Edward van de Meent]

(it's in the lean test suite)

[Eric Wieser]

I think it should be changed to

def casesTFOn {motive : (P : Prop) → [Decidable P] → Sort _} (P : Prop) [Decidable P] : (T : motive True) → (F : motive False) → motive P :=
  λ ht hf => match inst with
  | isTrue H => eq_true H ▸ ht
  | isFalse H => eq_false H ▸ hf

[Eric Wieser]

The test couldn't have been written that way before because it wasn't supported

[Edward van de Meent]

see for yourself

[Eric Wieser]

Yes, I'm saying that what you're proposing is a behavior change, and when you make such changes sometimes tests have to change

[Edward van de Meent]

the behaviour change i'm proposing shouldn't change this behaviour though? i think?

[Eric Wieser]

I would recommend you change the test as above and see if anything else breaks

[Eric Wieser]

Whether changing the test is ok can wait till review

[Edward van de Meent]

btw, i think the principle you're proposing here won't work, since the fix for lean4#6544 is separate from the fix for lean4#4246 , so lean will complain it can't figure out the implicit target

[Eric Wieser]

I think probably I'm claiming that the two things are morally the same bug

[Edward van de Meent]

(they're not)

[Eric Wieser]

My claim is that instance binders are not currently generalized because if they were, induction would not know how to populate them

[Edward van de Meent]

i think one of us is missing a key part here, in that as far as i can tell, lean4#4246 is about instance targets, not all instance arguments to induction

[Edward van de Meent]

also, the goal Decidable P strangely does not contain the instance that existed before

[Edward van de Meent]

so there is something really strange going on there

[Eric Wieser]

Edward van de Meent said:

also, the goal Decidable P strangely does not contain the instance that existed before

What's the full goal state after the induction line?

[Edward van de Meent]

with the following snippet:

def casesTFOn {motive : Prop → Sort _} (P : Prop) [inst : Decidable P] : (T : motive True) → (F : motive False) → motive P :=
  λ ht hf => match inst with
  | isTrue H => eq_true H ▸ ht
  | isFalse H => eq_false H ▸ hf

example (P : Prop) [Decidable P] : ¬¬P → P := by
  induction P using casesTFOn with
  | T => admit
  | F => admit
  admit

at the third admit:

case inst
P : Prop
⊢ Decidable P

[Edward van de Meent]

which is really weird to me

[Edward van de Meent]

time to dive into the induction implementation again, i guess

[Eric Wieser]

Just to check, does the alternative test I suggested pass?

[Edward van de Meent]

or actually, it makes sense? since the goal gets changed to [Decidable P] -> ¬¬P → P (because we're generalizing the instance), if you then try to use induction P using casesTFOn, you're indeed missing the needed instance

[Aaron Liu]

Edward van de Meent said:

with the following snippet:

def casesTFOn {motive : Prop → Sort _} (P : Prop) [inst : Decidable P] : (T : motive True) → (F : motive False) → motive P :=
  λ ht hf => match inst with
  | isTrue H => eq_true H ▸ ht
  | isFalse H => eq_false H ▸ hf

example (P : Prop) [Decidable P] : ¬¬P → P := by
  induction P using casesTFOn with
  | T => admit
  | F => admit
  admit

at the third admit:

case inst
P : Prop
⊢ Decidable P

On the web editor this gives me "no goals"

[Edward van de Meent]

yea, like i said, this is an issue on my branch where i try to fix lean4#6544

[Aaron Liu]

oh sorry didn't see

[Edward van de Meent]

Eric Wieser said:

Just to check, does the alternative test I suggested pass?

the alternative test you wrote doesn't compile the induction principle even on current lean

[Eric Wieser]

Oh, you should have told me sooner!

[Eric Wieser]

-- TODO: replace `(_ : Decidable P)` with `[Decidable P]`
def casesTFOn {motive : (P : Prop) → [Decidable P] → Sort _} (P : Prop) (_ : Decidable P) :
    (T : motive True) → (F : motive False) → motive P :=
  λ ht hf => match ‹Decidable P› with
  | isTrue H => cast (by simp [H]) ht
  | isFalse H => cast (by simp [H]) hf

example (P : Prop) [Decidable P] : ¬¬P → P := by
  induction P, ‹_› using casesTFOn
  admit
  admit

[Edward van de Meent]

yea, that works

[Eric Wieser]

Does it work on your branch with [] instead of (_ :)?

[Edward van de Meent]

no, failed to infer implicit target

[Eric Wieser]

Ok, same failure as head then

[Edward van de Meent]

anywho, i think that actually lean ideally should decide to not revert Decidable P here...

[Edward van de Meent]

the question is, what is a good decision procedure to decide if one should or shouldnt revert this? (btw, i'm guessing lean would have a similar issue with normal implicit arguments on current lean)

[Edward van de Meent]

let me see if i can throw together an example

[Edward van de Meent]

structure Foo ( P : Prop) [Decidable P] where

def casesTFOn {motive : (P : Prop) → Sort _} (P : Prop) {inst:Decidable P} (x: Foo P): (T : motive True) → (F : motive False) → motive P :=
  λ ht hf => match inst with
  | isTrue H => eq_true H ▸ ht
  | isFalse H => eq_false H ▸ hf

example (P) [Decidable P] : ¬¬P → P := by
  induction P using casesTFOn
  admit
  admit
  sorry

[Edward van de Meent]

i guess this is a result of the fact that these kinds of arguments are "extra": they're not major premises/targets, they're not minor premises, and they're not the motive...

[Jz Pan]

Edward van de Meent said:

in particular, for some reason this causes the following to generate a goal Decidable P:

I think this is not the intended behavior because the motive does not mention Decidable P...

[Aaron Liu]

I would say this is induction on Decidable P

[Aaron Liu]

But it's not mentioned in the motive

[Aaron Liu]

What's the criteria for determining the premises/targets?

[Edward van de Meent]

if you have an induction principle, match on the type it eliminates into; the head symbol is the motive; all other arguments to the motive in this type are the targets

[Edward van de Meent]

the minor premises are the arguments to the induction principle which eliminate into motive

[Edward van de Meent]

the major premises are the targets

[Aaron Liu]

Edward van de Meent said:

the minor premises are the arguments to the induction principle which eliminate into motive

Explain?

[Aaron Liu]

I've decided to read the code, so I can figure out this confusing behavior

[Edward van de Meent]

take the induction principle for Nat. it looks like natinduction : (motive : Nat -> Sort u) -> (zero : motive 0) -> (succ : ((n' : Nat) -> motive n' -> motive (n' + 1)) -> (n : Nat) -> motive n

[Aaron Liu]

So the motive is motive, and the targets are [n]

[Aaron Liu]

What are the major and minor premises?

[Edward van de Meent]

the principle eliminates into motive n. the head symbol is called the motive, motive. its arguments (just n in this case) are the major premises, which is another word for targets. the arguments zero and succ are the minor premises, since they eliminate into motive 0 and motive (n' + 1) respectively.

[Aaron Liu]

oh i get it now

[Aaron Liu]

The major premise is what you're inducting on and the minor premise is the induction cases

[Edward van de Meent]

so the question is: given some context + some goal, how do you determine what variables should become part of the motive (i.e. be reverted or generalized), and which variables shouldn't?

[Aaron Liu]

What's wrong with the way it's being done right now?

[Aaron Liu]

Edward van de Meent said:

anywho, i think that actually lean ideally should decide to not revert Decidable P here...

Can you give a before and after of what you want induction to do?

[Edward van de Meent]

the same as what it does on current lean, in this case

[Edward van de Meent]

but there are other cases where i do want lean to generalize a free variable, and i'm not sure yet what criterion to use to decide between these

[Aaron Liu]

Here's what I got on the current Lean.

Before:

case goal
P : Prop
inst✝ : Decidable P
⊢ ¬¬P → P

After:

case goal.T
P : Prop
inst✝ : Decidable P
⊢ ¬¬True → True

case goal.F
P : Prop
inst✝ : Decidable P
⊢ ¬¬False → False

case goal.inst
P : Prop
⊢ Decidable P

assignment

?goal :=
  @casesTFOn (fun P => ∀ {inst : Decidable P}, ¬¬P → P) P ?goal.inst
    (fun {inst} => ?goal.T) (fun {inst} => ?goal.F) inst✝

[Edward van de Meent]

ah wait, that's not right

[Edward van de Meent]

Edward van de Meent said:

in particular, for some reason this causes the following to generate a goal Decidable P:

def casesTFOn {motive : Prop → Sort _} (P : Prop) [inst : Decidable P] : (T : motive True) → (F : motive False) → motive P :=
  λ ht hf => match inst with
  | isTrue H => eq_true H ▸ ht
  | isFalse H => eq_false H ▸ hf

example (P : Prop) [Decidable P] : ¬¬P → P := by
  induction P using casesTFOn
  admit
  admit

for this, it should behave the same as on current lean

[Eric Wieser]

Maybe it helps to note that this fails on current lean:

def casesTFOn {motive : Prop → Sort _} (P : Prop) {inst : Decidable P} : (T : motive True) → (F : motive False) → motive P :=
  λ ht hf => match inst with
  | isTrue H => eq_true H ▸ ht
  | isFalse H => eq_false H ▸ hf

example (P : Prop) [Decidable P] : ¬¬P → P := by
  induction P using casesTFOn
  admit
  admit

[Eric Wieser]

So I really think casesTFOn is garbage

[Eric Wieser]

This also fails:

def casesTFOn {motive : Prop → Sort _} (P : Prop) [inst : Decidable P] : (T : motive True) → (F : motive False) → motive P :=
  λ ht hf => match inst with
  | isTrue H => eq_true H ▸ ht
  | isFalse H => eq_false H ▸ hf

example (P : Prop) [Decidable P] : (if P then 1 else 0) < 2 := by
  induction P using casesTFOn
  admit
  admit

[Aaron Liu]

It works if you add the Decidable P as a target

[Aaron Liu]

You might still get a failed to infer implicit target though

[Eric Wieser]

Do you mean like this?

[Edward van de Meent]

I think I have a solution: call arguments to an induction principle semitargets if their type depends on a target. Then, have all explicit targets and semitargets passed to induction. At the point where these would be reverted, instead do something which behaves like refine (?_ : semitargettype -> ?_) semitarget (but in the language of metaprogramming) such that the semitargets stay available to the current scope, but they also become available in the appropriate form when proving the minor premises.

[Edward van de Meent]

I'll try implementing this tomorrow

[Edward van de Meent]

(then generalizing any non-(semi)target will be blocked)

[Kyle Miller]

Maybe it's worth mentioning how @[elab_as_elim] works. It has similar considerations.

Here's how it handles things (see docs#Lean.Elab.Term.getElabElimExprInfo):

1. The "motive" is the head variable of the return type.
2. The "motive fvars" consist of all the variables that appear in the return type and (transitively) every variable that appears in the type of a motive fvar.
3. A "major argument" is any variable that's not the motive and either (1) it's a motive fvar or (2) its type contains a motive fvar and every application in the type is a constant application (it's a "first-order argument")
4. Then, every other argument is a "minor argument".

Then the elaborator takes the following steps:

1. The major arguments are all elaborated.
2. The motive is computed from the expected type.
3. The minor arguments are elaborated.

The purpose of all this is to be able to elaborate enough in (1) to be able to get enough information to successfully compute the motive in (2), before elaborating all the other arguments, which likely need a motive to be successful in (3).

Possibly it would have worked to simply say that the minor arguments are those whose types contain the motive variable.

The terminology doesn't line up with induction (for example every type parameter is a "major argument" according to @[elab_as_elim]), but maybe there's something useful to think about here

It's not clear to me that getFVarSetToGeneralize itself is the culprit (though, disclosure, I haven't investigated the issue). It might be that the way using clauses are elaborated needs rethinking. The handling of eliminators has undergone evolution over a number of years.

[Edward van de Meent]

how can a motive fvar not occur as argument to the motive though??

[Edward van de Meent]

i don't see what kind of motive could have that...

[Kyle Miller]

When there's an argument that appears in the type of an argument that appears in the return type.

[Edward van de Meent]

so the principle can be something like (a:A) -> (motive : b a -> Sort) -> (x: b a) -> motive x?

[Edward van de Meent]

i guess that makes sense

[Kyle Miller]

Sure, that would make a be a "major argument" for @[elab_as_elim].

This is also possible: (a:A) -> (motive : (a' : A) -> b a' -> Sort) -> (x: b a) -> motive x. It too will include a as something that needs to be elaborated before computing the motive.

[Kyle Miller]

The motivation is that to be able to find all x's in the expected type you should elaborate x, but to elaborate x, you should know its type, so you should elaborate a.

[Edward van de Meent]

the a from my example would be a "motive fvar" too, right?

[Kyle Miller]

Yes, both in your example and mine.

[Edward van de Meent]

the key difference is that in my example it is only because of the transitive considerations

[Kyle Miller]

In yours its for two reasons: it appears in the type of x which appears in the return type, and because it appears in the motive argument's type.

[Kyle Miller]

In mine it's only for the first reason. (Both reasons are due to transitivity.)

[Edward van de Meent]

your example seems to be missing an argument to the final motive

[Kyle Miller]

Oh yeah, you're right. That's a simple case then, no transitivity.

[Jz Pan]

Edward van de Meent said:

so the principle can be something like (a:A) -> (motive : b a -> Sort) -> (x: b a) -> motive x?

I think for this case you can only induction on x and a is always fixed. If user want to do induction on a it should throws an error.

[Aaron Liu]

Jz Pan said:

Edward van de Meent said:

so the principle can be something like (a:A) -> (motive : b a -> Sort) -> (x: b a) -> motive x?

I think for this case you can only induction on x and a is always fixed. If user want to do induction on a it should throws an error.

This is actually really common. Take for example docs#Finset.induction, that starts with

{α : Type*} {motive : Finset α → Prop}

which fits the pattern described above.

[Edward van de Meent]

yea, that's fair. i also realised the same for List.rec and similar

[Jz Pan]

Aaron Liu said:

Jz Pan said:

Edward van de Meent said:

so the principle can be something like (a:A) -> (motive : b a -> Sort) -> (x: b a) -> motive x?

I think for this case you can only induction on x and a is always fixed. If user want to do induction on a it should throws an error.

This is actually really common. Take for example docs#Finset.induction, that starts with

{α : Type*} {motive : Finset α → Prop}

which fits the pattern described above.

In that case the α is fixed and cannot be changed during the proof of Finset.induction, since the α is not appeared as an input of motive. Like (a:A) -> (motive : b a -> Sort) -> (x: b a) -> motive x you cannot vary a during the proof, since a is not appeared as an input of motive. If you want to vary a you must use (a:A) -> (motive : (a' : A) -> b a' -> Sort) -> (x: b a) -> motive x. The compiler should not implicitly prepend an a' : A to the motive for the former case.

[Edward van de Meent]

you mean (a:A) -> (motive : (a' : A) -> b a' -> Sort) -> (x: b a) -> motive a x in that second case, right?

[Jz Pan]

Edward van de Meent said:

you mean (a:A) -> (motive : (a' : A) -> b a' -> Sort) -> (x: b a) -> motive a x in that second case, right?

Yes, I mean only in this case you can vary a in the motive. For (a:A) -> (motive : b a -> Sort) -> (x: b a) -> motive x the induction should always generate goals for the fixed a.

[Edward van de Meent]

or, well, as much as the value of motive depends on it

[Jz Pan]

Although the value b a of motive depends on a, but a does not appear as an input of motive which means that the a in motive is fixed and can never be changed... Just like thinking motive as a closure (a is in the closure) function which has only one argument, instead of a function taking two arguments.

[Jz Pan]

As an example here #mathlib4 > How to write induction principle for modules @ 💬 although some properties for M depends on A, but when I write motive in that way I mean the A is always fixed as the input A in the induction principle theorem, and can never be changed; I don't want induction principle generates goals with varying A.