Is it bug?

Stream: new members

[Anton Kalsin]

Sorry for my english.

I've placed questions in code. What is going on? Can anybody explain me?

namespace hidden
universe u

inductive eq {α : Type u} (a : α) : α → Prop
| refl : eq a

@[elab_as_eliminator]
theorem subst {α : Type u} {a b : α} {P : α → Prop}
  (h₁ : eq a b) (h₂ : P a) : P b :=
eq.rec h₂ h₁

def subst₂ {α : Type u} {a b : α}
  (P : α → Prop) (h₁ : eq a b) (h₂ : P a) : P b :=
@subst α a b P h₁ h₂

example {α β : Type u} {a b : α} (f : α → β) (h : eq a b) : eq (f a) (f b) :=
  have p : α → Prop, from assume x, eq (f a) (f x),

  -- why₁?
  have (λ x, eq (f a) (f x)) a = eq (f a) (f a), from rfl, -- it's ok
  --have p a = eq (f a) (f a), from rfl, -- it's not ok

  sorry

example {α β : Type u} {a b : α} (f : α → β) (h : eq a b) : eq (f a) (f b) :=
  let p : α → Prop := λ x, eq (f a) (f x) in

  have e : p a, from eq.refl (f a),

  -- why₂?
  have @subst α a b p h e = subst₂ p h e, from rfl, -- have this, but:
  show eq (f a) (f b), from @subst α a b p h e -- it's ok
  --show eq (f a) (f b), from subst₂ p h e -- it's not ok

end hidden

This code on web editor

[Kevin Buzzard]

Try the more modern web editor at https://leanprover-community.github.io/lean-web-editor/ and see if anything changes?

[Kevin Buzzard]

That's running 3.5.0c

[Anton Kalsin]

No changes

[Mario Carneiro]

For why₁, you need to use let p : α → Prop := assume x, eq (f a) (f x), instead of have

[Mario Carneiro]

The difference is that with let lean will remember the definition and be able to unfold it later

[Anton Kalsin]

Thanks. It's work

[Mario Carneiro]

For why₂, the difference is that subst₂ is not marked as elab_as_eliminator, so when it tries to figure out why P b in the type of subst₂ should match with eq (f a) (f b) it guesses P := eq (f a) and b := f b and gets to nonsense

[Mario Carneiro]

If you use @subst₂ ... it should work

[Mario Carneiro]

Actually, for elab_as_eliminator to work b has to be explicit and provided

[Mario Carneiro]

so that it knows what to abstract

[Anton Kalsin]

Thanks. It's not clear for me now, but I'll read tutorial in more detail

[Mario Carneiro]

It's not really a theory thing, it has to do with how elaboration works. As long as you sprinkle enough @ signs you can make it work