Adapt to PR tify

This is the companion of https://github.com/fajb/coq/tree/tify
- Update the reflexive proof verifier for lia,lra etc.
- Define instances for the [rify] tactic (Require Import Rify)

test-suite/micromega/milp.v

@@ -0,0 +1,190 @@
+Require Import Rbase Rify isZ Lra Zfloor.
+Local Open Scope R_scope.
+
+Lemma up0 : up 0%R = 1%Z.
+Proof. intros. rify. lra. Qed.
+
+Lemma up_succ r : up (r + 1)%R = (up r + 1)%Z.
+Proof. intros. rify. lra. Qed.
+
+Lemma up_IZR z : up (IZR z) = (z + 1)%Z.
+Proof.
+  rify. lra.
+Qed.
+
+Lemma up_shiftz r z : up (r + IZR z)%R = (up r + z)%Z.
+Proof.
+  rify. lra.
+Qed.
+
+
+Lemma up_succ2 r n : Zfloor (r + IZR n) = (Zfloor r + n)%Z.
+Proof.
+  rify. lra.
+Qed.
+
+Goal forall x1 x2 x3  x5 x6
+    (H: -x2 > 0)
+    (H0: x3 >= 0)
+    (H1: -x1 + x5 + x6 = 0)
+    (H2: x1 + -x5 + x6 = 0)
+    (H4: -x1 > 0)
+    (H6: x2 + -x3 = 0)
+    (H7: 3 + 3*x1 = 0),
+    False.
+Proof.
+  intros.
+  lra.
+Qed.
+
+
+Lemma spurious_isZ : forall
+    (x l X : R)
+    (delta : R)
+    (iZ1    : isZ x)
+    (H13 :  - (X - l) <= 0)
+    (iZ2    : isZ X)
+    (H4 : l > 0)
+    (iZ2    : isZ X)
+    (H9 : delta / 2 <> 0)
+    (iZ2    : isZ X)
+    (H11 : 0 < delta / 2)
+    (iZ1    : isZ x)
+    (H10 : (X <= 0)),
+    False.
+Proof.
+  intros.
+  lra.
+Qed.
+
+Goal forall (k x:R) (P:Prop)
+            (Hyp : 0 <= k < 1)
+            (H2 : k < x < 1 /\ P)
+            (H3 : k < x < 1),
+  0 < x.
+Proof.
+  intros.
+  lra.
+Qed.
+
+
+  Ltac cnf := match goal with
+              | |- Tauto.cnf_checker  _ ?F _ = true =>
+                  let f:= fresh "f" in
+                  set(f:=F); compute in f; unfold f;clear f
+              end.
+
+  Ltac collect :=
+    match goal with
+      | |- context [ RMicromega.xcollect_isZ ?A ?B ?F] =>
+        let f := fresh "f" in
+        set (f:= RMicromega.xcollect_isZ A B F) ; compute in f ; unfold f; clear f
+    end.
+
+
+Goal forall (x y:R)
+    (H : x <= y)
+    (Hlt : x < y),
+    y - x = 0 -> False.
+Proof.
+  intros.
+  lra.
+Qed.
+
+Lemma two_x_1 : forall (x:R)
+            (IZ : isZ x)
+            (H : 2 * x + 1 =  0),
+    False.
+Proof.
+  intros.
+  lra.
+Qed.
+
+Goal forall x1 x2 x3 x4,
+    isZ x1 ->
+    isZ x2 ->
+    isZ x3 ->
+    isZ x4 ->
+    - x1 + x2 - x3 + x4 >= 0 ->
+    x1 - x2 + x3 - x4 + 1 > 0 ->
+    - x1 + x2 - x3 + x4  >  0 ->
+    False.
+Proof.
+  intros. lra.
+Qed.
+
+
+
+Goal forall z1 z2 z3, Zfloor (IZR z1 - IZR z2 + IZR z3)%R = (z1 - z2 + z3)%Z.
+Proof.
+  intros.
+  rify.
+  (** Now, some work over isZ *)
+  lra.
+Qed.
+
+Goal forall (z : Z) x, IZR z <= x -> (z <= Zfloor x)%Z.
+Proof.
+  rify.
+  lra.
+Qed.
+
+
+
+Goal forall (z : Z) x,  IZR z <= x < IZR z + 1 -> Zfloor x = z.
+Proof.
+  intros.
+  rify.
+  lra.
+Qed.
+
+
+Goal R1 + (R1 + R1) = 3.
+Proof.
+  intros.
+  rify.
+  reflexivity.
+Qed.
+
+Goal forall x,
+    x * 3 = 1 ->
+    False.
+Proof.
+  intros.
+  Fail lra.
+Abort.
+
+Goal forall x,
+    isZ x ->
+    x * 3 = 1 ->
+    False.
+Proof.
+  intros.
+  lra.
+Qed.
+
+
+
+Require Import Rfunctions R_sqrt.
+
+Goal forall e x
+            (He : 0 < e)
+            (ef := Rmin (e / (3 * (Rabs (x) + 1))) (sqrt (e / 3)) : R)
+            (H : sqrt (e / 3) > 0)
+            (H0 : 3 * (Rabs ( x) + 1) >= 1),
+            0 < ef.
+Proof.
+  intros.
+  rify. nra.
+Qed.
+
+
+Goal forall x v,
+            v * (3  * x) = 1 ->
+            x >= 1 ->
+            v = 1 / (3 * x).
+Proof.
+  intros.
+  rify. nra.
+Qed.
+

