Adapt to https://github.com/rocq-prover/stdlib/pull/207

theories/lra.v

@@ -1,6 +1,6 @@
 From mathcomp Require all_algebra. (* Remove this line when requiring Rocq > 9.1 *)
 From elpi Require Import elpi.
 From Coq Require Import BinNat QArith Ring.
 From Coq.micromega Require Import RingMicromega QMicromega EnvRing Tauto Lqa.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
 From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint.
@@ -94,17 +94,29 @@
 - by move=> ff1 IH1 ff2 IH2; congr eq.
 Qed.
 
+#[local] Notation nPEeval :=
+  ltac:(exact (EnvRing.PEeval (R_of_Z Z0) (R_of_Z (Zpos xH)) add mul sub opp
+                 R_of_Z id exp)
+        || exact (EnvRing.PEeval add mul sub opp R_of_Z id exp)) (only parsing).
+  (* Replace by LHS when requiring Rocq >= 9.2 *)
+
 Definition Reval_PFormula (e : PolEnv R) k (ff : Formula Z) : eKind k :=
-  let eval := EnvRing.PEeval add mul sub opp R_of_Z id exp e in
+  let eval := nPEeval e in
   let (lhs,o,rhs) := ff in Reval_op2 k o (eval lhs) (eval rhs).
 
 Lemma pop2_bop2 (op : Op2) (q1 q2 : R) :
   Reval_bop2 op q1 q2 <-> Reval_pop2 op q1 q2.
 Proof. by case: op => //=; rewrite eqPropE eqBoolE; split => /eqP. Qed.
 
+#[local] Notation neval_formula :=
+  ltac:(exact (eval_formula (R_of_Z Z0) (R_of_Z (Zpos xH)) add mul sub opp
+                 eqProp le lt R_of_Z id exp)
+        || exact (eval_formula add mul sub opp eqProp le lt R_of_Z id exp))
+  (only parsing).
+  (* Replace by LHS when requiring Rocq >= 9.2 *)
+
 Lemma Reval_formula_compat (env : PolEnv R) k (f : Formula Z) :
-  hold k (Reval_PFormula env k f) <->
-  eval_formula add mul sub opp eqProp le lt R_of_Z id exp env f.
+  hold k (Reval_PFormula env k f) <-> neval_formula env f.
 Proof.
 by case: f => lhs op rhs; case: k => /=; rewrite ?pop2_bop2; case: op.
 Qed.
@@ -211,17 +223,33 @@
 - by move=> ff1 IH1 ff2 IH2; congr eq.
 Qed.
 
+(* Remove the two lines below when requiring Rocq >= 9.2 *)
+#[local] Notation Q0 := (Qmake Z0 xH) (only parsing).
+#[local] Notation Q1 := (Qmake (Zpos xH) xH) (only parsing).
+
+#[local] Notation neval_pexpr :=
+  ltac:(exact (eval_pexpr (F_of_Q Q0) (F_of_Q Q1) add mul sub opp F_of_Q id exp)
+        || exact (eval_pexpr add mul sub opp F_of_Q id exp))
+  (only parsing).
+  (* Replace by LHS when requiring Rocq >= 9.2 *)
+
 Definition Feval_PFormula (e : PolEnv F) k (ff : Formula Q) : eKind k :=
-  let eval := eval_pexpr add mul sub opp F_of_Q id exp e in
+  let eval := neval_pexpr e in
   let (lhs,o,rhs) := ff in Feval_op2 k o (eval lhs) (eval rhs).
 
 Lemma pop2_bop2' (op : Op2) (q1 q2 : F) :
   Feval_bop2 op q1 q2 <-> Feval_pop2 op q1 q2.
 Proof. by case: op => //=; rewrite eqPropE eqBoolE; split => /eqP. Qed.
 
+#[local] Notation nFeval_formula :=
+  ltac:(exact (eval_formula (F_of_Q Q0) (F_of_Q Q1) add mul sub opp
+                 eqProp le lt F_of_Q id exp)
+        || exact (eval_formula add mul sub opp eqProp le lt F_of_Q id exp))
+  (only parsing).
+  (* Replace by LHS when requiring Rocq >= 9.2 *)
+
 Lemma Feval_formula_compat env b f :
-  hold b (Feval_PFormula env b f) <->
-  eval_formula add mul sub opp eqProp le lt F_of_Q id exp env f.
+  hold b (Feval_PFormula env b f) <-> nFeval_formula env f.
 Proof.
 by case: f => lhs op rhs; case: b => /=; rewrite ?pop2_bop2'; case: op.
 Qed.
