The Coq mailing list

[Fr�d�ric Besson <frederic.besson AT inria.fr>]

On 27 août 2010, at 18:00, Stéphane Glondu wrote:

> Le 27/08/2010 12:20, Michael a écrit :
>> The tactic psatzl is working fine, thank you for that hint.
>> 
>> I'm still having some other problems, which seem (with regard to the 
>> content)
>> simple. I think it's a problem about type conversion:
>> I'd like to calculate (or actually replace) (IZR 32 * powerRZ 2 (-5) * x) 
>> with
>> simply x. However, I don't succeed in converting the two parts in such a 
>> way
>> that i can reduce them to get "x" alone.
Here is a fairly automatic way of discharging this goal.
Ltac apply_Rinv_r X :=
   generalize (Rinv_r X) ; generalize (Rinv X) ; intros.

Ltac elim_inv :=
 repeat 
 match goal with
   |  H : context[ Rinv ?X] |-  _ => apply_Rinv_r X
   |  |-  context[ Rinv ?X]  => apply_Rinv_r X
 end.


Goal forall (x:R), ( IZR 32 * powerRZ 2 (-5) * x = x)%R.
Proof.
 intros.
 assert (   IZR 32 * powerRZ 2 (-5) = 1).
  compute.  elim_inv. psatzl R.
 rewrite H.
 psatzl R.
Qed.

--
Frédéric