!4#2894

Stream: mathlib4

[Jeremy Tan]

!4#2894 The mathlib3 code for the last function here works almost perfectly after correcting names. The exception is that Lean 4 cannot infer the instance CharP R p for the last few lines despite it already being encoded as a hypothesis hp (Lean 3 can). How can I "extract" the instance from the hypothesis?

theorem expChar_is_prime_or_one (q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q = 1 :=
  or_iff_not_imp_right.mpr fun h => by
    cases' CharP.exists R with p hp
    -- ...
    have p_eq_q : p = q := (char_eq_expChar_iff R p q).mpr (char_prime_of_ne_zero R p_ne_zero)
    cases' CharP.char_is_prime_or_zero R p with pprime
    · rwa [p_eq_q] at pprime
    · contradiction

I have provisionally included CharP R p up top as an explicit instance to illustrate my point

[Jeremy Tan]

Trying to apply what I learned from !4#2813

[Eric Wieser]

I would guess etaExperiment might be relevant here

[Jeremy Tan]

Eric Wieser said:

I would guess etaExperiment might be relevant here

tried that, doesn't change anything, still errors out

[Oliver Nash]

Thanks for working on this. I just had a quick look and I think the issue was that we don't have casesI (yet?). I pushed a commit which I believe should fix the build.

[Eric Wieser]

Am I imagining that Lean 4 did away with the instance cache and that therefore casesI isn't needed?

[Jeremy Tan]

Oliver Nash said:

Thanks for working on this. I just had a quick look and I think the issue was that we don't have casesI (yet?). I pushed a commit which I believe should fix the build.

oh, I didn't know haveI existed in Lean 4 at all, thanks

[Yaël Dillies]

Lean 4's haveI does not mean the same thing as Lean 3's haveI

[Mario Carneiro]

Eric Wieser said:

Am I imagining that Lean 4 did away with the instance cache and that therefore casesI isn't needed?

Yes to the second part, no to the first. Lean 4 didn't do away with the instance cache, it now effectively calls resetI whenever the local context changes at all. Some internals had to be changed to make this performant enough

[Eric Wieser]

Yaël Dillies said:

Lean 4's haveI does not mean the same thing as Lean 3's haveI

Can you elaborate on this?

[Ruben Van de Velde]

It's now "I" for "inline" rather than "instance cache". I still don't know what that means in practice

[Notification Bot]

12 messages were moved from this topic to #mathlib4 > tactic documentation by Eric Wieser.

[Mario Carneiro]

The difference is that have x : Nat := 0; exact Nat.succ x expands to (fun x => Nat.succ x) 0 while haveI x : Nat := 0; exact Nat.succ x expands to Nat.succ 0

[Kevin Buzzard]

so lean 3 tactic let is lean 4 have? I hadn't realised this.

[Kevin Buzzard]

@Oliver Nash it seems that have : CharP R p := hp also works! I find this quite bizarre -- the claim seems to be that now Lean 4 doesn't need lean 3 haveI because the cache is reset, but the PR in its broken state before you inserted the haveI line seems to be an explicit counterexample to this. We have hp explicitly in the local context and the have line just adds it a second time, which magically fixes all the problems. This looks to me like a bug in the instance cache generation system?

[Mario Carneiro]

Kevin Buzzard said:

so lean 3 tactic let is lean 4 have? I hadn't realised this.

No, let and have are still different and the distinction is the same as in lean 3

[Mario Carneiro]

the only difference with haveI is the resulting term after elaboration. You still cannot make use of a defeq x = 0 after haveI x := 0

[Mario Carneiro]

The behavior you describe sounds like an instability in the instance search mechanism, e.g. putting it last makes it take a different path

[Eric Rodriguez]

Kevin Buzzard said:

so lean 3 tactic let is lean 4 have? I hadn't realised this.

I think the confounding thing is that there's two different haves in Lean3 - have in tactic mode, iirc, does just do the inlining process that Lean4 haveI does. However, there's a _term-mode_ have which is different, and is like lean4's have tactic.

[Kyle Miller]

Huh, I'd never realized this about Lean 3's have tactic. I'd always thought it worked just the same way as the have expression, but I'd never checked.

Lean 3:

def foo'' : ℕ :=
begin
  have n : ℕ := 2,
  have n' := n + n,
  have n'' := n' + n',
  have n''' := n'' + n'',
  exact n'''
end

#print foo''
-- def foo'' : ℕ :=
-- 2 + 2 + (2 + 2) + (2 + 2 + (2 + 2))

Lean 4:

def foo'' : Nat := by
  have n : Nat := 2
  have n' := n + n
  have n'' := n' + n'
  have n''' := n'' + n''
  exact n'''

#print foo''
/-
def foo'' : Nat :=
let_fun n := 2;
let_fun n' := n + n;
let_fun n'' := n' + n';
let_fun n''' := n'' + n'';
n'''
-/

(let_fun x := v; w is syntactic sugar for (fun x => w) v)

[Kevin Buzzard]

Mario Carneiro said:

Eric Wieser said:

Am I imagining that Lean 4 did away with the instance cache and that therefore casesI isn't needed?

Yes to the second part, no to the first. Lean 4 didn't do away with the instance cache, it now effectively calls resetI whenever the local context changes at all. Some internals had to be changed to make this performant enough

So is the following a bug?

import Mathlib.Tactic.Cases

class Foo (T : Type) : Prop where

theorem exists_foo : ∃ T, Foo T := sorry

example : False := by
  cases' exists_foo with T hT
  -- `hT : Foo T`
  -- have : Foo T := inferInstance -- fails
  have : Foo T := hT
  have : Foo T := inferInstance
  sorry

[Adam Topaz]

I would guess that this is a bug with cases' but I can't say for sure. Of course, Mario will be able to tell immediately.

[Kyle Miller]

This seems to affect cases too:

class Foo (T : Type) : Prop where

theorem exists_foo : ∃ T, Foo T := sorry

example : False := by
  cases exists_foo
  rename_i T hT
  have : Foo T := hT -- delete to get error in next line
  have : Foo T := inferInstance
  sorry

[Adam Topaz]

both rcases and obtain work perfectly fine.

[Mario Carneiro]

Based on this evidence I would guess cases is at fault. rcases is most likely saved because it constructs some intermediates using have

[Floris van Doorn]

Together with @Kyle Miller I figured out what causes this.

• cases and cases' both call docs#Lean.MVarId.introN
• introN (via introNImp) calls docs4#Lean.Meta.withNewLocalInstances that checks whether certain fvars are classes using two methods isClassQuick? and isClassExpensive?. These two functions both have some support dealing with metavariables, but it makes the wrong decision in certain cases, not recognizing that Foo T is a class in Kyle's latest example. We tested that this fix fixes Kyle's latest example. Is a PR with this change welcome?

[Scott Morrison]

Seems like it would be worth making a PR with this fix. It may sit on the queue for a little while still.