The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Sun, Jun 15, 2008 at 01:06:46PM +0200, Matthieu Sozeau wrote:
> Hello,
> 
> Le 15 juin 08 à 12:00, 
>Â frederic.blanqui AT loria.fr
>  a écrit :
> 
> >On Fri, 13 Jun 2008, 
>Â >frederic.blanqui AT loria.fr
> > wrote:
> >
> >>Hello. As it is well known, many function definitions are rejected  
> >>by Coq since they do not pass Coq termination checker which accepts  
> >>only structurally terminating functions. Would it be possible to  
> >>add a new command line option to coqc that would disable the  
> >>termination checker?
> >
> >Instead of a command line option, it would be better to have a  
> >command like "Unsafe Fixpoint" to disable the termination check  
> >locally and keep a trace of this in the file itself.
> 
> Actually, one would still need to tell on which argument to recurse,  
> as the reduction functions need this to decide when to unfold. So I  
> think a { general x } annotation would be the right way to do it. I'm  
> willing to make the change (I have a patch somewhere doing that  
> already), but maybe there are some arguments against it?


Humm...

It would be nice to have the opinion of "(in)coherence experts"
concerning this, but in the meantime I happened to had last Monday a
discussing with Colin Riba on that topic. He provided me an example
that strongly suggests that Bad Things May Happen very quickly with
the above ideas.

More precisely:

* It is common knowledge that having unguarded fixpoints of
unrestricted type kills not only the termination, but also the
coherence: take for instance ((fix bug (n:nat) : False := bug n) O).

* Now, the example mentionned to me by Colin shows that even ungarded
fixpoints of "friendly types" such as bool->bool can hurt a lot. 
Take:

Fixpoint bug (b : bool) : bool := negb (bug b).

Then, morally, (bug true) is equal to (negb (bug true)) by unfold of
the left occurrence of bug, whereas it's very easy to prove that 
(forall b:bool, b <> negb b), hence you have your contradiction.

I say "morally" above since I've actually tried to do it in Coq and
only almost succeeded (i.e. failed). First, killing the check of
fixpoints is really straightforward: for those would want to try, you
just have to bypass function check_fix in kernel/inductive.ml and make
sure this function always returns () immediately.

Then the following script becomes possible:

-----------------------------------------------------------------------
Fixpoint bug (b : bool) : bool := negb (bug b).

Lemma bug_eqn : forall b, b = true -> bug b = negb (bug b).
Proof.
intros.
pattern b at 1; rewrite H.
(* Note that you're now in a true minefield.
   All your favorite tactics diverge : unfold, rewrite, change, ... 
   We need to go low-level *)
lazy delta [bug].
lazy iota.
lazy beta.
remember true as b'. (* don't know why this work and not rewrite *)
rewrite H.
reflexivity.
Show Proof.
(* Qed.  *)(* Proof is actually finished for good ... but Qed diverges *)
Admitted.

Lemma negb_neq : forall b, b = negb b -> False.
Proof.
destruct b; discriminate.
Qed.

Lemma Bug : False.
Proof.
apply negb_neq with (bug true).
apply bug_eqn.
reflexivity.
Qed.
---------------------------------------------------------------------


As you can see, I haven't obtain rigorously a proof of False, but this
is only because Coq has diverged first. This isn't particularly
comfortable: maybe someone more clever could achieve this proof or
maybe benign changes in Coq could lead to acceptance of the above
script. Or maybe not.

Anyway, this example is far from solving all questions: 

* first, is it safe to add this way a truly terminating (but not
  structural) fixpoint this way ? I suppose yes, but even that is
  not clear, at least for me.

* Second, is it safe to add a non-terminating fixpoint that doesn't
  provide immediate contradiction in its equation as above ? For
  instance, what about (fix f (n:nat) : nat := f n) or 
  (fix g (n:nat) := g (S n)) ? 
  I would be tempted to think that something wrong is still going on,
  since you would have nat objects around that neither compute to O or
  (S _). But since they have no normal form, maybe we're only
  loosing termination.

With this kind of questions around, with the risk of ending on a
diverging Coq (see the comments in the script above), and with the
high probability of loosing coherence as well, I really don't think
it's a good idea to provide such an Unsafe Fixpoint feature by
default.

Best, 
Pierre Letouzey