Integrate Comments to Equations Tutorial Basics

[thomas-lamiaux]

Integrate Comments to Equations Tutorial Basics

• l16: no-confusion/subterm -> these are probably quite obscure for beginners (at least no-confusion), maybe you should explain more or drop it?
• l102: provided they can be inferred. For instance, above we wrote…
• l105: We can use underscores…
• l108: has constructors it is…
• l113: why the parentheses around the underscore? (here and other places)
• l135 the [Fixpoint] one -> the one provided by the [Fixpoint] command and Coq's native pattern-matching.
• l151: acceptable -> can be used interchangeably.
• l158: (n : nat ) -> (n : nat)
• l179: c.f -> c.f.
• l184: finish the proof, to show that you need to case-split on [n]?

case n as [|n'].
all: autorewrite with nth_option.
all: reflexivity.
Abort.

Also, at that point you pretend that this is about computation, but
autorewrite is propositional reasoning. That is, you would be able to add the new
derived equation to the nth_option hintbase:

Lemma nth_option_nil : forall {A} n, nth_option n (nil (A := A)) = None.
Proof.
  intros.
  case n ; now autorewrite with nth_option.
Qed.

Hint Rewrite @nth_option_nil : nth_option.

And now the first autorewrite goes through.
I'm not sure it is something you want to flash here, or even later, but it might confuse learners that you talk about computation…

• l187: on [a, …, a] -> on [a1, …, an]
• l194: is it intentional that map is filled, but not the other two? (It would make sense to me that you want to give at least one example, but force people to look for themselves in the other too, until we get a better set-up for exercises)
• l219: the functions -> functions, can not -> cannot (here and in other places)
• l245-246: Arguments is probably not precise enough to be able to say what one would want to say ("simplify exactly when the list of arguments matches one of the patterns of the definition"), but your proposed version is very aggressive. Usually, for app I'd rather do Arguments app !_ /. (which means "unfold app when it is applied to at least one argument and that argument is a constructor). There's also the simpl nomatch invocation, which I've never used but seems relevant…
• l266: mention how each equalities are named (it always takes me forever to find it again)? Although using the database is usually the sensible way to go, sometimes its useful to be able to summon the exact equality…
• l266: declares -> proves, and again below
• l266: in a database -> collected in a hint database
• l271: when doing in proof as compared to cbn the user … -> in proofs compared to cbn, as the user…
  Also, this is misleading: by using cbn [f1 … fn] one can obtain a similar behaviour. So it's maybe best not to mention this point at all.
• l277: uses -> use
• l278: We can similarly -> make this explicitly an exercise?
• l295: detruct
• l300: a more idiomatic way would be induction l in n |- * (although I know in the end you want to say "functional induction is better" anyway).
• l309: I'd say the important aspect is not that the inductive types can get more complicated (although they certainly can), but that the functions might not be simply following the structure of the types, without even talking about [with]/[where] clauses? Like in the most trivial example

Equations half (n : nat) : nat :=
  half 0 := 0 ;
  half 1 := 0 ;
  half (S (S n)) := S (half n).

• l311-313: maybe mention that this is called functional induction? Attempt:

Consequently, for each definition, [Equations] derives a functional induction
principle: this is an induction principle that follows the structure of the
function, including deep pattern-matching, [with] and [where] clauses,
correct induction hypotheses and generalisation as in the above example, etc.
This induction principle can be accessed by using the [funelim] tactic.

• l318: do your induction -> do the induction on (or better? induct on)
• l320: let's -> let us (here and other places)
• l352: to automatically simply by when -> use for automatic simplification
• l356: to make it automatic -> this way
• l358: by the syntax -> with the following syntax
  Maybe make it clear that this is not about Equations per se, but simply using the
  general rewriting hint mechanism of Coq?
• l360: name_function -> function_name
• l362: provides us with -> provides a
• l363-364: I would rephrase to

However, note that this mechanism is expressive enough to be
non-terminating if the wrong lemmas are added to the database.

• Add something as to the fact that the default lemmas are always safe, ie
  confluent and terminating?
• In general, I would replace "please note" with simply "note"
• l400: what is "it"?
• l404: I would rephrase to "… happens in such proofs by functional induction that
  after simplification we get a lot of uninteresting cases, that we would like to
  deal with in an automatic but controlled way."
• l409: a proof search by -> a proof search using
  "a particular instance" is rather vague, do you mean it uses try typeclasses eauto with … using a given set of hints? Then you should say so, mention what the databases are and what they do.
• l447: you are doing -> you want to do?
  (Good examples, especially app_nth2, I would never have thought about doing
  funelim (nth_option n l) despite nth_option n l appearing nowhere in my goal!)
• It is a bit weird to mention the useful lemmas but not import the corresponding files. And you might suggest using lia instead, which gets rid of these arithmetic goals without needing to find the right lemma.
• Maybe you should also mention somewhere that you can use simp in H and simp in * to also simplify in the hypotheses? This is useful in these exercises…
• Before 2: you do not have any example of a deep pattern-matching, as in the half example above. Maybe it would be useful to have something like this to show the power of funelim?
• l479: Agda -> dependently-typed programming community? (Ie Idris has it too for instance)
• l498: verify -> satisfy
• l532: |with] -> [with]
• l537: makes a subclause… -> does a case-split corresponding to the [with] clause?
• l539: the sentence is strange, attempt:

For [filter], in the [p a = true] case, a [filter_clause_1] appears, and
similarly in the [false] case.

• l541: [Equations] -> [Equations]'
• l541-544: I wonder whether this is an opportunity for polishing on the Equations side…
• l568: requiring for the input … different than -> requiring the input … different from
• l566: They can also be useful to… -> Finally, [with] clauses can be used to…
• l571: as -> has
• l604: your function -> your functions
• l625: using … -> using the usual [Equations] syntax/using [Equations]' usual syntax
• l651: maybe add some About rev_acc_elim. at this point so that we get to see what its type is?
• l656: exact … -> 1: exact … (I'm picky about goal selectors :p) (and below)
• l665: automatised -> automated
• l676: now you use simp in without having introduced it before!

[thomas-lamiaux]

@MevenBertrand can you elaborate on:

• what is the point of reasoning with rewrite than cbn according to you ?
• I wanted to be more specific about simp, but I have no idea what subterm and Below are

Also the behaviour of funelim should change soon, c.f. this comment #1 (comment)

[thomas-lamiaux]

Refactored 1.2 to adapt to the comments

[MevenBertrand]

what is the point of reasoning with rewrite than cbn according to you ?
I'm not sure I understand the question ^^'

I wanted to be more specific about simp, but I have no idea what subterm and Below are
These are hint databases used to respectively solve goals related to the subterm relation (whenever you Derive Subterm … various lemmas about that subterm relation are generated and added to the hint database), and well-foundedness assumption. If you want to know what is in a hint database, Print HintDb … is your friend :)

[thomas-lamiaux]

@MevenBertrand Could you check section 1.2 and tell me if you are satisfied by the modifications ?

[MevenBertrand]

Very nice addition of the examples for nested pattern-matching. Some more typo catches, but otherwise, lgtm :)

[thomas-lamiaux]

Merging now, thanks for the insight @MevenBertrand !