Tutorial Inductive Types

[thomas-lamiaux]

What are the inductive type accepted by Coq:

• mutual inductive
• uniform parameters
• indices
• non-uniform parameters
• nested

Fixpoint + match

Tactics to reason about them

[Villetaneuse]

Thinking about it, I think there will be many tutorials about inductive types:

• simple inductive types, first enumerated, then truly inductive (nat, lists, ...), the discriminate, destruct and induction tactics, and match à la OCaml to write programs; maybe end with generated elimination rules.
• inductive propositions, first not really inductive (and, or) then even, le, etc
• maybe a separate tutorial for trees, AST-like inductives, maybe with mutual inductives
• then a hardcore tutorial with indices, parameters, match in its full generality (match foo as bar in (C _ _ baz1 baz2) return (R bar baz1 baz2))..., singleton elimination, equality, etc and positivity constraint.

But even this somewhat simple plan could fail due to difficulties leaking in the early stages.

[thomas-lamiaux]

I dont know what else is needed but I think there should be at least one tutorial touring all of them at once

[thomas-lamiaux]

@TheoWinterhalter maybe you could give some feedback from your class on what is confusing student even though they have already done some ocaml / rocq for most

[TheoWinterhalter]

Feedback on what exactly? One thing I can say is that understanding what should be the induction principle of an inductive type is something that is hard for students, especially when the inductive type is an inductive predicate (regardless of whether it is dependent or not (in Prop), which I guess would be an additional pain point).

[thomas-lamiaux]

Well exactly that, there could indeed be an explanation on inductive principles. I don't think it fits a tutorial though.