The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

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.

You cannot compute with reals (at least the ones in Coq stdlib, which
are axiomatized). You have to use Z to perform the computation and use
properties of R to rewrite and simplify. It's quite painful indeed, but
here is a possibility:

Lemma powerRZ_inv :
  forall x, x <> 0 -> forall y, powerRZ x y = / powerRZ x (-y).
Proof.
  intros x Hx y.
  destruct y; simpl.
  rewrite Rinv_1; reflexivity.
  rewrite Rinv_involutive.
  reflexivity.
  apply pow_nonzero; assumption.
  reflexivity.
Qed.

Goal forall x, IZR 32 * powerRZ 2 (-5) * x = x.
Proof.
  intro x.
  rewrite powerRZ_inv, Zopp_neg.
  change (powerRZ 2 5) with (powerRZ (INR 2) (Z_of_nat 5)).
  rewrite <- Zpower_nat_powerRZ.
  rewrite Rinv_r.
  psatzl R.
  change 0 with (IZR 0); apply IZR_neq; discriminate.
  psatzl R.
Qed.

SearchAbout is absolutely needed to find lemmas in the stdlib (there are
so many of them about reals...) The first lemma looks like it should be
part of the standard library, but I didn't find it...


Cheers,

-- 
Stéphane