[zify] Define zify in terms of tify_* tactics

restructure components (isolate tify,zify)

Author: fajb

subcomponents/lia.v

@@ -1,11 +1,3 @@
 From subcomponents Require ring.
+From subcomponents Require tify.
 From Stdlib Require micromega.Lia.
-From Stdlib Require micromega.SatDivMod.
-From Stdlib Require micromega.Zify.
-From Stdlib Require micromega.ZifyBool.
-From Stdlib Require micromega.ZifyClasses.
-From Stdlib Require micromega.ZifyComparison.
-From Stdlib Require micromega.ZifyInst.
-From Stdlib Require micromega.ZifyN.
-From Stdlib Require micromega.ZifyNat.
-From Stdlib Require micromega.ZifyPow.

subcomponents/tify.v

@@ -0,0 +1,12 @@
+From subcomponents Require integers.
+From subcomponents Require ring.
+From Stdlib Require micromega.Tify.
+From Stdlib Require micromega.Zify.
+From Stdlib Require micromega.SatDivMod.
+From Stdlib Require micromega.ZifyBool.
+From Stdlib Require micromega.ZifyClasses.
+From Stdlib Require micromega.ZifyComparison.
+From Stdlib Require micromega.ZifyInst.
+From Stdlib Require micromega.ZifyN.
+From Stdlib Require micromega.ZifyNat.
+From Stdlib Require micromega.ZifyPow.

test-suite/micromega/bug_18158.v

@@ -85,7 +85,7 @@ Goal forall x y ,
     -> Z.le (Z.shiftr y 8) 255
     -> Z.le (Z.shiftr x 24) 255.
   intros.
-  Zify.zify_saturate.
+  Tify.tify_saturate.
   (* [mp_lia zchecker] used to raise a [Stack overflow] error. It is supposed to fail normally. *)
   assert_fails (mp_lia zchecker).
 Abort.

test-suite/success/TifyZR.v

@@ -0,0 +1,86 @@
+From Stdlib Require Import Tify.
+From Stdlib Require Import ZifyClasses.
+From Stdlib Require Import Reals.
+From Stdlib Require Import Lra.
+(*  [zify] instances are already loaded *)
+
+Goal forall (y:nat),
+    (Z.of_nat y + 1)%Z = Z.of_nat (y + 1).
+Proof.
+  tify Z.
+  change ((Z.of_nat y + 1)%Z = (Z.of_nat y + 1)%Z).
+  reflexivity.
+Qed.
+
+Goal forall (y:nat),
+    (Z.of_nat y + 1)%Z = Z.of_nat (y + 1).
+Proof.
+  tify R. (* This is no known way to map to R, default to Z *)
+  change ((Z.of_nat y + 1)%Z = (Z.of_nat y + 1)%Z).
+  reflexivity.
+Qed.
+
+(* Define instances for R *)
+Lemma inj_IZR_iff : forall n m, n = m <-> (IZR n = IZR m)%R.
+Proof.
+  split.
+  apply f_equal.
+  apply eq_IZR.
+Qed.
+
+(* For the test, we lose the information that Z is discrete *)
+#[global]
+Instance Inj_Z_R : InjTyp Z R :=
+  mkinj _ _ IZR (fun x =>  True) (fun _ => I).
+Add Tify InjTyp Inj_Z_R.
+
+#[global]
+Instance Inj_nat_R : InjTyp nat R :=
+  mkinj _ _ INR (fun x =>  0 <= x)%R pos_INR.
+Add Tify InjTyp Inj_nat_R.
+
+#[global]
+Instance Inj_R_R : InjTyp R R :=
+  mkinj _ _ (fun x=> x) (fun x =>  True) (fun _ => I).
+Add Tify InjTyp Inj_R_R.
+
+#[global]
+Instance Op_eq_Z_R : BinRel (T:=R) (@eq Z) :=
+  { TR := @eq R ; TRInj := inj_IZR_iff }.
+Add Tify BinRel Op_eq_Z_R.
+
+#[global]
+Instance Op_plus_R : BinOp Z.add :=
+  { TBOp := Rplus; TBOpInj := plus_IZR }.
+Add Tify BinOp Op_plus_R.
+
+#[global]
+Instance Op_plus_nat_R : BinOp Nat.add :=
+  { TBOp := Rplus; TBOpInj := plus_INR }.
+Add Tify BinOp Op_plus_nat_R.
+
+#[global]
+Instance Op_Z_of_nat_R : UnOp (T1:= R) (T2:=R) Z.of_nat:=
+  { TUOp x := x ; TUOpInj x := eq_sym (INR_IZR_INZ x) }.
+Add Tify UnOp Op_Z_of_nat_R.
+
+#[global]
+Instance Op_S_R : UnOp (T1:= R) (T2:=R) S :=
+  { TUOp := (fun x => Rplus x 1) ; TUOpInj := S_INR  }.
+Add Tify UnOp Op_S_R.
+
+#[global]
+Instance Op_O : CstOp (T:= R)  O:=
+  { TCst := 0%R ; TCstInj := INR_0 }.
+Add Tify CstOp Op_O.
+
+Goal forall (y:nat),
+    (Z.of_nat y + 1)%Z = Z.of_nat (y + 1).
+Proof.
+  intros.
+  Fail lra. (* Does not reason over Z *)
+  Fail (tify Z; change ((INR y + 1)%R = (INR y + R1)%R)).
+  tify R.
+  change ((INR y + 1)%R = (INR y + R1)%R).
+  lra.
+Qed.