test-suite/output/MExtraction.v

@@ -57,11 +57,12 @@ Extract Constant Rinv   => "fun x -> 1 / x".
     extraction is only performed as a test in the test suite. *)
 Recursive Extraction
            Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
+           map_eFormula eFormula
            Tauto.abst_form
-           ZMicromega.cnfZ  ZMicromega.Zeval_const QMicromega.cnfQ
+           ZMicromega.cnfZ  ZMicromega.Zeval_const QMicromega.cnfQ RMicromega.cnfR
            List.map simpl_cone (*map_cone  indexes*)
            denorm QArith_base.Qpower vm_add
-   normZ normQ normQ Z.to_N N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+           normZ normQ (*normQ*) Z.to_N N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
 
 (* Local Variables: *)
 (* coding: utf-8 *)

test-suite/success/tify.v

@@ -0,0 +1,82 @@
+From Stdlib Require Import Reals.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import ZifyClasses Tify.
+
+(* Inject nat -> Z *)
+
+Instance Inj_nat_Z : InjTyp nat Z.
+Proof.
+  apply (mkinj _ _ Z.of_nat (fun x => (0 <= x)%Z)).
+  apply Nat2Z.is_nonneg.
+Defined.
+Add Tify InjTyp Inj_nat_Z.
+
+Instance Op_nat_add_Z : BinOp Nat.add.
+Proof.
+  apply mkbop with (TBOp := Z.add).
+  simpl. apply Nat2Z.inj_add.
+Defined.
+Add Tify BinOp Op_nat_add_Z.
+
+Instance Op_eq_nat_eq_Z : BinRel (@eq nat).
+Proof.
+apply mkbrel with (TR := @eq Z).
+simpl. split. congruence.
+apply Nat2Z.inj.
+Defined.
+Add Tify BinRel Op_eq_nat_eq_Z.
+
+
+(** Inject nat -> R *)
+
+Definition isZ (r:R) := IZR (Zfloor r) = r.
+
+Instance Inj_nat_R : InjTyp nat R.
+Proof.
+  apply (mkinj _ _ INR (fun r => isZ r /\ 0 <= r)).
+  - intros. split. unfold isZ.
+    rewrite INR_IZR_INZ.
+    rewrite ZfloorZ. reflexivity.
+    apply pos_INR.
+Defined.
+Add Tify InjTyp Inj_nat_R.
+
+Instance Op_add_R : BinOp Nat.add.
+Proof.
+  apply mkbop with (TBOp := Rplus).
+  simpl. intros. apply plus_INR.
+Defined.
+Add Tify BinOp Op_add_R.
+
+Instance Op_eq_nat_eq_R : BinRel (@eq nat).
+Proof.
+apply mkbrel with (TR := @eq R).
+simpl. split; intro. congruence.
+apply INR_eq; auto.
+Defined.
+Add Tify BinRel Op_eq_nat_eq_R.
+
+
+(* tify selects the right injection *)
+
+Goal forall (x y:nat), (x + y = y + x)%nat.
+Proof.
+  intros.
+  tify R.
+  apply Rplus_comm.
+Qed.
+
+Goal forall (x y:nat), (x + y = y + x)%nat.
+Proof.
+  intros.
+  tify Z.
+  apply Zplus_comm.
+Qed.
+
+(* The R instances do not break lia. *)
+From Stdlib Require Import Lia.
+Goal forall (x y:nat), (x + y = y + x)%nat.
+Proof.
+  intros.
+  lia.
+Qed.

