Zulip Chat Archive

Stream: new members

Topic: subtype coercion


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Oct 23 2019 at 08:43):

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

view this post on Zulip Marc Huisinga (Oct 23 2019 at 08:44):

or use abbreviationinstead of def

view this post on Zulip Johan Commelin (Oct 23 2019 at 08:47):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 23 2019 at 08:48):

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

view this post on Zulip Johan Commelin (Oct 23 2019 at 08:48):

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Oct 23 2019 at 09:07):

@Jeremy Avigad :up:

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ryan Krueger (Feb 23 2020 at 20:15):

(deleted)

view this post on Zulip 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