## Stream: new members

### Topic: Is it bug?

#### Anton Kalsin (Jan 21 2020 at 00:04):

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 (Jan 21 2020 at 00:06):

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

#### Kevin Buzzard (Jan 21 2020 at 00:06):

That's running 3.5.0c

No changes

#### Mario Carneiro (Jan 21 2020 at 00:09):

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

#### Mario Carneiro (Jan 21 2020 at 00:09):

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

#### Anton Kalsin (Jan 21 2020 at 00:12):

Thanks. It's work

#### Mario Carneiro (Jan 21 2020 at 00:13):

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 (Jan 21 2020 at 00:13):

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

#### Mario Carneiro (Jan 21 2020 at 00:15):

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

#### Mario Carneiro (Jan 21 2020 at 00:15):

so that it knows what to abstract

#### Anton Kalsin (Jan 21 2020 at 00:24):

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

#### Mario Carneiro (Jan 21 2020 at 00:31):

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

Last updated: May 11 2021 at 12:15 UTC