theories/Strings/PString.v

@@ -14,7 +14,7 @@ From Stdlib Require Import ZArith.
 
 #[local] Instance Op_max_length : ZifyClasses.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/SatDivMod.v

@@ -29,7 +29,7 @@ Instance SatDiv : Saturate Z.div :=
     PRes  := fun _ _ r => 0 <= r;
     SatOk := Z_div_nonneg_nonneg
   |}.
-Add Zify Saturate SatDiv.
+Add Tify Saturate SatDiv.
 
 #[global]
 Instance SatMod : Saturate Z.modulo :=
@@ -39,4 +39,4 @@ Instance SatMod : Saturate Z.modulo :=
     PRes  := fun _ _ r => 0 <= r;
     SatOk := Z_mod_nonneg_nonneg
   |}.
-Add Zify Saturate SatMod.
+Add Tify Saturate SatMod.

theories/micromega/Tify.v

@@ -0,0 +1,17 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+From micromega_plugin Require Export Tify.
+
+Ltac tify T:= intros;
+             tify_elim_let ;
+             tify_op T;
+             (tify_iter_specs) ;
+             tify_saturate.

theories/micromega/Zify.v

@@ -9,7 +9,7 @@
 (************************************************************************)
 
 From Stdlib Require Import ZifyClasses ZifyInst.
-From micromega_plugin Require Export Zify.
+From micromega_plugin Require Export Tify.
 
 (** [zify_pre_hook] and [zify_post_hook] are there to be redefined. *)
 Ltac zify_pre_hook := idtac.
@@ -30,9 +30,9 @@ Ltac zify_to_euclidean_division_equations :=
 
 Ltac zify := intros;
              zify_pre_hook ;
-             zify_elim_let ;
-             zify_op ;
-             (zify_iter_specs) ;
-             zify_saturate;
+             tify_elim_let ;
+             tify_op BinInt.Z;
+             (tify_iter_specs) ;
+             tify_saturate;
              zify_to_euclidean_division_equations ;
              zify_post_hook.

theories/micromega/ZifyBool.v

@@ -17,24 +17,24 @@ From Stdlib Require Import ZifyInst.
 Instance Inj_bool_bool : InjTyp bool bool :=
   { inj b := b ; pred b := b = true \/ b = false ;
     cstr b := ltac:(destruct b; tauto) }.
