A question regarding the eta rule for the product type

Stream: lean4

[Gordon Hsu]

Why is there an error for rfl in the code below?

example (m : Nat × Nat) : Nat :=
  let ⟨a, b⟩ := m
  have : m.2 = b := rfl /-
  type mismatch
    rfl
  has type
    ?m.36775 = ?m.36775 : Prop
  but is expected to have type
    b = m.snd : Prop
  -/
  a

Besides using a match and congrArg Prod.snd as shown below, can definitional equality be applied somehow?

example (m : Nat × Nat) : Nat :=
  match e : m with
  | ⟨a, b⟩ =>
    have : m.2 = b := congrArg Prod.snd e
    a

[Kyle Miller]

Destructuring let notation doesn't keep track of the relationship between the value being destructed and the new variables unfortunately.

The match e : m with is one way to do it, and the other is to simply not destruct m in the first place.

[Gordon Hsu]

Thanks for the clarification. One other question, how is the let binder different from Prod.eta (p : α × β) : (p.1, p.2) = p := rfl? Why is one definitionally equal, yet the other isn't? I think I am missing something very basic.

[Aaron Liu]

The let binder throws away the relationship between a, b, and m.

[Kyle Miller]

The let destructuring bind is sugar for match, so just like match there's no relationship between the original value and the pattern variables.

[Kyle Miller]

Underneath all this is that match uses recursors to break apart values, and there's no defeq relationship between the value broken apart and the components given by the recursor.

It seems like a reasonable feature request for match for structure-likes to be special cased, to use projections instead of the recursor. So for example let ⟨a, b⟩ := m; ... would be short for let a := m.1; let b := m.2; ....

[Kyle Miller]

One small complexity here is that in case the structure-like has dependent fields, successive fields refer to the new let variables rather than m.

This is a reasonably large project though.

[Kevin Buzzard]

Note that in tactic mode obtain \<a,b\> := m will simply remove m and replace it with Prod.mk a b so you won't have this problem

[Aaron Liu]

It also leaves some ugly recursors in the term generated.

[Kyle Miller]

That's not something people usually care about for proofs though. (But in the context of the original question, yes that could be an issue, and it's consistent with the 'don't use tactics for data' advice.)

[Gordon Hsu]

Thanks for all your help :big_smile:
Since let boils down to match that uses recursors, there is no definitional equality with propositional equality being the only thing available. The obtain tactic is indeed helpful in tactic mode.

[Eric Wieser]

There is an open feature request on GitHub for changing the let behavior here

[Gordon Hsu]

Eric Wieser said:

There is an open feature request on GitHub for changing the let behavior here

That's awesome, but I couldn't find the GitHub issue.

[Kyle Miller]

I wasn't able to find it either.

[Eric Wieser]

lean4#5216 is what I was thinking of