diff options
| author | Hugo Herbelin | 2018-10-22 22:38:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-06-22 17:44:13 +0200 |
| commit | 9dc1f1fd48484b00d67871b6869a4c0c48e26f26 (patch) | |
| tree | ff8c8b9895aac529bd248b122013ef88cfee7f7e | |
| parent | b34680b8d23025ba083854800438bf0e7b092de2 (diff) | |
Elementary properties about IZR for generic use.
| -rw-r--r-- | theories/Reals/RIneq.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 33e40a115b..4fa8b3216a 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1774,6 +1774,28 @@ Proof. now rewrite <- INR_IPR, SuccNat2Pos.id_succ. Qed. +Lemma IZR_NEG : forall p, IZR (Zneg p) = Ropp (IZR (Zpos p)). +Proof. + reflexivity. +Qed. + +(** The three following lemmas map the default form of numerical + constants to their representation in terms of the axioms of + [R]. This can be a useful intermediate representation for reifying + to another axiomatics of the reals. It is however generally more + convenient to keep constants represented under an [IZR z] form when + working within [R]. *) + +Lemma IZR_POS_xO : forall p, IZR (Zpos (xO p)) = (1+1) * (IZR (Zpos p)). +Proof. + intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial. +Qed. + +Lemma IZR_POS_xI : forall p, IZR (Zpos (xI p)) = 1 + (1+1) * IZR (Zpos p). +Proof. + intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial. +Qed. + Lemma plus_IZR_NEG_POS : forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q). Proof. |