Explanation: Induction, pattern matching, fixed points #86

patrick-nicodemus · 2025-04-03T20:19:33Z

I have written a document which I think best falls under the "Explanation" heading of https://diataxis.fr/

It explains induction and pattern matching, with some worked examples of dependent elimination. It needs a bit of polishing but overall comments would be good.

I'm not really familiar with mutual recursion, but I think I understand dependent elimination for a single inductive type pretty well and can write on that. I think the presentation here is good:
http://adam.chlipala.net/cpdt/html/MoreDep.html
and it would be good to incorporate some of that into the documentation.

thomas-lamiaux · 2025-04-03T20:35:42Z

I have to look at it in more details but I think it is a very good first step for sth that is often confusing for beginners.
But, before moving forward, I think we should discuss what we want for inductive types because

I was thinking of having a more complete tutorial about inductive types that would also mention tactics to reason about them like induction, destruct etc... Explanation: Induction, pattern matching, fixed points #86. But doing so may create sth too long?
We should also discuss the target. Should we have one tutorial, or one for CS people and another version for maths people? This is a tutorial for CS people, and I think that have two is indeed the best.

patrick-nicodemus · 2025-04-03T20:48:33Z

I think that the tactics should be in a separate tutorial if usage is the primary goal.

I think thematically it makes sense to have one "explanation" be purely about Gallina with no tactic scripts, because it is a pedagogical piece about the theory behind CIC inductive definitions and how to use them in Rocq. The tactics can go in a second tutorial that refers to the explainer for the low level theory, and maybe suggests common mistakes (your induction hypothesis is too weak and you need to revert more variables)

On the other hand if we are talking about the relationship between induction and destruct tactics and the Gallina terms they can go here, helping to bridge the mental gap between proof scripts and gallina

thomas-lamiaux · 2025-04-03T21:33:51Z

I'll read it more carefully, and tell you more about it next week.
It would be good to ask on zulip what people think about that.

SkySkimmer · 2025-04-04T13:58:58Z

src/Explanation_Induction.v

+    use these as our basic examples.
+*)
+
+Notation "x -> y" := (forall _ : x, y) (at level 99, right associativity, y at level 200).


is this file meant to run with -noinit? if not what is this Notation for?

For some reason the prelude wasn't loading when I edited this, I probably just didn't have my environment configured properly. It's fine to load the prelude for this file.

thomas-lamiaux · 2025-04-05T15:40:02Z

@patrick-nicodemus I have looked at it in details. First, here is some general feedback. I'll write a review just after to make technical comments on the code and the explanations.

Right now, the explanations are a bit weird because it is kinda written as an explanation, even though the content is more the one of a tutorial. This is explaining how to write function by fixpoint and pattern-matching in practice, talking about stuff like in .. as .. return, introducing concept and difficulties step by step. But, this content really is the one of a tutorial. An explanation would be more like "How does strict positivity work, and why it is needed" or "How does the guard condition work?" giving an overview of how a feature works internally, for instance, to explain why it works like that in practice.

I think this should really be a tutorial "Introduction to Inductive Types, and Writing Functions on them by Fixpoint and Pattern-Matching". It is almost already there, and it is really needed. It can then be completed by a second tutorial, "how to reason about inductive types".

thomas-lamiaux

It mostly need reordering

thomas-lamiaux · 2025-04-05T15:43:30Z

src/Explanation_Induction.v

+    In this section we explain the basics of inductive types and pattern
+    matching in Rocq. We focus on the fragment of the language which
+    Rocq shares with languages based on the Hindley-Milner type system
+    with algebraic data types, such as OCaml and Haskell,
+    deferring dependent types to the next section.
+
+    Programmers who are experienced in OCaml or Haskell
+    can skim this section quickly to learn the Rocq syntax
+    for pattern matching and recursive function definitions via the
+    [fix] combinator.


This is not really a good argument because everything is always dependent in Rocq, including parameters.
I think it is best to introduce the different inductive types as mentioned in #81, in order sth like:

Basic ones like nat

Mutual inductive types

parametrized inductive types

index inductive types, and non-uniform parameters

nested inductive types

thomas-lamiaux · 2025-04-05T15:44:41Z

src/Explanation_Induction.v

+(** The examples we have considered so far are "enumerated types",
+    where the constructors for the inductive type [T] have been constants
+    inhabiting T. In the following example, we show that the programmer
+    can declare constructors which are functions from another type into [T].
+    We also illustrate that inductive types, like other kinds of definitions,
+    can be *parameterized* by arguments, which defines a *family* of inductive
+    data types. *)


Start a new section about parametrized inductive types. Move and discuss recursion in the previous section.

thomas-lamiaux · 2025-04-05T15:47:11Z

src/Explanation_Induction.v

+Fixpoint add (n m : nat) :=
+  match n with
+  | O => m
+  | S n0 => S (add n0 m)
+  end.


In practice, everyone uses Fixpoint. So in a tutorial, you want to explain

