Zulip Chat Archive

Stream: general

Topic: set coe_to_sort constructor


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.

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.

Rob Lewis (Jun 18 2020 at 09:02):

subtype.mk?

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

Rob Lewis (Jun 18 2020 at 09:23):

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

Patrick Massot (Jun 18 2020 at 09:30):

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

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

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

Mario Carneiro (Jun 18 2020 at 09:36):

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

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?

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

Mario Carneiro (Jun 18 2020 at 10:34):

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

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

Mario Carneiro (Jun 18 2020 at 10:36):

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

Yury G. Kudryashov (Jun 18 2020 at 12:14):

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

Last updated: Dec 20 2023 at 11:08 UTC