The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

I've been trying to learn how to write dependently typed code in Coq.

As far as I can tell, there are three styles:

1. Use tactics to fill in Definition blocks.

2. Directly "implement" stuff with dependent types (like Idris)

3. Use Program to delay obligations, so write "normal" code and fulfil obligations later.

The problem I face with #1 is that _proving_ things about Definitions encoded this way is impossible for me. For example, if I use omega in some Definition D, I cannot prove anything about D, because on unfolding D, I see the mess that is the omega implementation, I assume.

So, for proving things about definitions, #1 is out.

#2 is.. challenging, and as a newbie, I find that I often do not know how to express the things I want to say, or do not know how to convince Coq that certain things are impossible (eg: safe indexing into a vector)

So, for now, #3 seems easiest.

I would like references on the third style of implementing things. Could someone please recommend reading material?

Thanks,

Siddharth

--

Sending this from my phone, please excuse any typos!