Zulip Chat Archive

Stream: new members

Topic: rec only to Prop?

Chris M (Jul 30 2020 at 18:45):

I have the code

universe u

inductive ind1 : Sort u
| const1 : ind1
| const2 : ind1  ind1  ind1

#check @ind1.rec

And this last check gives me

ind1.rec :
   {C : ind1  Prop},
    C ind1.const1  ( (a a_1 : ind1), C a  C a_1  C (ind1.const2 a a_1))   (n : ind1), C n

This is strange, because shouldn't C have the type C:ind1 \to Sort v or something like this? This is at least what the reference manual says.

Chris B (Jul 30 2020 at 19:10):

I think this is large elimination vs. small elimination (into Prop). You need to meet certain conditions in order to get large elimination. This one's small because it's in Sort u. If you change it to Type u, the motive will be (C : ind1 -> Sort l)

Chris B (Jul 30 2020 at 19:11):

You can also get large elimination with an instance of subsingleton.

Chris B (Jul 30 2020 at 19:15):

There are some other rules for getting a large eliminating inductive prop, it's like zero or one constructors, and all of the arguments have to be params/indices or props themselves ala false/eq.

Chris B (Jul 30 2020 at 19:32):

IIRC the motivation is that with proof irrelevance and large eliminating prop you can do something like

def x : ind1.{0} := ind1.const1
def y : ind1.{0} := ind1.const2 x x
-- by proof_irrel
lemma x_eq_y : x = y := rfl

inductive color
| black : color
| white : color

def pick_color : ind1 -> color
| const1 := black
| const2 := white

def black_eq_white : black = white := congr_arg pick_color x_eq_y

Chris M (Jul 31 2020 at 03:17):

What does the .{0} in ind1.{0} mean?

Chris B (Jul 31 2020 at 05:03):

@Chris M It's a way of explicitly passing the universe variable. In this case putting it in Sort 0/Prop.

#check ind1 -- ind1 : Sort u_1
universe x
#check ind1.{x} -- ind1 : Sort x
#check ind1.{0} -- ind1 : Prop

Last updated: Dec 20 2023 at 11:08 UTC