diff options
| author | Gaëtan Gilbert | 2020-06-23 10:43:32 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-23 10:43:32 +0200 |
| commit | 34e62d05df4ecd833f87115aa0e986ef7626359e (patch) | |
| tree | 2bb09958d290286c59161547a3442865f50fa59c | |
| parent | 213999187d506394945a4d2163802b504be0c6ac (diff) | |
| parent | 9dc1f1fd48484b00d67871b6869a4c0c48e26f26 (diff) | |
Merge PR #8796: Elementary properties about IZR for generic use
Reviewed-by: SkySkimmer
| -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. |