getting the defining equation of a recursor

Stream: new members

[Patrick Thomas]

Is there a way to display the defining equation for the recursor of a given inductive type? Is this a sensible question? I just read about recursors from pg. 28 of https://hott.github.io/book/nightly/hott-online-1204-g7415493.pdf. I know #check will give me the type of the function, but is there a way to get the function itself?

[Scott Morrison]

Does

inductive mynat
| Z
| S : mynat → mynat
#print prefix mynat

give you what you want?

[Chris Hughes]

I think he means the iota reduction rule, which isn't written anywhere I don't think.

[Patrick Thomas]

I'm not certain, but I think what I see printed from #print prefix mynat for mynat.rec is the type?

[Kevin Buzzard]

The recursor for a type X is called X.rec and it doesn't have a definition, it just has a type. It is an axiom in the theory

[Kevin Buzzard]

Every time a new type is created using inductive or structure or class the constructors and recursor are added to the theory as new constants or axioms or whatever you want to call them. They have no definitions. Everything else gets defined in terms of these.

[Patrick Thomas]

So there is no defining equation like recA×B(C,g,(a,b)) :≡ g(a)(b) as given in the linked text? How do we determine how to use them?

[Kevin Buzzard]

That's iota reduction, which is true by definition.

[Kevin Buzzard]

Lean cannot even tell the difference between the two sides in some sense, but prefers the right hand side to the left hand side. A tactic like dsimp would apply all reductions Lean can think of. A list of the reductions Lean knows is in section 3.7 of the reference manual. What is your background? I hope I'm not patronising you -- I don't mean to. I didn't know this stuff at all a year or so ago, so I just assume nobody else knows it ;-)

[Kevin Buzzard]

I guess iota reduction is the only "move" that Lean can make faced with a recursor, because it can't unfold the definition, because there is no definition.

[Patrick Thomas]

Nope, this is new to me, I appreciate it.

[Kevin Buzzard]

I feel guilty about all this. About six months ago I spent quite a lot of time trying to figure out what was going on here -- what was true by definition and what was true for other reasons (e.g. a+b=b+a is true because of a theorem, not by definition). I got it all straight in my head and then made a note to write some good teaching materials but I never made those teaching materials.

[Patrick Thomas]

No worries. Thank you for the link to that section of the reference manual. I think that will help.

[Kevin Buzzard]

I can never find it because the title is "computation" -- I had not realised that this is what a computer scientist means when they talk about computation! They mean changing terms into other terms, apparently. The Lean tactic change (and show, a synonym) changes the goal to anything which is definitionally equivalent to the goal; it's a useful tactic if you want to experiment with definitional equality.

[Mario Carneiro]

This is definitely not what a computer scientist means when they say "computation", but it is what a type theorist means when they say "computation"

[Kevin Buzzard]

Aren't they the same thing? ;-)