Eq.subst

Stream: lean4

[Dan Velleman]

In this example:

example (a b c m n : Int) (h1 : b = a * m) (h2 : c = b * n) : c = a * m * n :=
  Eq.subst h1 h2

I get the error message application type mismatch Eq.subst h1 argument h1 has type b = a * m : Prop but is expected to have type b = a * m * n : Prop. If I use @Eq.subst and supply the motive explicitly, it works. So I guess Lean isn't able to figure out the motive, but I'm surprised at that. Isn't inferring the motive pretty straightforward in this case?

[François G. Dorais]

elab_as_eliminator isn't much used in Lean 4. (It was added at some point to help porting mathlib but it isn't acutally used.)

In term mode, you need to supply the motive for pretty much all recursors. Instead of @Eq.subst, you can use Eq.subst (motive:=_) so the other implicit arguments are filled in.

That said, in the case of Eq.subst, you can simply use ▸:

example (a b c m n : Int) (h1 : b = a * m) (h2 : c = b * n) : c = a * m * n := h1 ▸ h2

[Mario Carneiro]

See also lean4#1679

[Dan Velleman]

I was assuming h1 ▸ h2 was just shorthand for Eq.subst h1 h2--that's what it said in TPIL 3. But I see that TPIL 4 says something slightly different--it says that ▸ is "a macro built on top of Eq.subst and Eq.symm." So I guess it has changed.
Actually, when I hover over h1 ▸ h2 in Lean it tells me that ▸ is a macro built on top of Eq.rec and Eq.symm.

[Mario Carneiro]

It was changed, because \t in lean 3 was very often useless / didn't do the obvious thing even when by rw h; exact e would work - which has exactly the same amount of information as h \t e

[François G. Dorais]

Eq.subst is limited to propositions; Eq.ndrec is the same but applies to any sort. Eq.rec is the natural eliminator for equality but it has a more complex signature that is rarely of much use.

[Richard Copley]

With this setup:

import Lean.Meta.Tactic.Rewrite

example (a b : Prop) (ha : a) : b → b :=
by
  have h₁ : (a → b) → b := fun f => f ha
  have h₂ : (a → b) = b := propext ⟨(fun f => f ha), (fun hb _ha => hb)⟩
  have h₃ := h₂ ▸ h₁
  -- h₁ : (a → b) → b
  -- h₂ : (a → b) = b
  -- h₃ : b → b

exact h₃ closes the goal, but exact h₂ ▸ h₁ gives the following error

type mismatch
  h₁
has type
  (a → b) → b : Prop
but is expected to have type
  (a → b) → a → b : Prop

Same error if I specify the expected type of h₃,

  have h₃ : b → b := h₂ ▸ h₁

Is there a bug here?

[Kevin Buzzard]

Higher order unification is undecidable so it's just different algorithms giving different answers I guess

[Kevin Buzzard]

My guess is that having access to the type of the term eq.subst is supposed to be producing changes how elaboration works.

[Richard Copley]

Must be! But we know it's possible to find a motive that does what is wanted, because we need only ignore the expected type :smiling_face_with_tear:

[Kevin Buzzard]

Right, and we also know that no computer program can reliably find these motives, because there's no algorithm, so it's not clear that failure of a computer program to do so is a bug.