Zulip Chat Archive

Stream: general

Topic: set coe_to_sort constructor


view this post on Zulip Patrick Massot (Jun 18 2020 at 08:59):

What is the official name of def mk_it {α : Type*} {s : set α} {x : α} (h : x ∈ s) : s := ⟨x, h⟩? Surprisingly I need it in let statement, Lean simply doesn't let me define something of type s without this function.

view this post on Zulip Patrick Massot (Jun 18 2020 at 09:01):

And now I see cases tactic failed, unexpected failure when introducing auxiliary equatilies. I really need to learn stuff about that coercion from sets to types.

view this post on Zulip Rob Lewis (Jun 18 2020 at 09:02):

subtype.mk?

view this post on Zulip Patrick Massot (Jun 18 2020 at 09:14):

The question is: how to you make let believing that obvious answer?

example {α : Type*} {s : set α} (x :α) (h : x  s) : true :=
begin
  let X : s := subtype.mk x h, -- error!
  sorry
end

view this post on Zulip Rob Lewis (Jun 18 2020 at 09:23):

let X : ↥s := subtype.mk x h? :(

view this post on Zulip Patrick Massot (Jun 18 2020 at 09:30):

Indeed that works, but doesn't make me feel super happy.

view this post on Zulip Mario Carneiro (Jun 18 2020 at 09:34):

We could fix it by using t ← i_to_expr ``(%%e : Sort*) or the like in let, but I think that will produce a coe rather than a coe_sort

view this post on Zulip Mario Carneiro (Jun 18 2020 at 09:35):

I don't know if there is a function exposed that will allow us to trigger the coe-to-sort parser transform

view this post on Zulip Mario Carneiro (Jun 18 2020 at 09:36):

I suppose a hack would be to elaborate \lam (x : e), x and then extract e

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 10:31):

Oh I see -- the issue is that lean will automatically insert a coe, but not a coe to sort?

view this post on Zulip Mario Carneiro (Jun 18 2020 at 10:33):

It will still typecheck, but it will be an observable difference and that could lead to downstream breakage

view this post on Zulip Mario Carneiro (Jun 18 2020 at 10:34):

for example if one has a simp lemma and the other doesn't

view this post on Zulip Mario Carneiro (Jun 18 2020 at 10:35):

As is it's not inserting any coe because the "type" is parsed first and then the value is parsed and asserted to have the type (which is okay because the type is coerced here) and then the type and the value are passed to definev which complains because the "type" isn't a type

view this post on Zulip Mario Carneiro (Jun 18 2020 at 10:36):

(This bug is in the code of tactic.interactive.let btw)

view this post on Zulip Yury G. Kudryashov (Jun 18 2020 at 12:14):

  let X : s := x, h, -- works

Last updated: May 09 2021 at 19:11 UTC