The Coq mailing list

[Bruno Barras <Bruno.Barras AT cl.cam.ac.uk>]

Hello,

> I want to prove the following subgoal:
> 
> 1 subgoal
> 
>   n : nat
>   i : nat
>   HR : {m:nat | (i=(plus m m)\/i=(S (plus m m)))}
>   j : nat
>   I : i=(plus j j)\/i=(S (plus j j))
>   ============================
>    {m:nat | ((S i)=(plus m m)\/(S i)=(S (plus m m)))}
> 
> Trying "Elim I" produces: 
> 
> div2 < Elim I.
> Error during interpretation of command:
> Elim I.
> Error: or_rec not declared
> 
> How can I decompose the hypothesis "I"?

You cannot since I is a non-informative disjunction. This boolean information 
telling you if i is even or odd will be removed in the extraction process, so 
you cannot use it to build the result.

You are trying to prove a division by 2 algorithm. Here you are in the 
situation where you try to return  (S i) div 2  from the recursive call (HR)
 i div 2. As a programmer, you should quickly realize that it does not work 
and you have to generalize your function to keep track of the parity of i 
(computing it at every step would be very inefficient).

This means you also have to generalize your specification to make the parity 
*informative*. You can try and prove:

{ m:? | i=(plus m m)} + {m:? | i=(S (plus m m))}
  (* i is even *)            (* i is odd *)

And as a second step, you can easily prove your original specification using 
this one.

Another possibiliy is to make a deeper recursive call, since (S (S n)) div 2 
can be infered from  n div 2, but then you should not use Inductive or Elim 
tactics which only make direct structural induction. Use Fix instead.

Hope this helps,

Bruno Barras.

-----------------------------------------
e-mail: 
bruno.barras AT cl.cam.ac.uk
www:    http://www.cl.cam.ac.uk/~bb236/
tel:    +44 (1223) 334688
-----------------------------------------