-Add Zify InjTyp Inj_bool_bool.
+Add Tify InjTyp Inj_bool_bool.
 
 (** Boolean operators *)
 
 #[global]
 Instance Op_andb : BinOp andb :=
   { TBOp := andb ; TBOpInj _ _ := eq_refl}.
-Add Zify BinOp Op_andb.
+Add Tify BinOp Op_andb.
 
 #[global]
 Instance Op_orb : BinOp orb :=
   { TBOp := orb ; TBOpInj _ _ := eq_refl}.
-Add Zify BinOp Op_orb.
+Add Tify BinOp Op_orb.
 
 #[global]
 Instance Op_implb : BinOp implb :=
   { TBOp := implb; TBOpInj _ _ := eq_refl }.
-Add Zify BinOp Op_implb.
+Add Tify BinOp Op_implb.
 
 Lemma xorb_eq b1 b2 : xorb b1 b2 = andb (orb b1 b2) (negb (eqb b1 b2)).
 Proof.
@@ -44,93 +44,93 @@ Qed.
 #[global]
 Instance Op_xorb : BinOp xorb :=
   { TBOp x y := andb (orb x y) (negb (eqb x y)); TBOpInj := xorb_eq }.
-Add Zify BinOp Op_xorb.
+Add Tify BinOp Op_xorb.
 
 #[global]
 Instance Op_eqb : BinOp eqb :=
   { TBOp := eqb; TBOpInj _ _ := eq_refl }.
-Add Zify BinOp Op_eqb.
+Add Tify BinOp Op_eqb.
 
 #[global]
 Instance Op_negb : UnOp negb :=
   { TUOp := negb ; TUOpInj _ := eq_refl}.
-Add Zify UnOp Op_negb.
+Add Tify UnOp Op_negb.
 
 #[global]
 Instance Op_eq_bool : BinRel (@eq bool) :=
   {TR := @eq bool ; TRInj b1 b2 := iff_refl (b1 = b2) }.
-Add Zify BinRel Op_eq_bool.
+Add Tify BinRel Op_eq_bool.
 
 #[global]
 Instance Op_true : CstOp true :=
   { TCst := true ; TCstInj := eq_refl }.
-Add Zify CstOp Op_true.
+Add Tify CstOp Op_true.
 
 #[global]
 Instance Op_false : CstOp false :=
   { TCst := false ; TCstInj := eq_refl }.
-Add Zify CstOp Op_false.
+Add Tify CstOp Op_false.
 
 (** Comparison over Z *)
 
 #[global]
 Instance Op_Zeqb : BinOp Z.eqb :=
   { TBOp := Z.eqb ; TBOpInj _ _ := eq_refl }.
-Add Zify BinOp Op_Zeqb.
+Add Tify BinOp Op_Zeqb.
 
 #[global]
 Instance Op_Zleb : BinOp Z.leb :=
   { TBOp := Z.leb; TBOpInj _ _ := eq_refl }.
-Add Zify BinOp Op_Zleb.
+Add Tify BinOp Op_Zleb.
 
 #[global]
 Instance Op_Zgeb : BinOp Z.geb :=
   { TBOp := Z.geb; TBOpInj _ _ := eq_refl }.
-Add Zify BinOp Op_Zgeb.
+Add Tify BinOp Op_Zgeb.
 
 #[global]
 Instance Op_Zltb : BinOp Z.ltb :=
   { TBOp := Z.ltb ; TBOpInj _ _ := eq_refl }.
-Add Zify BinOp Op_Zltb.
+Add Tify BinOp Op_Zltb.
 
 #[global]
 Instance Op_Zgtb : BinOp Z.gtb :=
   { TBOp := Z.gtb; TBOpInj _ _ := eq_refl }.
-Add Zify BinOp Op_Zgtb.
+Add Tify BinOp Op_Zgtb.
 
 (** Comparison over N *)
 
 #[global]
 Instance Op_Neqb : BinOp N.eqb :=
   { TBOp := Z.eqb; TBOpInj n m := ltac:(now destruct n, m) }.