@@ -242,6 +270,10 @@
 Definition Feval_nformula : PolEnv F -> NFormula Q -> Prop :=
   eval_nformula 0 +%R *%R eq (fun x y => x <= y) (fun x y => x < y) R_of_Q.
 
+(* Remove the two lines below when requiring Rocq >= 9.2 *)
+#[local] Notation Q0 := (Qmake Z0 xH) (only parsing).
+#[local] Notation Q1 := (Qmake (Zpos xH) xH) (only parsing).
+
 Lemma FTautoChecker_sound
     (ff : BFormula (RFormula F) isProp) (f : BFormula (Formula Q) isProp)
     (w : seq (Psatz Q)) (env : PolEnv F) :
@@ -255,14 +287,16 @@
 Proof.
 rewrite (Fnorm_bf_correct erefl erefl erefl erefl erefl erefl).
 move/(_ R_of_Q) => -> Hchecker.
+have RQ0 : R_of_Q Q0 = 0 :> F by rewrite /R_of_Q/= mul0r.
+have RQ1 : R_of_Q Q1 = 1 :> F by rewrite /R_of_Q/= divr1.
 move: Hchecker env; apply: (tauto_checker_sound _ _ _ _ Feval_nformula).
 - exact: (eval_nformula_dec Rsor).
 - by move=> [? ?] ? ?; apply: (check_inconsistent_sound Rsor FSORaddon).
 - move=> t t' u deducett'u env evalt evalt'.
   exact: (nformula_plus_nformula_correct Rsor FSORaddon env t t').
-- move=> env k t tg cnfff; rewrite Feval_formula_compat //.
+- move=> env k t tg cnfff; rewrite Feval_formula_compat // ?RQ0 ?RQ1.
   exact: (cnf_normalise_correct Rsor FSORaddon env t tg).1.
-- move=> env k t tg cnfff; rewrite hold_eNOT Feval_formula_compat //.
+- move=> env k t tg cnfff; rewrite hold_eNOT Feval_formula_compat // ?RQ0 ?RQ1.
   exact: (cnf_negate_correct Rsor FSORaddon env t tg).1.
 - move=> t w0 checkw0 env; rewrite (Refl.make_impl_map (Feval_nformula env)) //.
   exact: (checker_nf_sound Rsor FSORaddon) checkw0 env.
@@ -284,14 +318,28 @@
 Definition omap2 {aT1 aT2 rT} (f : aT1 -> aT2 -> rT) o1 o2 :=
   obind (fun a1 => omap (f a1) o2) o1.
 
-Fixpoint PExpr_Q2Z (e : PExpr Q) : option (PExpr Z) := match e with
-  | PEc (Qmake z 1) => Some (PEc z) | PEc _ => None
-  | PEX n => Some (PEX n)
-  | PEadd e1 e2 => omap2 PEadd (PExpr_Q2Z e1) (PExpr_Q2Z e2)
-  | PEsub e1 e2 => omap2 PEsub (PExpr_Q2Z e1) (PExpr_Q2Z e2)
-  | PEmul e1 e2 => omap2 PEmul (PExpr_Q2Z e1) (PExpr_Q2Z e2)
-  | PEopp e1 => omap PEopp (PExpr_Q2Z e1)
-  | PEpow e1 n => omap (PEpow ^~ n) (PExpr_Q2Z e1) end.
+Definition PExpr_Q2Z := ltac:(exact
+  (fix PExpr_Q2Z (e : PExpr Q) : option (PExpr Z) :=
+     match e with
+     | PEO => Some PEO | PEI => Some PEI
+     | PEc (Qmake z 1) => Some (PEc z) | PEc _ => None
+     | PEX n => Some (PEX _ n)
+     | PEadd e1 e2 => omap2 PEadd (PExpr_Q2Z e1) (PExpr_Q2Z e2)
+     | PEsub e1 e2 => omap2 PEsub (PExpr_Q2Z e1) (PExpr_Q2Z e2)
+     | PEmul e1 e2 => omap2 PEmul (PExpr_Q2Z e1) (PExpr_Q2Z e2)
+     | PEopp e1 => omap PEopp (PExpr_Q2Z e1)
+     | PEpow e1 n => omap (PEpow ^~ n) (PExpr_Q2Z e1) end)
+|| exact
+  (fix PExpr_Q2Z (e : PExpr Q) : option (PExpr Z) :=
+     match e with
+     | PEc (Qmake z 1) => Some (PEc z) | PEc _ => None
+     | PEX n => Some (PEX n)
+     | PEadd e1 e2 => omap2 PEadd (PExpr_Q2Z e1) (PExpr_Q2Z e2)
+     | PEsub e1 e2 => omap2 PEsub (PExpr_Q2Z e1) (PExpr_Q2Z e2)
+     | PEmul e1 e2 => omap2 PEmul (PExpr_Q2Z e1) (PExpr_Q2Z e2)
+     | PEopp e1 => omap PEopp (PExpr_Q2Z e1)
+     | PEpow e1 n => omap (PEpow ^~ n) (PExpr_Q2Z e1) end)).
+  (* Replace by LHS when requiring Rocq >= 9.2 *)
 
 Definition Formula_Q2Z (ff : Formula Q) : option (Formula Z) :=
   omap2

theories/ring.v

@@ -1,6 +1,6 @@
 From mathcomp Require all_algebra. (* Remove this line when requiring Rocq > 9.1 *)
 From elpi Require Import elpi.
 From Coq Require Import ZArith Ring Ring_polynom Field_theory.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
 From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint.
 From mathcomp.zify Require Import ssrZ zify.
@@ -251,6 +251,12 @@
     (Eqsth F) RE (congr1 GRing.inv) (F2AF (Eqsth F) RE (RF F)) (RZ F) (PN F)
     (triv_div_th (Eqsth F) RE (Rth_ARth (Eqsth F) RE (RR F)) (RZ F)).
 
+#[local] Notation nFcons00 :=
+  ltac:(exact (Fcons00 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb)
+        || exact (Fcons00 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb
+                    (triv_div 0 1 Z.eqb))) (only parsing).
+  (* Replace by LHS when requiring Rocq >= 9.2 *)
+
 Lemma field_correct (F : fieldType) (n : nat) (l : seq F)
                     (lpe : seq (RExpr F * RExpr F * PExpr Z * PExpr Z))
                     (re1 re2 : RExpr F) (fe1 fe2 : FExpr Z) :
@@ -285,9 +291,8 @@
                 (norm_subst' (PEmul (num nfe2) (denum nfe1))) /\
       is_true_ (PCond' true negb_ andb_
                        zero one add mul sub opp Feqb F_of_Z nat_of_N exp l'
-                       (Fapp (Fcons00 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb
-                                      (triv_div 0 1 Z.eqb))
-                             (condition nfe1 ++ condition nfe2) [::]))) ->
+                       (Fapp nFcons00
+                          (condition nfe1 ++ condition nfe2) [::]))) ->
   Reval re1 = Reval re2.
 Proof.
 move=> Hlpe' /(_ (fun n => (int_of_Z n)%:~R) 0%R -%R +%R (fun x y => x - y)).
