subtype coercion

Stream: new members

[Vincent Beffara]

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]

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]

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

[Marc Huisinga]

or use abbreviationinstead of def

[Johan Commelin]

@Vincent Beffara See also https://github.com/leanprover-community/mathlib/blob/5ed5f59433278367f0b2ceeb7b363d21840a3fc0/test/delta_instance.lean

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Marc Huisinga]

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

[Vincent Beffara]

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

[Johan Commelin]

@Jeremy Avigad :up:

[Rob Lewis]

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]

@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]

@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]

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.

[Ryan Krueger]

(deleted)

[Ryan Krueger]

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?