Extending rationalify_R_goal to support more variants of real constants.

This is to address the 8.7 change of representation of real constants.
coq-community · Dec 1, 2019 · b7ee061 · b7ee061
1 parent 50b7f8d
commit b7ee061
Showing 1 changed file with 20 additions and 2 deletions.
diff --git a/Q_to_R.v b/Q_to_R.v
@@ -728,6 +728,21 @@ Proof.
   repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ; unfold IZR, INR at 2; rewrite <- INR_IPR; field; auto.
 Qed.
 
+Lemma IZR_Zneg_Zpos : forall p, IZR (Zneg p) = Ropp (IZR (Zpos p)).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma IZR_Zpos_xO : forall p, IZR (Zpos (xO p)) = ((1+1) * (IZR (Zpos p)))%R.
+Proof.
+  intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial.
+Qed.
+
+Lemma IZR_Zpos_xI : forall p, IZR (Zpos (xI p)) = (1 + (1+1) * IZR (Zpos p))%R.
+Proof.
+  intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial.
+Qed.
+
 (** These tactics transfer hypotheses and goals from Q to R *)
 
 Ltac realify_Q_assumptions :=
@@ -764,8 +779,11 @@ Ltac rationalify_R_goal :=
  | [ |- context [(Rdiv (Q_to_R ?X1) (Q_to_R ?X2))] ] => rewrite <- Q_to_Rdiv; auto; rationalify_R_goal
  | [ |- context [(Ropp (Q_to_R ?X1)) ]] => rewrite <- Q_to_Ropp; rationalify_R_goal
  | [ |- context [(Rinv (Q_to_R ?X1))] ] => rewrite <- Q_to_Rinv; auto; rationalify_R_goal
- | [ |- context [R0] ] => rewrite <- Q_to_R_Zero; rationalify_R_goal
- | [ |- context [R1] ] => rewrite <- Q_to_R_Qone; rationalify_R_goal
+ | [ |- context [0%R] ] => rewrite <- Q_to_R_Zero; rationalify_R_goal
+ | [ |- context [1%R] ] => rewrite <- Q_to_R_Qone; rationalify_R_goal
+ | [ |- context [(IZR (Zneg ?X1))] ] => rewrite IZR_Zneg_Zpos; rationalify_R_goal
+ | [ |- context [(IZR (Zpos (xI ?X1)))] ] => rewrite IZR_Zpos_xI; rationalify_R_goal
+ | [ |- context [(IZR (Zpos (xO ?X1)))] ] => rewrite IZR_Zpos_xO; rationalify_R_goal
  | [ |- context [(IZR ?X1)] ] => rewrite <- Z_to_Q_to_R_IZR; realify_Q_goal
  | [ |- _ ] => idtac
  end.