The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>]

Roland Zumkeller wrote:
> Hi,
>
> You can verify the hypothesis that it's due to the guard condition
> with the command "Guarded", which checks the condition during a proof.

        Thanks, indeed Guarded confirms that it's the
guard condition check that is the problem.

        By the way, I could not find 'Guarded' in the
reference manual.  It might be a good idea to add a line
on this somewhere.

        Now, in fact, the problem seems to be that the
guardedness check destroys all sharing that existed
in terms.
        To be more concrete, I'm generating series of
lemmas (in fact Remarks), named rem_1, rem_2, etc.
        Each applies a rather elementary reasoning step,
using the previous remarks.
        Now, I'm going to do some elementary arithmetic
to illustrate the problem concretely.
Here is where it bogs down: rem_2421 states that:

Remark rem_2421 : (forall X:term, auto__q2 X -> auto__q1 X -> False)
    -> (forall X:term, auto__q2 X -> auto__q3 X -> False)
    -> (forall X:term, auto__q4 X -> auto__q2 X -> False)
    -> forall X1:term, auto__q4 X1 -> auto__q3 X1 -> False.

You may interpret this, by the way, as saying that there is
no term X1 accepted both at states q4 and q3 of some tree
automaton: e.g., auto__q4 X1 precisely means that X1 would
be accepted at q4.  The (forall X:term, <whatever>) are
induction hypotheses, which will be introduced by appropriate
uses of 'fix' later in the script.

        To prove rem_2421, my proof script first introes
the three induction hypotheses, then calls 'fix' to add
the goal as a new induction hypothesis.
        Now, it considers how you might prove
auto__q4 X1 -> auto__q3 X1 -> False
        so it does a case analysis on X1.
The type term is inductive, with 18 constructors,
so that makes 18 subcases.
        One of these, when X1=cons t t0, is:
forall t t0 : term,
   auto__q4 (cons t t0) -> auto__q3 (cons t t0) -> False

        This is dealt with in rem_1916.
        So now, we look at all possible ways that we can
have derived auto__q4 (cons t t0).  The automaton has 6
transitions labeled with cons leading to state q4, so
this one subgoal leads to 6 further subgoals.
        One of these is:
forall X1 X2:term,
   auto__q3 (cons X1 X2) -> auto__q3 X1 -> auto__q3 X2 -> False

        This is dealt with in rem_1891.
Again, we look at all possible ways that we can have derived
auto__q3 (cons X1 X2).  This leads to 6 subgoals again.
        One of these is:
forall X1 X2:term,
  auto__q3 X1 -> auto__q3 X2 -> auto__q4 X2 -> auto__q2 X1 -> False.

        This is dealt with in rem_1885.
Now the proof observes that the above is trivially
implied by one of the induction hypotheses,
namely forall X1:term, auto__q2 X1 -> auto__q3 X1 -> False.

        However, some of the generated subgoals need to
induct further.  Some of the remarks before rem_2421
need up to 5 stacked induction hypotheses, 2 more
than rem_2421 itself.
        Let me give a rough estimate.
        Based on the figures above, just one
induction will produce 18 x 6 x 6 = 648 subcases,
if 6 is about the typical number of transitions leading
to a state (I've seen at least one with 64 incoming
transitions).
        Two nested inductions will produce 648^2
~ 420 000 subcases.  Three will produce about 272 million.
        Note that three nested inductions is about
where it is stuck.  To complete the actual proof,
it would need to go to five nested inductions
(... because we are using five induction hypotheses
in the worst case here).  That would be about
10^14 subcases.

        However, note that most of these subcases
are the same.  At the point where I am stuck, even
though the reasoning above evaluated the number of
subcases to about 272 million, there
are at most 2421 *different* subcases (because each
different subcase is dealt with by a different rem_<n>,
and we are at rem_2421).
        At the end of the proof, even though we may
need about 10^14 subcases, the same
rough estimate shows that at most 79314 of them
are actually different.
        (Precisely, the 10^14, with all digits, is
114254951251968.  That may give a better mental image of
the problem.  Another way to state this is that, if
Coq spends 1 micro second to check each subcase, it
will need 3.62 years to explore all of them.  Not quite
undoable, though.)

        So, is there a way to have Coq understand
sharing while checking guard conditions?


        -- Jean Goubault-Larrecq
        (LSV/ENS Cachan & CNRS UMR 8643 & INRIA projet SECSI).