## Stream: new members

### Topic: subtype coercion

#### Vincent Beffara (Oct 23 2019 at 08:29):

Hi,
TPiL states that "the standard library defines a coercion from subtype {x : α // p x} to α so I would expect the following to work:

def tttt (n : ℕ) : Prop := true
def toto := { n : ℕ // true }
def toto' := subtype tttt
def titi : toto := ⟨3,trivial⟩
def titi' : toto' := ⟨3,trivial⟩
def tata (n : ℕ) : ℕ := n+2
#reduce (tata titi)
#reduce (tata titi')
instance tutu : has_coe toto ℕ := ⟨subtype.val⟩
#reduce (tata titi)


Unfortunately only the last reduce works, the first one complains that it is expecting a nat and gets a toto instead. Am I misunderstanding the sentence in TPiL?

#### Chris Hughes (Oct 23 2019 at 08:41):

The problem is probably that you renamed the type, and after renaming, a type loses all the instances it has.

The instance search does not unfold the definition of toto when searching for a coercion.

#### Rob Lewis (Oct 23 2019 at 08:43):

You can put @[reducible] in front of toto and toto' to make it work.

#### Marc Huisinga (Oct 23 2019 at 08:44):

or use abbreviationinstead of def

#### Johan Commelin (Oct 23 2019 at 08:47):

Recently we got some slick method to carry instances over to a "type wrapper"

#### Johan Commelin (Oct 23 2019 at 08:48):

The thing is, sometimes you want this to happen, sometimes not. Example: if X is an ordered set... then dual X should of course not find the order instance on X

#### Johan Commelin (Oct 23 2019 at 08:48):

Instead, we want to define a new order, that is opposite to the one on X

#### Johan Commelin (Oct 23 2019 at 08:48):

But Lean doesn't see any difference between dual and toto

#### Marc Huisinga (Oct 23 2019 at 08:50):

is semi-reducibility explained anywhere in TPIL, or are there examples for where defs are unfolded and where not?

#### Vincent Beffara (Oct 23 2019 at 08:57):

Thanks, I think I see the point. The wording in TPiL is a bit misleading then, it can be read as "whenever you define a subtype Lean will instantiate the corresponding coercion", which it doesn't (for good reason).

#### Rob Lewis (Oct 23 2019 at 09:15):

is semi-reducibility explained anywhere in TPIL, or are there examples for where defs are unfolded and where not?

reducible, semireducible, and irreducible are just relative markers. Different components of the system need to decide how hard to try to reduce expressions. Type class inference only unfolds reducible defs, the elaborator typically unfolds reducible and semireducible, the kernel can see through everything. Some tactics (linarith, ring) have options to set how hard they should try to match expressions.

#### Jeremy Avigad (Oct 23 2019 at 15:48):

@Vincent Beffara There is a brief discussion in TPIL of the fact that type class inference doesn't generally unfold definitions:
https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#managing-type-class-inference
Would it be helpful to refer to that section somewhere else in the text? Where would you put the reference and what would you say?

#### Mario Carneiro (Oct 23 2019 at 22:50):

@Jeremy Avigad I would suggest re-wording the discussion about the coercion from subtype to Type so not suggest that a definition is made. I'm not sure exactly what the context is for this passage though

#### Jeremy Avigad (Oct 23 2019 at 23:44):

Oh, good. I will say that subtypes have coercions, and then point out that if you define a type to be equal to a subtype, you can explictly make it an instance. Thanks.

(deleted)

#### Ryan Krueger (Feb 23 2020 at 20:25):

If one has to define the coercion themselves (e.g., as Vincent did with

instance tutu : has_coe toto ℕ := ⟨subtype.val⟩


), what is the point of coe_subtype?

Last updated: May 11 2021 at 22:14 UTC