two basic recursor questions

Stream: general

[Kevin Buzzard]

I know this is probably dependent type theory 101, but I've realised that as a mathematician I am only really interested in structures, and hence don't have a good understanding of recursors [my excitement in discovering that I could do induction on the reals was rather punctured when I realised the recursor was "if it's true for all equivalence classes of Cauchy sequences, then it's true for all reals"].

Q1) The recursor for eq is basically the assertion that if x = y then there's a map C x -> C y where C is Sort-valued (indeed I've been telling the 1st years that transitivity of = is proved by induction on =). But I can't convince myself that this should be the recursor, which just means that I don't understand the precise algorithm which goes from the definition of the inductive type to the definition of the recursor. Where do I learn more about that? Is it easy to see if you think about things the right way?

Q2) = is a prop and or is as well. But or only eliminates to Prop, and = seems to eliminate to Sort. What is the difference? This might just be Q1 again.

[Chris Hughes]

Recursors for propositions make more sense if you look at the drec recursor.

[Chris Hughes]

For Q2 the difference is that or has two constructors and eq has one.

[Chris Hughes]

Also, every argument to the constructor is either a proposition or mentioned in the Type of the output.

[Chris Hughes]

Mario's paper has the generic algorithm

[Chris Hughes]

https://github.com/digama0/lean-type-theory

[Chris Hughes]

I find it quite hard to read personally.

[Mario Carneiro]

For eq, the key is to notice that eq is not the inductive type, eq a : A -> Prop is. It has one constructor, refl : (eq a) a. So suppose you have a dependent family C : Pi (b : A), eq a b -> Prop, and you want to prove it holds true "everywhere", that is, \all b h, C b h. Since h : eq a b, and there is "only one" equality in the inductive family, namely h = (refl : eq a a), then it suffices to prove C a (refl a). And that's the recursor: C a (refl a) -> \all b (h : a = b), C b h. If you ignore the last argument, it says C a -> a = b -> C b.

[Mario Carneiro]

Sorry about the readability; chapter 2 was intended to be terse so that it can be used as a reference. It's not the best source for motivation

[Kevin Buzzard]

Thanks for these comments. I will go away and think more.

[Gihan Marasingha]

I'm trying to get a better understanding of recursors too. If I understand correctly, rec is the fundamental recursor from which the other recursors are defined. Is that correct?

Playing around, it seems that:

• rec, rec_on, and cases_on are defined for all inductive types,
• binduction_on and brec_on are defined if the type has a recursive constructor, and
• dcases_on, drec, and drec_on are defined if the type is in Prop.

Is that correct?

If so, it would be great if there was a list of simple examples of each recursor in action. For instance, give a simple example of a proof by dcases_on that is nicer than the (nicest) proof of the same result by rec.

[Kevin Buzzard]

I don't know the story at all about exactly what the system generates (eg when you get a no_confusion or whatever) but I do know that everything is built from rec. You can use try things like #print nat.rec_on and see its definition and then#print nat.rec and see something completely different.

[Gihan Marasingha]

Thanks. I'm probably wasting my time with this as I only see one use (outside of the induction' tactic definition) of dcases_on in mathlib . I wonder if it's only there to help with constructing induction tactics.