@@ -305,6 +310,12 @@
     move=> _ ->; exact/PCondP ].
 Qed.
 
+#[local] Notation nFcons2 :=
+  ltac:(exact (Fcons2 0 1 Z.add Z.mul Z.sub Z.opp (pow_pos Z.mul) Z.eqb)
+        || exact (Fcons2 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb
+                    (triv_div 0 1 Z.eqb))) (only parsing).
+  (* Replace by LHS when requiring Rocq >= 9.2 *)
+
 Lemma numField_correct (F : numFieldType) (n : nat) (l : seq F)
                        (lpe : seq (RExpr F * RExpr F * PExpr Z * PExpr Z))
                        (re1 re2 : RExpr F) (fe1 fe2 : FExpr Z) :
@@ -339,9 +350,8 @@
                 (norm_subst' (PEmul (num nfe2) (denum nfe1))) /\
       is_true_ (PCond' true negb_ andb_
                        zero one add mul sub opp Feqb F_of_Z nat_of_N exp l'
-                       (Fapp (Fcons2 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb
-                                     (triv_div 0 1 Z.eqb))
-                             (condition nfe1 ++ condition nfe2) [::]))) ->
+                       (Fapp nFcons2
+                          (condition nfe1 ++ condition nfe2) [::]))) ->
   Reval re1 = Reval re2.
 Proof.
 move=> Hlpe' /(_ (fun n => (int_of_Z n)%:~R) 0%R -%R +%R (fun x y => x - y)).