The Coq mailing list

[Enrico Tassi <Enrico.Tassi AT inria.fr>]

On Tue, 2019-02-05 at 10:59 +0100, Norman Rink wrote:
> Dear Coq-club,
> 
> I am relatively new to Coq. While I feel comfortable with
> “pedestrian”-style Coq developments – by which I mean specifying
> comparably simply-typed functions in Gallina and proving theorems
> about these functions outside of the definitions – I am now trying to
> use Coq/Gallina more effectively by writing dependently-typed
> functions (hoping that this will save some outside-of-definitions
> proof effort).
> [cut]
> Any help or pointers would be greatly appreciated. Many thanks.

Another approach to tuples based on a very mild use of types depending
on values is described in chapter 6 of this draft:
  https://math-comp.github.io/mcb/
The main advantage is that you program and prove in a simply typed
setting (that you already master), and you later pack data and proofs
in order to obtain data with a richer type (this is what chapter 6 is
about).

You can find the corresponding .v in the math-comp library, see the
coqdoc here:
  http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.tuple
.html

My2C,
-- 
Enrico Tassi