intro (x, y)

Stream: general

[Heather Macbeth]

I noticed some odd behaviour with the intro (x, y) syntax which I couldn't isolate further.

import Std.Tactic.RCases

-- strange behaviour
example : ∀ (x : α × α), x = id x := by
  intro (x, y)
  -- `⊢ (x, y) = id (x, y)`
  dsimp
  -- not done yet, goal `⊢ (x, y) = (x, y)`
  rfl

/- compare normal behaviour: -/

example : ∀ (x : α × α), x = id x := by
  rintro ⟨x, y⟩
  -- `⊢ (x, y) = id (x, y)`
  dsimp
  -- done

example : ∀ (x : α × α), x = id x := by
  intro p
  -- `⊢ p = id p`
  dsimp
  -- done

I'm on Std 101f1d041068be39093633e4ebf95f8c6fae2240.

[Heather Macbeth]

I clicked around in the infoview and I couldn't see how the goal ⊢ (x, y) = id (x, y) differed between the first and second examples, but I suppose there must be some subtle difference since the dsimp acts on them differently.

[Kyle Miller]

What's the pp.all output in the intro (x, y) case?

[Jireh Loreaux]

presumably these are simple enough terms that pp.all is actually readable. How about looking at that?

[Heather Macbeth]

⊢ @Eq.{?u.11 + 1} (Prod.{?u.11, ?u.11} α α) (@Prod.mk.{?u.11, ?u.11} α α x y)
  (@id.{?u.11 + 1} (Prod.{?u.11, ?u.11} α α) (@Prod.mk.{?u.11, ?u.11} α α x y))

[Heather Macbeth]

versus, in the second example,

⊢ @Eq.{?u.128 + 1} (Prod.{?u.128, ?u.128} α α) (@Prod.mk.{?u.128, ?u.128} α α x y)
  (@id.{?u.128 + 1} (Prod.{?u.128, ?u.128} α α) (@Prod.mk.{?u.128, ?u.128} α α x y))

[Matthew Ballard]

Is there a useful trace for dsimp?

[Alex J. Best]

In this case pp.raw might instead reveal the issue:

[mdata noImplicitLambda:1 Eq.{succ ?_uniq.11} (Prod.{?_uniq.11, ?_uniq.11} _uniq.21 _uniq.21) (Prod.mk.{?_uniq.11, ?_uniq.11} _uniq.21 _uniq.21 _uniq.51 _uniq.52) (Prod.mk.{?_uniq.11, ?_uniq.11} _uniq.21 _uniq.21 _uniq.51 _uniq.52)]

there is some mdata floating around that I assume blocks something

[Heather Macbeth]

With set_option trace.Meta.Tactic.simp.rewrite true I get

[Meta.Tactic.simp.rewrite] @id_eq:1000, id (x, y) ==> (x, y)

for both.

[Heather Macbeth]

@Alex J. Best Indeed! The first one has this mdata noImplicitLambda, the second doesn't.

[Heather Macbeth]

OK, so is this a bug or a feature?

[Jireh Loreaux]

lol, I didn't know about pp.raw, but I think we should change the name to pp.all_no_really_I_mean_ALL. :laughing:

[Heather Macbeth]

And if it's a bug, is it a bug in intro (x, y) or a bug in dsimp?

[Kyle Miller]

Found it, in dsimp in docs#Lean.Meta.dsimpGoal

      if let some (_, lhs, rhs) := targetNew.eq? then
        if (← withReducible <| isDefEq lhs rhs) then
          mvarIdNew.assign (← mkEqRefl lhs)
          return (none, usedSimps)

it's not erasing metadata before doing eq?

[Kyle Miller]

i.e., it should be targetNew.consumeMData.eq?, just like the other pattern matches against targetNew in that function

[Heather Macbeth]

Awesome! Let me know whether you want me to write up a bug report or whether I can leave it in your capable hands.

[Kyle Miller]

lean4#2514