## Stream: general

### Topic: coe_coe

#### 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?

#### 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

#### Chris Hughes (May 01 2018 at 20:19):

What's the difference between has_coe and has_coe_t?

#### 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)⟩


#### Kevin Buzzard (May 01 2018 at 20:35):

Maybe the type class coercion system uses this instance?

#### Kenny Lau (May 01 2018 at 20:36):

curiously, this has_coe_t appears literally nowhere

#### Kevin Buzzard (May 01 2018 at 20:36):

Did you check the C++ bit?

#### 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⟩


#### 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

#### Kevin Buzzard (May 01 2018 at 20:38):

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

#### Kevin Buzzard (May 01 2018 at 20:38):

There's something about it in TPIL IIRC

#### 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.

#### Chris Hughes (May 01 2018 at 20:46):

Which means I need double the lemmas

#### 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

#### Kevin Buzzard (May 01 2018 at 20:49):

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

#### 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

#### 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

#### Mario Carneiro (May 02 2018 at 09:03):

why are you using composite coercions to begin with?

#### 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

#### Mario Carneiro (May 02 2018 at 09:04):

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

#### Kevin Buzzard (May 02 2018 at 10:17):

He wants to go from pnat to int

#### 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

#### Chris Hughes (May 02 2018 at 10:23):

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

#### Mario Carneiro (May 02 2018 at 10:23):

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

#### Mario Carneiro (May 02 2018 at 10:23):

in proofs you can do whatever

#### Mario Carneiro (May 02 2018 at 10:24):

but it is important to state your lemmas correctly

#### 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.

like what?

#### Mario Carneiro (May 02 2018 at 10:26):

just rw coe_coe

#### Chris Hughes (May 02 2018 at 10:26):

I could do that too.

#### Mario Carneiro (May 02 2018 at 10:27):

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

#### Mario Carneiro (May 02 2018 at 10:27):

(hint: it's infinite)

#### Kenny Lau (May 02 2018 at 10:28):

infinity doesn't exist

#### Mario Carneiro (May 02 2018 at 10:28):

and neither do those corollaries, in mathlib

Last updated: May 16 2021 at 20:13 UTC