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.