The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/12/2014 08:10 AM, Ömer Sinan Ağacan wrote:
> Hi all,
>
> I'm having trouble implementing even the simplest dependently typed
> term using `Fixpoint`, `Definition` etc. I've been doing a lot of
> proving using tactics lately and I'm very comfortable with tactics. So
> I thought why not define everything using tactics? I came up with
> this:
>
> https://gist.github.com/osa1/47ed1dd4267fa379259d
>
> Now before coming to the problem with this, here's a few things: (see
> also generated OCaml link in the link above)
>
> * The whole thing looks a bit complex but actually implementing it was
> very, very easy. Definitely a lot easier than how it'd be if I wanted
> to implement it without tactics.

Another benefit is how the interaction while developing the proof script 
helps one write programs.

> * Even though generated Coq terms are huge, generated OCaml is
> actually very good. It still has some problems though. `snoc` has a
> redundant argument which could be eliminated by using OCaml lists for
> vectors. First argument of `sum-pairs` is redundant because it's just
> vector's length so we could use Vector.t's field instead. Similarly, I
> think `pascal_aux`'s first argument may also be removed etc.

It is possible to remove such things as well.  Some of this can be done 
using Coq's extraction options.  But, for others, it takes a more 
comprehensive form of erasability than Coq currently has built in.

> So I was actually happy with those definitions. But the problem is I
> can't prove even the simplest fact about those definitions. I think
> the reason is that `simpl.` no longer works.
>
> First I tried some simple `Eval simpl in ...` commands but none of
> them worked. I could compile OCaml files and run what I want just
> fine, but in Coq it just doesn't work.
>
> I tried `Eval compute in ...` but it just returned huge terms.
>
> I think because of that I can't prove anything. See my lemma in the
> link above. I should expect `simpl.` to make my goal `1 = 1`, but it
> just doesn't work.

Yes - if you define a function using tactics like simple induction, you 
probably won't want to see into the function at all via unfold, simpl, 
etc.  Such tactic-defined functions are often very large and unwieldy to 
work with, even if you could.   This leads to a different style of 
proving, where one has to make sure that the type of a function encodes 
everything interesting about it - so that the function can remain opaque 
(you could just use Qed instead of Defined).  This is not a style that 
everyone would appreciate, but it has other benefits.  As long as one 
considers the extracted OCaml program to be what is being developed, and 
not the Coq "Gallina code" itself.  It is also a more modular style of 
programming - because the only thing that depends on how a function is 
implemented is the function itself, not proofs about it (which depend 
only on the function's type).

The alternative is to learn about the "convoy pattern" that Adam 
Chlipala uses extensively in his CPDT book.  However, when I was reading 
(a draft of) that CPDT book, it was precisely because of the convoy 
pattern and what weakness of Coq it covers up that I gave up Coq and 
learned Agda.  I only came back to Coq when I realized I could use 
tactics to program effectively, use an added erasability feature to 
generate nice OCaml, and keep the types of functions sufficiently 
comprehensive that I never unfold/simpl/compute them within proofs.

By the way, inversion tactics use the convoy pattern themselves 
internally - they're just not very good about tailoring each usage of 
that pattern precisely to the specific need.

-- Jonathan