coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Stéphane Glondu <steph AT glondu.net>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Easy proofs complicated with reals
- Date: Fri, 27 Aug 2010 18:00:13 +0200
- Openpgp: id=49881AD3
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
- [Coq-Club] Easy proofs complicated with reals, Michael
- Re: [Coq-Club] Easy proofs complicated with reals, Evgeny Makarov
- <Possible follow-ups>
- Re: Re: [Coq-Club] Easy proofs complicated with reals,
Michael
- Re: [Coq-Club] Easy proofs complicated with reals, Stéphane Glondu
- Re: [Coq-Club] Easy proofs complicated with reals, Frédéric Besson
- Re: [Coq-Club] Easy proofs complicated with reals,
gallais @ EnsL
- Re: [Coq-Club] Easy proofs complicated with reals, Stéphane Glondu
- Re: [Coq-Club] Easy proofs complicated with reals, Stéphane Glondu
Archive powered by MhonArc 2.6.16.