The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

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.
* 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.

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.

So I guess I paid the price of using tactics. This is actually very
sad, because 1) I never really understand how to define dependently
typed anything without tactics 2) Using tactics was really fun and
easy.

Now my question is that 1) why Coq can't [simpl] my terms? 2) is there
a way to fix this and make [simpl] working without changing
tactic-based definitions?

I'm also open to all kinds of suggestions on alternative ways of
defining those which allow me to prove stuff.

Thanks,

---
Ömer Sinan Ağacan
http://osa1.net