The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

[long post ahead]

I just learned an interesting lesson about writing decision
procedures using reflection in Coq.  It's probably one that others have
encountered before - so "tl;dr" if this is a familiar refrain: functions
used within reflection procedures are not the only elements where
transparency (Defined vs. Qed) needs to be considered.  Atoms matter,
too.


Suppose some of the atoms (hypotheses of the target goal, or terms
in the target goal that are not in the reified domain of the reflection
procedure) have inductive types.  In my case, some are lists.  Then,
in order to prove certain subgoals within the reflection code itself,
one may use theorems about that inductive type.  In my case, I needed
the simple app_nil_end theorem that "forall (l:list A), l = l ++ []".
But, things can go wrong when using such a theorem at the wrong time.
The problem is that, even if app_nil_end (and app_nil_r, on which it
is based) is made transparent, it still needs to match on l. And if l is
an atom, then for the purposes of the reflection procedure, l is opaque.
Attempts to run such a reflection procedure will block on that match if
it is in the execution path. That doesn't mean that one cannot use a
function like app_nil_end on l if l is an atom, just that such uses
should be confined to non-executing parts of the reflection procedure.

Admitttedly, I probably should have thought a bit more about what it
really means to need a function like app_nil_end (and app_nil_r) to be
transparent, instead of thoughtlessly making a transparent copy in each
such case. There is something about app_nil_end's type that suggests
that it should never be involved in computing.  I think this is roughly
that it's a pure "shortcut" for the append function.  If a computation
really does have transparent lists available to append, it wouldn't need
app_nil_end - it would instead compute the append of nil and get the
desired result.  So app_nil_end's entire purpose is for use in those
cases where such computation (reduction of append) isn't possible or
preferable.

But if I had kept app_nil_end (and app_nil_r) opaque, and then still had
made the mistake of using app_nil_end in the wrong place, the result is
a failure of the reflection procedure that is very difficult to debug.
One can examine the term returned by the reflection procedure on a
test case that fails to see where it fails to reduce. This is so tedious
to do by hand for large terms that I was considering writing an Ltac
tactic to automate it.  And, one needs test cases that cover all
possible execution paths.  Which frankly sounds quite a bit like test
suites in non-certified software development.

These issues with transparency point out a false sense of security
offered by writing a reflection procedure in Gallina and having it
type check.  Type checking proves that it's correct in a way, much more
so than what one could achieve by writing a decision procedure entirely
in Ltac (or even Ltac2), but that way is still limited.  The decision
procedure's safety and termination are proven, but not its progress.
It may block during reduction for the above reasons, and that is a bug.

It would be nice if Coq could provide some assistance about whether the
current goal is in the "reduction path" of the function being defined,
which hypotheses in that goal are reducible (transparent), and whether
a non-transparent hypothesis will block reduction (because certain
arguments of transparent functions need to themselves be transparent).
After all, Coq does other checks that seem similar in feel to this:
guardedness, positivity, preventing Prop instances from being
informative (destructable) at the wrong times, making sure matches
cover all possibilities. These are all similar in that, locally, things
may type check, but more globally they are still not correct in some
way.