The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear all,

I was doing a proof where I used

destruct (Nlt_ge_dec (i + j) (2 ^ 32)) as a tactic. Nlt_ge_dec is a definition of myself. It is defined as follows.

Definition Nlt_ge_dec:
   forall i j: N,
   { i < j } + { i >= j }.
intros i j.
unfold Nlt, Nge.
destruct (i ?= j); try (right; discriminate).
tauto.
Defined.

At the end of the proof I was doing, at the Qed Coq took forever to complete the Qed. Upon investiging this, I found that

Eval compute in (N.compare i (2 ^ 1)).

results in

     = match i with
       | 0%N => Lt
       | N.pos (_~1~1)%positive => Gt
       | N.pos (_~0~1)%positive => Gt
       | 3%N => Gt
       | N.pos (_~1~0)%positive => Gt
       | N.pos (_~0~0)%positive => Gt
       | 2%N => Eq
       | 1%N => Lt
       end
     : comparison

(8 patterns in the match)

Eval compute in (N.compare i (2 ^ 2)).

results in

     = match i with
       | 0%N => Lt
       | N.pos (_~1~1~1)%positive => Gt
       | N.pos (_~0~1~1)%positive => Gt
       | 7%N => Gt
       | N.pos (_~1~0~1)%positive => Gt
       | N.pos (_~0~0~1)%positive => Gt
       | 5%N => Gt
       | 3%N => Lt
       | N.pos (_~1~1~0)%positive => Gt
       | N.pos (_~0~1~0)%positive => Gt
       | 6%N => Gt
       | N.pos (_~1~0~0)%positive => Gt
       | N.pos (_~0~0~0)%positive => Gt
       | 4%N => Eq
       | 2%N => Lt
       | 1%N => Lt
       end
     : comparison

(16 patterns in the match).

This pattern continues.

At this point it is clear why the Qed never finishes. The most obvious solution would be to make Nlt_ge_dec opaque but this has the disadvantage that I lose some automatic simplifications that I was relying on. Another idea would be to wrap the 2^32 into a constant that is opaque but to keep a theorem around that states that the constant is equal to 2^32. This would probably work. Any other ideas what to do? I will keep looking for a solution myself as well and will report back if I find another one. Interstingly, I was using N instead of nat here in order to avoid such computational explosions but apparently they can still happen quite easily.

All the best,

Chris