bug in revert

Stream: mathlib4

[Jireh Loreaux]

I think there's a bug in revert:

import Mathlib.Data.Fintype.Card

example {E n : Type*} [Fintype n] {T : n → E} : ∀ j, T j = T j := by
  revert T
  have : True := trivial -- comment this line to break the proof *and* the statement elaboration
  refine Fintype.induction_subsingleton_or_nontrivial n ?base ?step
  case base => intros; rfl
  case step => intros; rfl

[Jireh Loreaux]

With set_option pp.raw true, before the have the goal state is:

forall {T : _uniq.23 -> _uniq.22} (j : _uniq.23), Eq.{succ u_1} _uniq.22 (T j) (T j)

and after it is:

[mdata noImplicitLambda:1 forall {T : _uniq.23 -> _uniq.22} (j : _uniq.23), Eq.{succ u_1} _uniq.22 (T j) (T j)]

[Jireh Loreaux]

I've posted this in the Mathlib stream instead of lean4 because I haven't been able to minimize away the particular induction lemma used, and so I'm not sure it's a problem with revert.

[Thomas Murrills]

Some minimization:

import Lean

@[elab_as_elim]
def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry

example {n : Type} : ∀ {T : n}, T = T := by
  have : True := trivial -- comment this line to break the proof
  exact Foo.induction n

[Thomas Murrills]

It seems like elab_as_elim is essential here; the proof breaks completely either way without it.

(Though interestingly, without @[elab_as_elim] the error reporting location still changes depending on whether the no_implicit_lambda mdata is present! It makes sense that the error itself is different, but I'm surprised the location is different too, given that they're both type mismatches on Foo.induction n. Maybe mdata isn't handled correctly when reporting (these) errors?)

[Jireh Loreaux]

Do you mind posting this in the lean 4 stream?

[Floris van Doorn]

and/or open an issue in the lean4 repository

[Jireh Loreaux]

Note that providing the motive explicitly works though (even with by exact). Maybe this is unsurprising, but I felt it was worth noting.

import Lean

@[elab_as_elim]
def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry

example {n : Type} : ∀ {T : n}, T = T := by
  have : True := trivial -- comment this line to break the proof
  exact Foo.induction n

example {n : Type} : ∀ {T : n}, T = T :=
  @Foo.induction (fun n : Type => ∀ {T : n}, T = T) n

[Thomas Murrills]

Ah, sorry, short on time right now; maybe someone with the power to do so could move this entire thread to lean4 though?

[Thomas Murrills]

Note though that providing the motive explicitly actually reverses the behavior wrt no_implicit_lambda!

example {n : Type} : ∀ {T : n}, T = T := by
  -- have : True := trivial -- *un*comment this line to break the proof
  exact Foo.induction (P := fun n : Type => ∀ {T : n}, T = T) n

[Kyle Miller]

The implicit lambda feature seems like it might be a red herring (edit: not exactly, it's related, but there's still another bug). This causes a typechecking bug on each example:

@[elab_as_elim]
def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry

example {n : Type} {T : n} : T = T := by
  exact Foo.induction n

example {n : Type} {T : n} : T = T := Foo.induction n

[Kyle Miller]

This seems to be a failure to have elabAsElim report "motive not type correct" here. This is what it's trying to pass off as a valid term:

example {n : Type} {T : n} : T = T := @Foo.induction (fun x ↦ @Eq x T T) n

[Jireh Loreaux]

That doesn't explain why the have fixes computing the motive.

[Kyle Miller]

That's true, but it does mostly explain why there's an error on example rather than on exact

[Kyle Miller]

The reason why have fixes it does turn out to be the implicit lambda feature. It's simply that the motive can only be type correct if you don't introduce the T argument first. Both of these work:

example {n : Type} : {T : n} → T = T := no_implicit_lambda% (Foo.induction n)
example {n : Type} : (T : n) → T = T := Foo.induction n

[Kyle Miller]

Here's a workaround for your original example:

import Mathlib.Data.Fintype.Card

example {E n : Type*} [Fintype n] {T : n → E} : ∀ j, T j = T j := by
  revert T
  change ∀ T, _ -- changes binder type from implicit to explicit
  refine Fintype.induction_subsingleton_or_nontrivial n ?base ?step
  case base => intros; rfl
  case step => intros; rfl

[Kyle Miller]

It seems worth filing an issue that revert doesn't give you a way to change binders from implicit to explicit and it interacts badly with the implicit lambda feature.

[Kyle Miller]

I would have suggested using the induction tactic here, but that doesn't seem to work when n is a type like this.

[Eric Wieser]

I think there is an issue somewhere about induction not working for docs#Fintype.induction_subsingleton_or_nontrivial ?

[Eric Wieser]

The issue is the implicit arguments I believe, not the type

[Eric Wieser]

Here is the thread

[Eric Wieser]

lean4#4246

[Thomas Murrills]

Why do (or maybe a better question, why should) some tactics, like have, wind up with no_implicit_lambda on the goal, and some don’t? It’s hard to see the rhyme and reason.

[Thomas Murrills]

Is it essentially just leftover from its role as a necessary internal flag?

[Kyle Miller]

lean4#4722 has the elabAsElim fixes, which make Foo.induction fail in the right place.

[Thomas Murrills]

And more generally: should no_implicit_lambda ever appear on a user-facing goal? (Or should it effectively always appear on the goal?)

I’m just wondering if it’s reasonable to have something that invisibly changes behavior appear inconsistently like that.

[Kyle Miller]

I think for have the point is to make sure that have doesn't also do an intro for implicits that happen to be there.

[Kyle Miller]

I've been thinking that it might make more sense if the implicit lambda feature is activated at by and then disabled in some consistent way from then on...

[Kyle Miller]

Here's another workaround @Jireh Loreaux, I forgot about this notation:

example {E n : Type*} [Fintype n] {T : n → E} : ∀ j, T j = T j := by
  revert T
  refine @(Fintype.induction_subsingleton_or_nontrivial n ?base ?step)
  case base => intros; rfl
  case step => intros; rfl

[Jireh Loreaux]

I'm not sure what that new @ notation means

[Kyle Miller]

@(e) means "disable implicit lambda feature when elaborating e"