Zulip Chat Archive

Stream: general

Topic: coe_coe


view this post on Zulip Chris Hughes (May 01 2018 at 19:20):

Just noticed the lemma coe_coe, which is tagged as simp, does this mean I need to be careful about tagging lemmas that make a double coercion into a single coercion with simp?

view this post on Zulip Kenny Lau (May 01 2018 at 20:15):

Just noticed the lemma coe_coe, which is tagged as simp, does this mean I need to be careful about tagging lemmas that make a double coercion into a single coercion with simp?

yes

view this post on Zulip Chris Hughes (May 01 2018 at 20:19):

What's the difference between has_coe and has_coe_t?

view this post on Zulip Kenny Lau (May 01 2018 at 20:21):

L37:

class has_coe (a : Sort u) (b : Sort v) :=
(coe : a  b)

/-- Auxiliary class that contains the transitive closure of has_coe. -/
class has_coe_t (a : Sort u) (b : Sort v) :=
(coe : a  b)

L94:

instance coe_trans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe a b] [has_coe_t b c] : has_coe_t a c :=
⟨λ x, coe_t (coe_b x : b)

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:35):

Maybe the type class coercion system uses this instance?

view this post on Zulip Kenny Lau (May 01 2018 at 20:36):

curiously, this has_coe_t appears literally nowhere

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:36):

Did you check the C++ bit?

view this post on Zulip Kenny Lau (May 01 2018 at 20:36):

maybe it's because of this:

instance coe_to_lift {a : Sort u} {b : Sort v} [has_coe_t a b] : has_lift_t a b :=
coe_t

view this post on Zulip Kenny Lau (May 01 2018 at 20:37):

so my conjecture is that they use has_coe_t to do transitive stuff, and then make has_lift_t the interface

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:38):

I remember Mario once saying something like he couldn't see the point of has_lift

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:38):

There's something about it in TPIL IIRC

view this post on Zulip Chris Hughes (May 01 2018 at 20:44):

So I don't need to worry unless it's a coe_t. The reason I noticed is because the coercion from pnat to int is a coe_t obviously, so it was being rewritten by coe_coe.

view this post on Zulip Chris Hughes (May 01 2018 at 20:46):

Which means I need double the lemmas

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:47):

Has_lift gives you access to the \u uparrow notation but lean won't ever insert them for you if you're not has_coe

view this post on Zulip Kevin Buzzard (May 01 2018 at 20:49):

But each lemma is twice as easy to prove :simple_smile:

view this post on Zulip Mario Carneiro (May 02 2018 at 08:58):

You shouldn't need "double the lemmas", you just need to make sure that any simp lemmas LHS are already split up into multiple coe arrows

view this post on Zulip Chris Hughes (May 02 2018 at 09:02):

But I also want the single arrows for rw's, because if I don't use simp, most of my coercions are single coercions

view this post on Zulip Mario Carneiro (May 02 2018 at 09:03):

why are you using composite coercions to begin with?

view this post on Zulip Mario Carneiro (May 02 2018 at 09:04):

I honestly wish the parser inserted multiple coe arrows, but the best I can do to recreate that is coe_coe

view this post on Zulip Mario Carneiro (May 02 2018 at 09:04):

but you can always write ((a:B):C) to get multiple coe arrows inserted

view this post on Zulip Kevin Buzzard (May 02 2018 at 10:17):

He wants to go from pnat to int

view this post on Zulip Mario Carneiro (May 02 2018 at 10:22):

I can see that. But why? What is the simp lemma under consideration? Like I said, you can use ((n:nat):int) to double-coerce

view this post on Zulip Chris Hughes (May 02 2018 at 10:23):

But that means having to type ((n : nat):int) all the time, instead of just n.

view this post on Zulip Mario Carneiro (May 02 2018 at 10:23):

all the time meaning only on the LHS of rules marked [simp]

view this post on Zulip Mario Carneiro (May 02 2018 at 10:23):

in proofs you can do whatever

view this post on Zulip Mario Carneiro (May 02 2018 at 10:24):

but it is important to state your lemmas correctly

view this post on Zulip Chris Hughes (May 02 2018 at 10:25):

But for any lemma marked simp, I also want it's single coercion corollary if I want to rewrite something.

view this post on Zulip Mario Carneiro (May 02 2018 at 10:25):

like what?

view this post on Zulip Mario Carneiro (May 02 2018 at 10:26):

just rw coe_coe

view this post on Zulip Chris Hughes (May 02 2018 at 10:26):

I could do that too.

view this post on Zulip Mario Carneiro (May 02 2018 at 10:27):

I think you underestimate the number of "single coercion corollaries"

view this post on Zulip Mario Carneiro (May 02 2018 at 10:27):

(hint: it's infinite)

view this post on Zulip Kenny Lau (May 02 2018 at 10:28):

infinity doesn't exist

view this post on Zulip Mario Carneiro (May 02 2018 at 10:28):

and neither do those corollaries, in mathlib


Last updated: May 16 2021 at 20:13 UTC