coe_coe

Stream: general

[Chris Hughes]

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]

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]

What's the difference between has_coe and has_coe_t?

[Kenny Lau]

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]

Maybe the type class coercion system uses this instance?

[Kenny Lau]

curiously, this has_coe_t appears literally nowhere

[Kevin Buzzard]

Did you check the C++ bit?

[Kenny Lau]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

There's something about it in TPIL IIRC

[Chris Hughes]

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]

Which means I need double the lemmas

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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]

why are you using composite coercions to begin with?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

He wants to go from pnat to int

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

in proofs you can do whatever

[Mario Carneiro]

but it is important to state your lemmas correctly

[Chris Hughes]

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

[Mario Carneiro]

like what?

[Mario Carneiro]

just rw coe_coe

[Chris Hughes]

I could do that too.

[Mario Carneiro]

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

[Mario Carneiro]

(hint: it's infinite)

[Kenny Lau]

infinity doesn't exist

[Mario Carneiro]

and neither do those corollaries, in mathlib