The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Quoting frank maltman 
<frank.maltman AT googlemail.com>:

>
 The Div2 module seems somewhat underdeveloped (it only has one   
lemma *not* concerned with parity or double).

Hello Frank,

  In that module, there is a lemma that can be used in many situations,
since it gives you a specification of div2. In combination with even's  
decidability, you can prove a lot of properties.


Lemma even_odd_double :
  forall n,
    (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).



You infer a lemma of the same kind:

Lemma div2_sumbool : forall n, let p := div2 n in
                      {n = double p} + {n = S (double p)}.
Proof.
 intro n;destruct (even_odd_double n) as [H H0].
destruct (even_odd_dec n) as [e | o].
rewrite H in e;pattern n at 2;rewrite e;left;auto.
rewrite H0 in o;pattern n at 2;rewrite o;right;auto.
Qed.

This lemma can be used for instance for proving div2_le:

Lemma div2_le : forall n, div2 n <= n.
Proof.
intro n; case (div2_sumbool n);generalize (div2 n);intro p;
 intro H;rewrite H;unfold double;auto with arith.
Qed.

Pierre