theories/All/All.v

@@ -47,6 +47,7 @@ From Stdlib Require Export micromega.Lqa.
 From Stdlib Require Export micromega.Lra.
 From Stdlib Require Export micromega.OrderedRing.
 From Stdlib Require Export micromega.Psatz.
+From Stdlib Require Export micromega.MMicromega.
 From Stdlib Require Export micromega.QMicromega.
 From Stdlib Require Export micromega.RMicromega.
 From Stdlib Require Export micromega.Refl.
@@ -57,8 +58,10 @@ From Stdlib Require Export micromega.ZArith_hints.
 From Stdlib Require Export micromega.ZCoeff.
 From Stdlib Require Export micromega.ZMicromega.
 From Stdlib Require Export micromega.Zify.
+From Stdlib Require Export micromega.Tify.
 From Stdlib Require Export micromega.ZifyBool.
 From Stdlib Require Export micromega.ZifyClasses.
+From Stdlib Require Export micromega.TifyClasses.
 From Stdlib Require Export micromega.ZifyComparison.
 From Stdlib Require Export micromega.ZifyInst.
 From Stdlib Require Export micromega.ZifyN.
@@ -67,6 +70,8 @@ From Stdlib Require Export micromega.ZifyPow.
 From Stdlib Require Export micromega.ZifySint63.
 From Stdlib Require Export micromega.ZifyUint63.
 From Stdlib Require Export micromega.Ztac.
+From Stdlib Require Export micromega.isZ.
+From Stdlib Require Export micromega.Rify.
 From Stdlib Require Export funind.FunInd.
 From Stdlib Require Export funind.Recdef.
 From Stdlib Require Export extraction.ExtrHaskellBasic.

theories/Reals/RIneq.v

@@ -2522,6 +2522,9 @@ Qed.
 Lemma succ_IZR : forall n:Z, IZR (Z.succ n) = IZR n + 1.
 Proof. now intros n; unfold Z.succ; apply plus_IZR. Qed.
 
+Lemma pred_IZR : forall n:Z, IZR (Z.pred n) = IZR n - 1.
+Proof. now intros n; unfold Z.pred; apply plus_IZR. Qed.
+
 Lemma opp_IZR : forall n:Z, IZR (- n) = - IZR n.
 Proof.
   intros [| p | p]; unfold IZR; simpl.

theories/Strings/PString.v

@@ -12,9 +12,9 @@ From Stdlib Require Import ZArith.
 #[local] Open Scope list_scope.
 #[local] Arguments to_Z _/ : simpl nomatch.
 
-#[local] Instance Op_max_length : ZifyClasses.CstOp max_length :=
+#[local] Instance Op_max_length : TifyClasses.CstOp max_length :=
   { TCst := 16777211%Z ; TCstInj := eq_refl }.
-Add Zify CstOp Op_max_length.
+Add Tify CstOp Op_max_length.
 
 #[local] Ltac case_if :=
   lazymatch goal with

theories/micromega/Lia.v

@@ -1,3 +1,4 @@
+
 (************************************************************************)
 (*         *      The Rocq Prover / The Rocq Development Team           *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)

theories/micromega/Lra.v

@@ -29,7 +29,7 @@ Ltac rchange :=
   let __varmap := fresh "__varmap" in
   let __ff := fresh "__ff" in
   intros __wit __varmap __ff ;
-  change (Tauto.eval_bf (Reval_formula (@find R 0%R __varmap)) __ff) ;
+  change (Tauto.eval_bf (eReval_formula (@find R 0%R __varmap)) __ff) ;
   apply (RTautoChecker_sound __ff __wit).
 
 Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity.