Tutorial Equations: Indexed Inductive Types

[thomas-lamiaux]

A tutorial explaining how to use Equations to define functions on indexed inductive types and the particularities of reasoning about them

To do :

• Talk about the no confusion property for vec => find an example

[thomas-lamiaux]

@MevenBertrand at last CUDW we discuss how to finish this tutorial but I lost the notes. Could you check it out, and give some thought on how to complete it ? I think mostly the ideas was discussed derive / signature / no confusion and depelim which are currently not discussed

[MevenBertrand]

Isn't there a problem? The file called Tutorial_Equations_indexed.v on this branch looks like the Tutorial_Equations_wf.v of the well-founded induction tutorial? Or am I missing something?

But yeah, I believe the points you mentioned were the main ones. There is also the subterm relation, which one can derive and subsequently use for well-founded proofs. And maybe saying something about forced patterns as well? Here's the example from the manual:

Equations eqt {A} (x y z : A) (p : x = y) (q : y = z ) : x = z :=
eqt x ?(x) ?(x) eq refl eq refl := eq refl.

And finally might it make sense to mention how Equations can use UIP to make its life easier with indexed inductive types when the index type is an hSet?

[thomas-lamiaux]

@MevenBertrand I have fixed the file (if you want to look at it, it is currently rather short)

[MevenBertrand]

I gave it a quick look, a few remarks:

• your code currently does not work (there is a problem with vmap and friends used with the wrong implicit arguments, and a missing lemma vmap_congr)
• forced patterns already apply for the vector examples: in your first definition of vmap, if you look at the generated term it matches on n first, then v (and in each case uses no-confusion to discard the impossible branch); if you replace 0 with ?(0) and (S n) with ?(S n), though, you get the expected vmap. Apparently, this is the default behaviour for implicit arguments (ie this happens automatically for vmap').

Otherwise, it's going in the right direction, although it's still quite raw :) I can do a proper detailed review for small things, typos etc. when you've finished a first draft.

[thomas-lamiaux]

I have fixed the code.

• I don't know what to say about signature and depelim. Would you have some idea ?
• I don't know what to think about the difference between vmap and vmap' due to forcing

I'll do a more careful reading to clean tomorrow.

[MevenBertrand]

About depelim, I guess you can show how it is an improvement over similar tactics? There is an example in Basics.v of usage of depelim where inversion is not strong enough (because the goal depends on the eliminated variable) and leaves a bunch of terrible equalities around, destruct is also terrible (because the index is not a variable), and dependent inversion outright fails.

About signature, not sure what to say, maybe it's mostly a technical aspect that does not need to go into the manual.

About the difference between vmap and vmap', I'm not sure it's very relevant either. The extracted functions are going to be different, but in practice that's probably not very relevant anyway, the computational content is going to be basically similar (maybe if you make the definition transparent and apply it to a variable whose type is concrete, say x : Vect.t A 3 then things might become ugly?), and anyway you probably mainly want to interact with the definition through the propositional unfolding lemmas, which are going to be basically similar. So again, maybe it's not very important.

[palmskog]

To summarize my criticism of this tutorial as discussed in in the Zulip chat:

• "indexed inductive type" is not defined or explained in sufficient detail for (I believe) people to understand what this tutorial is about.
• the different kinds of "indexing" of inductive types in Coq (uniform parameters, parameters, indices, non-uniform parameters) is not discussed or exemplified.

It's also a bit surprising to me that the tutorial focuses on functions on vectors, even though using vectors is consistently recommended against for Coq beginners (Stdlib even has a warning these days).

I agree with Matthieu's suggestions here on the order to present concepts/examples.

[thomas-lamiaux]

@palmskog my understanding is that vectors are not recommended because without Equations to help you it is very painful to reason about them ? Which makes it a good example to me as it is also simple. But more importantly, what other example would you use ?

[thomas-lamiaux]

@mattam82 could you please suggest sth here ?

[mattam82]

It is derivable when diagonal constructor equalities C_i x1 .. xn = C_i y1 ... yn : I idx1 ... idxn are equivalent to $$\Sigma$$p1 : xk = yk, ... xl = yl where {k, ..., l} is the subset of non-forced arguments. Equivalence = type equivalence (as in the HoTT book). The type equivalence proof might depend on possibly already declared HSet proofs for the types of indices.

[mattam82]

Typically:

vcons A n a v = vcons A n a' v' : Vector.t A (S n) <-> 
{ eqn : n = n & eqa : a = a' & v # eqn = v' } <-> (* Need to make eqn disappear as it is forced by index (S n) *)
{ eqa : a = a' & v # eq_refl = v' } <-> (* nat has UIP, eqa : n = n = eq_refl n *)
a = a' : A  /\ v = v' :> Vector.t A n (* simplify *)

[spitters]

You may also want to point out the relation between depelim and dependent induction.
https://coq.inria.fr/doc/V8.18.0/refman/proofs/writing-proofs/reasoning-inductives.html#examples-of-dependent-destruction-dependent-induction
@mattam82 should know more about this.

[yannl35133]

Regarding part 2.2, I think it is easier and more useful to mostly introduce the lemmas Equations derive from the pov of where they are needed.

• Signature is needed for indexed inductive types, when you want to do pattern matching on them (through Equations or depelim)
• The NoConfusion family is for [inductive] types which appear as indices of a type we do pattern matching on
  • NoConfusionHom is the best case scenario, but it only works if, for all constructors, all arguments which appear in the indices do so in pattern position; in other words, NoConfusionHom does not record equalities of constructor arguments when they appear in the indices, but it needs to still imply equalities of the whole application
  • NoConfusion can always be generated, but using it requires UIP on its indices (specifically, only the indices where constructor arguments may appear)
• DepElim is the easiest way to prove UIP, but it's not complete

[mattam82]

I fixed quite a few things and added more examples of tactics. I think the "forced argument" explanation should be integrated somewhere but it's better for you to try it and I'll review it, to see if I managed to convey to you the idea or if it needs more explanations :)

[thomas-lamiaux]

@mattam82 don't expect me to write sth about forced arguments. I have read about it, and talked about it with people but I have the feeling that all the explanations I am getting are very handwavy. Sure, in practice I kind of get it, but until I see a proper definition in metacoq, I don't think I will really get it. So I think it is much better if you write sth small for it. I will review your PR, but I have already looked at it quickly, and it basiccaly looks good.

[mattam82]

@mattam82 don't expect me to write sth about forced arguments. I have read about it, and talked about it with people but I have the feeling that all the explanations I am getting are very handwavy. Sure, in practice I kind of get it, but until I see a proper definition in metacoq, I don't think I will really get it. So I think it is much better if you write sth small for it. I will review your PR, but I have already looked at it quickly, and it basiccaly looks good.

Alright, I gave it a go. I implemented your suggestions as well. Remaing the depelim/dependent elimination thing to sort out

[thomas-lamiaux]

Now is #75