Merge PR #9854: Improve field_simplify on fractions with constant denominator

Reviewed-by: MSoegtropIMC
Ack-by: Zimmi48
Reviewed-by: amahboubi
Reviewed-by: vbgl

9 files changed, 72 insertions, 11 deletions

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index f97e781832..95fceb773a 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -98,7 +98,8 @@
 # Coquelicot
 ########################################################################
 : "${coquelicot_CI_REF:=master}"
-: "${coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}"
+: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
+: "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}"
 
 ########################################################################
 # CompCert
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 33627fd8ef..6cb8dad604 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")"
 
 install_ssreflect
 
-FORCE_GIT=1
 git_download coquelicot
 
 ( cd "${CI_BUILD_DIR}/coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
diff --git a/dev/ci/nix/coquelicot.nix b/dev/ci/nix/coquelicot.nix
new file mode 100644
index 0000000000..d379bfa73d
--- /dev/null
+++ b/dev/ci/nix/coquelicot.nix
@@ -0,0 +1,9 @@
+{ autoconf, automake, ssreflect }:
+
+{
+  buildInputs = [ autoconf automake ];
+  coqBuildInputs = [ ssreflect ];
+  configure = "./autogen.sh && ./configure";
+  make = "./remake";
+  clean = "./remake clean";
+}
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 17070e66ee..a9cc91170f 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -72,6 +72,7 @@ let projects = {
   CoLoR = callPackage ./CoLoR.nix {};
   CompCert = callPackage ./CompCert.nix {};
   coq_dpdgraph = callPackage ./coq_dpdgraph.nix {};
+  coquelicot = callPackage ./coquelicot.nix {};
   Corn = callPackage ./Corn.nix {};
   cross_crypto = callPackage ./cross_crypto.nix {};
   Elpi = callPackage ./Elpi.nix {};
diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix
index e153043557..71028ec2dc 100644
--- a/dev/ci/nix/flocq.nix
+++ b/dev/ci/nix/flocq.nix
@@ -4,4 +4,5 @@
   buildInputs = [ autoconf automake ];
   configure = "./autogen.sh && ./configure";
   make = "./remake";
+  clean = "./remake clean";
 }
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 813c521ab0..ad2ee821b3 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1235,12 +1235,19 @@ Notation ring_correct :=
  (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th).
 
 (* simplify a field expression into a fraction *)
-(* TODO: simplify when den is constant... *)
 Definition display_linear l num den :=
-  NPphi_dev l num / NPphi_dev l den.
+  let lnum := NPphi_dev l num in
+    match den with
+    | Pc c => if ceqb c cI then lnum else lnum / NPphi_dev l den
+    | _ => lnum / NPphi_dev l den
+    end.
 
 Definition display_pow_linear l num den :=
-  NPphi_pow l num / NPphi_pow l den.
+  let lnum := NPphi_pow l num in
+    match den with
+    | Pc c => if ceqb c cI then lnum else lnum / NPphi_pow l den
+    | _ => lnum / NPphi_pow l den
+    end.
 
 Theorem Field_rw_correct n lpe l :
    Ninterp_PElist l lpe ->
@@ -1252,7 +1259,18 @@ Theorem Field_rw_correct n lpe l :
 Proof.
   intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
   rewrite (Fnorm_FEeval_PEeval _ _ H).
-  unfold display_linear; apply rdiv_ext;
+  unfold display_linear.
+  destruct (Nnorm _ _ _) as [c | | ] eqn: HN;
+  try ( apply rdiv_ext;
+        eapply ring_rw_correct; eauto).
+  destruct (ceqb_spec c cI).
+    set (nnum := NPphi_dev _ _).
+    apply eq_trans with (nnum / NPphi_dev l (Pc c)).
+      apply rdiv_ext;
+      eapply ring_rw_correct; eauto.
+    rewrite Pphi_dev_ok; try eassumption.
+    now simpl; rewrite H0, phi_1, <- rdiv1.
+  apply rdiv_ext;
   eapply ring_rw_correct; eauto.
 Qed.
 
@@ -1266,8 +1284,19 @@ Theorem Field_rw_pow_correct n lpe l :
 Proof.
   intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
   rewrite (Fnorm_FEeval_PEeval _ _ H).
-  unfold display_pow_linear; apply rdiv_ext;
-  eapply ring_rw_pow_correct;eauto.
+  unfold display_pow_linear.
+  destruct (Nnorm _ _ _) as [c | | ] eqn: HN;
+  try ( apply rdiv_ext;
+        eapply ring_rw_pow_correct; eauto).
+  destruct (ceqb_spec c cI).
+    set (nnum := NPphi_pow _ _).
+    apply eq_trans with (nnum / NPphi_pow l (Pc c)).
+      apply rdiv_ext;
+      eapply ring_rw_pow_correct; eauto.
+    rewrite Pphi_pow_ok; try eassumption.
+    now simpl; rewrite H0, phi_1, <- rdiv1.
+  apply rdiv_ext;
+  eapply ring_rw_pow_correct; eauto.
 Qed.
 
 Theorem Field_correct n l lpe fe1 fe2 :
diff --git a/test-suite/output/bug_9370.out b/test-suite/output/bug_9370.out
new file mode 100644
index 0000000000..0ff151c8b4
--- /dev/null
+++ b/test-suite/output/bug_9370.out
@@ -0,0 +1,12 @@
+1 subgoal
+  
+  ============================
+  1 = 1
+1 subgoal
+  
+  ============================
+  1 = 1
+1 subgoal
+  
+  ============================
+  1 = 1
diff --git a/test-suite/output/bug_9370.v b/test-suite/output/bug_9370.v
new file mode 100644
index 0000000000..a7f4b7c23e
--- /dev/null
+++ b/test-suite/output/bug_9370.v
@@ -0,0 +1,12 @@
+Require Import Reals.
+Open Scope R_scope.
+Goal 1/1=1.
+Proof.
+  field_simplify (1/1).
+Show.
+  field_simplify.
+Show.
+  field_simplify.
+Show.
+  reflexivity.
+Qed.
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
index 03e6ff61ab..38bed570a3 100644
--- a/theories/Reals/Ratan.v
+++ b/theories/Reals/Ratan.v
@@ -324,8 +324,6 @@ unfold cos_approx; simpl; unfold cos_term.
 rewrite !INR_IZR_INZ.
 simpl.
 field_simplify.
-unfold Rdiv.
-rewrite Rmult_0_l.
 apply Rdiv_lt_0_compat ; now apply IZR_lt.
 Qed.
 
@@ -1612,4 +1610,3 @@ Lemma PI_ineq :
 Proof.
 intros; rewrite <- Alt_PI_eq; apply Alt_PI_ineq.
 Qed.
-