-Add Zify BinOp Op_Neqb.
+Add Tify BinOp Op_Neqb.
 
 #[global]
 Instance Op_Nleb : BinOp N.leb :=
   { TBOp := Z.leb; TBOpInj n m := ltac:(now destruct n, m) }.
-Add Zify BinOp Op_Nleb.
+Add Tify BinOp Op_Nleb.
 
 #[global]
 Instance Op_Nltb : BinOp N.ltb :=
   { TBOp := Z.ltb; TBOpInj n m := ltac:(now destruct n, m) }.
-Add Zify BinOp Op_Nltb.
+Add Tify BinOp Op_Nltb.
 
 (** Comparison over positive *)
 
 #[global]
 Instance Op_Pos_eqb : BinOp Pos.eqb :=
   { TBOp := Z.eqb; TBOpInj _ _ := eq_refl }.
-Add Zify BinOp Op_Pos_eqb.
+Add Tify BinOp Op_Pos_eqb.
 
 #[global]
 Instance Op_Pos_leb : BinOp Pos.leb :=
   { TBOp := Z.leb; TBOpInj _ _ := eq_refl }.
-Add Zify BinOp Op_Pos_leb.
+Add Tify BinOp Op_Pos_leb.
 
 #[global]
 Instance Op_Pos_ltb : BinOp Pos.ltb :=
   { TBOp := Z.ltb; TBOpInj _ _ := eq_refl }.
-Add Zify BinOp Op_Pos_ltb.
+Add Tify BinOp Op_Pos_ltb.
 
 (** Comparison over nat *)
 
@@ -161,17 +161,17 @@ Qed.
 #[global]
 Instance Op_nat_eqb : BinOp Nat.eqb :=
   { TBOp := Z.eqb; TBOpInj := Z_of_nat_eqb_iff }.
-Add Zify BinOp Op_nat_eqb.
+Add Tify BinOp Op_nat_eqb.
 
 #[global]
 Instance Op_nat_leb : BinOp Nat.leb :=
   { TBOp := Z.leb; TBOpInj := Z_of_nat_leb_iff }.
-Add Zify BinOp Op_nat_leb.
+Add Tify BinOp Op_nat_leb.
 
 #[global]
 Instance Op_nat_ltb : BinOp Nat.ltb :=
   { TBOp := Z.ltb; TBOpInj := Z_of_nat_ltb_iff }.
-Add Zify BinOp Op_nat_ltb.
+Add Tify BinOp Op_nat_ltb.
 
 Lemma b2n_b2z x : Z.of_nat (Nat.b2n x) = Z.b2z x.
 Proof.
@@ -181,12 +181,12 @@ Qed.
 #[global]
 Instance Op_b2n : UnOp Nat.b2n :=
   { TUOp := Z.b2z; TUOpInj := b2n_b2z }.
-Add Zify UnOp Op_b2n.
+Add Tify UnOp Op_b2n.
 
 #[global]
 Instance Op_b2z : UnOp Z.b2z :=
   { TUOp := Z.b2z; TUOpInj _ := eq_refl }.
-Add Zify UnOp Op_b2z.
+Add Tify UnOp Op_b2z.
 
 Lemma b2z_spec b : (b = true /\ Z.b2z b = 1) \/ (b = false /\ Z.b2z b = 0).
 Proof.
@@ -197,7 +197,7 @@ Qed.
 Instance b2zSpec : UnOpSpec Z.b2z :=
   { UPred b r := (b = true /\ r = 1) \/ (b = false /\ r = 0);
     USpec := b2z_spec }.
-Add Zify UnOpSpec b2zSpec.
+Add Tify UnOpSpec b2zSpec.
 
 Ltac elim_bool_cstr :=
   repeat match goal with

theories/micromega/ZifyClasses.v

@@ -226,7 +226,7 @@ Proof.
   exact (fun H => proj2 IFF H).
 Qed.
 
-
+#[global] Set Warnings "-zify".
 
 (** Registering constants for use by the plugin *)
 Register eq_iff      as ZifyClasses.eq_iff.