Zulip Chat Archive

Stream: new members

Topic: Is it bug?


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 21 2020 at 00:06):

That's running 3.5.0c

view this post on Zulip Anton Kalsin (Jan 21 2020 at 00:08):

No changes

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Anton Kalsin (Jan 21 2020 at 00:12):

Thanks. It's work

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 21 2020 at 00:13):

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

view this post on Zulip Mario Carneiro (Jan 21 2020 at 00:15):

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

view this post on Zulip Mario Carneiro (Jan 21 2020 at 00:15):

so that it knows what to abstract

view this post on Zulip Anton Kalsin (Jan 21 2020 at 00:24):

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

view this post on Zulip 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