there is a fix constructor, how it works, what is the point

explain how it relates to Fixpoint

stick to Fixpoint for the rest of the tutorial unless fix really is needed, in which case you need to explain why

thomas-lamiaux · 2025-04-05T15:48:29Z

src/Explanation_Induction.v

+    The programmer rarely has to write [{struct m}] explicitly, as
+    Rocq can usually infer it, but it is likely to appear in Rocq's
+    output when they are printing proof terms that use induction.


Rocq will just try them all. This can make the code longer to type check, and the "wrong one" can be picked, making unfolding weird though it is rare.

thomas-lamiaux · 2025-04-05T15:52:56Z

src/Explanation_Induction.v

+Inductive EvenOdd : bool -> Type :=
+| ZeroEven : EvenOdd true
+| S_EO : forall (b : bool), EvenOdd b -> EvenOdd (negb b).


This really is not the usual definition of Even and Odd. This not a mutual inductive type. This is an encoding of mutual inductive type using indices. Mutual inductive type are primitive in the kernel and that it is how they should be used unless people know what they are doing.

This will be confusing to newcomers, and they are much better examples of index inductive types, like the predicate All. This part is to be removed entirely.

thomas-lamiaux · 2025-04-05T16:15:47Z

src/Explanation_Induction.v

+    The type of natural numbers [nat] that we defined earlier
+    can be defined in language with algebraic data types
+    like OCaml or Haskell. However, even though the type itself
+    may seem fairly simple, the pattern matching rule for
+    for defining functions on the natural numbers must account for
+    dependent typing: the elimination rule does not just tell us how to
+    define a function [nat -> A], but how to define an element of
+    [forall n: nat, P] where [P] may depend nontrivially on [n].


Everything is always dependent in Rocq. This is weird to introduce more complicated inductive type to go back to nat. Most explanations about match should be moved earlier, showng that Rocq can infer it in simple cases.

thomas-lamiaux · 2025-04-05T16:17:46Z

src/Explanation_Induction.v

+(** ** 4. Case study: Equality
+
+    The propositional equality type is a relatively
+    simple example of an indexed inductive type which allows us to
+    work through some examples without too much additional complexity.
+ *)


It should be part of the section index inductive type, provided it really adds sth

thomas-lamiaux · 2025-04-05T16:22:15Z

src/Explanation_Induction.v

+(** In the example above, if you remove [: vector A (n' + m)], it
+    won't compile. Rocq is unable to infer the return type unless it is
+    explicitly annotated. As a general rule, if your code doesn't
+    compile, adding more type annotations and filling in implicit
+    arguments may help you get better error messages, and make the
+    typechecker happy, _up to a point_.
+
+    However, if you don't understand how to correctly communicate type
+    annotations to the compiler, then all your efforts will be in
+    vain, which is why it's so important to understand how to read and
+    write dependent pattern matching type annotations in Rocq.
+
+    Thus, we turn to the details of dependent pattern matching.
+    *)


Type checking is decidable only if types are all given. If they are not given Rocq tries to infer what it can, but there is no guaranty.

thomas-lamiaux · 2025-04-05T16:26:40Z

src/Explanation_Induction.v

+(** Try the same trick here of looking at the return type using [refine]
+   to see how the context and return type changes inside the branches
+   [| tt => _ ] and [| ff => _ ]. *)
+
+Definition bool_induction :
+  forall P : bool -> Type,
+    P true -> P false -> forall b : bool, P b :=
+  fun P pf_tt pf_ff b =>
+  match b as b' return P b' with
+  | true => (* 1 *) pf_tt
+  | false => (* 2 *) pf_ff
+  end.


This part alternates between:

the weird def of is_even

vectors

nat

vectors

is_even

bool

That makes stuff non linear and confusing.

thomas-lamiaux · 2025-04-05T16:27:16Z

src/Explanation_Induction.v

+    But adding more annotations can help you get better error messages.
+    Once you get it to compile, you can try deleting the type
+    annotations and see if it still compiles.
+ *)


Add a section about nested inductive type like RoseTree

first draft

bd3fd5b

patrick-nicodemus changed the title ~~first draft~~ Explanation: Induction, pattern matching, fixed points Apr 3, 2025

SkySkimmer reviewed Apr 4, 2025

View reviewed changes

thomas-lamiaux reviewed Apr 5, 2025

View reviewed changes

Explanation: Induction, pattern matching, fixed points #86

Are you sure you want to change the base?

Explanation: Induction, pattern matching, fixed points #86

Uh oh!

Conversation

patrick-nicodemus commented Apr 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thomas-lamiaux commented Apr 3, 2025

Uh oh!

patrick-nicodemus commented Apr 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thomas-lamiaux commented Apr 3, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thomas-lamiaux commented Apr 5, 2025

Uh oh!

thomas-lamiaux left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

patrick-nicodemus commented Apr 3, 2025 •

edited

Loading

patrick-nicodemus commented Apr 3, 2025 •

edited

Loading