Update theories/micromega/ZifyBool.v

Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>

- insert boolean constraint (b = true \/ b = false)
- add specs for b2z
- zify_post_hook performs a case-analysis over boolean constraints
- Stricter typing constraints for `zify` declared operators
  The type is syntactically checked against the declaration of injections.
  Some explicit casts may need to be inserted.

7 files changed, 111 insertions, 50 deletions

diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg
index ab0c3bed26..c00c9ecad4 100644
--- a/plugins/micromega/g_zify.mlg
+++ b/plugins/micromega/g_zify.mlg
@@ -28,9 +28,8 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
 | ["Add" "PropOp"    constr(t) ] -> { Zify.PropBinOp.register t }
 | ["Add" "PropBinOp"    constr(t) ] -> { Zify.PropBinOp.register t }
 | ["Add" "PropUOp"   constr(t) ] -> { Zify.PropUnOp.register t }
-| ["Add" "Spec"      constr(t) ] -> { Zify.Spec.register t }
-| ["Add" "BinOpSpec" constr(t) ] -> { Zify.Spec.register t }
-| ["Add" "UnOpSpec"  constr(t) ] -> { Zify.Spec.register t }
+| ["Add" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t }
+| ["Add" "UnOpSpec"  constr(t) ] -> { Zify.UnOpSpec.register t }
 | ["Add" "Saturate"  constr(t) ] -> { Zify.Saturate.register t }
 END
 
@@ -51,5 +50,5 @@ VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF
 |[ "Show" "Zify" "UnOp" ]   -> { Zify.UnOp.print () }
 |[ "Show" "Zify" "CstOp"]   -> { Zify.CstOp.print () }
 |[ "Show" "Zify" "BinRel"]  -> { Zify.BinRel.print () }
-|[ "Show" "Zify" "Spec"]    -> { Zify.Spec.print () }
+|[ "Show" "Zify" "Spec"]    -> { Zify.BinOpSpec.print () ; Zify.UnOpSpec.print()}
 END
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index fa7b4aa480..ec0f278326 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -45,9 +45,7 @@ let op_iff = lazy (zify "iff")
 let op_iff_morph = lazy (zify "iff_morph")
 let op_not = lazy (zify "not")
 let op_not_morph = lazy (zify "not_morph")
-
-(* identity function *)
-(*let identity = lazy (zify "identity")*)
+let op_True = lazy (zify "True")
 let whd = Reductionops.clos_whd_flags CClosure.all
 
 (** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map.
@@ -356,6 +354,7 @@ let specs_cache = ref HConstr.empty
 
 (** Each type-class gives rise to a different table.
     They only differ on how projections are extracted.  *)
+
 module EInj = struct
   open EInjT
 
@@ -366,6 +365,11 @@ module EInj = struct
   let cast x = InjTyp x
   let dest = function InjTyp x -> Some x | _ -> None
 
+  let is_cstr_true evd c =
+    match EConstr.kind evd c with
+    | Lambda (_, _, c) -> EConstr.eq_constr_nounivs evd c (Lazy.force op_True)
+    | _ -> false
+
   let mk_elt evd i (a : EConstr.t array) =
     let isid = EConstr.eq_constr_nounivs evd a.(0) a.(1) in
     { isid
@@ -373,7 +377,7 @@ module EInj = struct
     ; target = a.(1)
     ; inj = a.(2)
     ; pred = a.(3)
-    ; cstr = (if isid then None else Some a.(4)) }
+    ; cstr = (if is_cstr_true evd a.(3) then None else Some a.(4)) }
 
   let get_key = 0
 end
@@ -386,6 +390,28 @@ let get_inj evd c =
     failwith ("Cannot register term " ^ t)
   | Some a -> EInj.mk_elt evd c a
 
+let rec decomp_type evd ty =
+  match EConstr.kind_of_type evd ty with
+  | EConstr.ProdType (_, t1, rst) -> t1 :: decomp_type evd rst
+  | _ -> [ty]
+
+let pp_type env evd l =
+  Pp.prlist_with_sep (fun _ -> Pp.str " -> ") (pr_constr env evd) l
+
+let check_typ evd expty op =
+  let env = Global.env () in
+  let ty = Retyping.get_type_of env evd op in
+  let ty = decomp_type evd ty in
+  if List.for_all2 (EConstr.eq_constr_nounivs evd) ty expty then ()
+  else
+    raise
+      (CErrors.user_err
+         Pp.(
+           str ": Cannot register operator "
+           ++ pr_constr env evd op ++ str ". It has type " ++ pp_type env evd ty
+           ++ str " instead of expected type "
+           ++ pp_type env evd expty))
+
 module EBinOp = struct
   type elt = EBinOpT.t
 
@@ -398,7 +424,9 @@ module EBinOp = struct
     let i1 = get_inj evd a.(7) in
     let i2 = get_inj evd a.(8) in
     let i3 = get_inj evd a.(9) in
+    let bop = a.(6) in
     let tbop = a.(10) in
+    check_typ evd EInjT.[i1.source; i2.source; i3.source] bop;
     { source1 = a.(0)
     ; source2 = a.(1)
     ; source3 = a.(2)
@@ -408,7 +436,7 @@ module EBinOp = struct
     ; inj1 = i1
     ; inj2 = i2
     ; inj3 = i3
-    ; bop = a.(6)
+    ; bop
     ; tbop
     ; tbopinj = a.(11)
     ; classify_binop =
@@ -460,6 +488,7 @@ module EUnOp = struct
     let i1 = get_inj evd a.(5) in
     let i2 = get_inj evd a.(6) in
     let uop = a.(4) in
+    check_typ evd EInjT.[i1.source; i2.source] uop;
     let tuop = a.(7) in
     { source1 = a.(0)
     ; source2 = a.(1)
@@ -491,6 +520,7 @@ module EBinRel = struct
     let i = get_inj evd a.(3) in
     let brel = a.(2) in
     let tbrel = a.(4) in
+    check_typ evd EInjT.[i.source; i.source; EConstr.mkProp] brel;
     { source = a.(0)
     ; target = a.(1)
     ; inj = get_inj evd a.(3)
@@ -627,19 +657,32 @@ module ESat = struct
   let get_key = 1
 end
 
-module ESpec = struct
+module EUnopSpec = struct
   open ESpecT
 
   type elt = ESpecT.t
 
-  let name = "Spec"
+  let name = "UnopSpec"
   let table = specs
   let cast x = Spec x
   let dest = function Spec x -> Some x | _ -> None
-  let mk_elt evd i a = {spec = a.(5)}
+  let mk_elt evd i a = {spec = a.(4)}
   let get_key = 2
 end
 
+module EBinOpSpec = struct
+  open ESpecT
+
+  type elt = ESpecT.t
+
+  let name = "BinOpSpec"
+  let table = specs
+  let cast x = Spec x
+  let dest = function Spec x -> Some x | _ -> None
+  let mk_elt evd i a = {spec = a.(5)}
+  let get_key = 3
+end
+
 module BinOp = MakeTable (EBinOp)
 module UnOp = MakeTable (EUnOp)
 module CstOp = MakeTable (ECstOp)
@@ -647,7 +690,8 @@ module BinRel = MakeTable (EBinRel)
 module PropBinOp = MakeTable (EPropBinOp)
 module PropUnOp = MakeTable (EPropUnOp)
 module Saturate = MakeTable (ESat)
-module Spec = MakeTable (ESpec)
+module UnOpSpec = MakeTable (EUnopSpec)
+module BinOpSpec = MakeTable (EBinOpSpec)
 
 let init_cache () =
   table_cache := !table;
diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli
index 7960475def..537e652fd0 100644
--- a/plugins/micromega/zify.mli
+++ b/plugins/micromega/zify.mli
@@ -21,7 +21,8 @@ module CstOp : S
 module BinRel : S
 module PropBinOp : S
 module PropUnOp : S
-module Spec : S
+module BinOpSpec : S
+module UnOpSpec : S
 module Saturate : S
 
 val zify_tac : unit Proofview.tactic
diff --git a/theories/micromega/ZifyBool.v b/theories/micromega/ZifyBool.v
index d41ac6cf2f..2d2b137117 100644
--- a/theories/micromega/ZifyBool.v
+++ b/theories/micromega/ZifyBool.v
@@ -14,7 +14,8 @@ Local Open Scope Z_scope.
 (* Instances of [ZifyClasses] for dealing with boolean operators. *)
 
 Instance Inj_bool_bool : InjTyp bool bool :=
-  { inj := (fun x => x) ; pred := (fun x => True) ; cstr := (fun _ => I)}.
+  { inj := (fun x => x) ; pred := (fun b => b = true \/ b = false) ;
+    cstr := (ltac:(intro b; destruct b; tauto))}.
 Add InjTyp Inj_bool_bool.
 
 (** Boolean operators *)
@@ -45,6 +46,10 @@ Instance Op_xorb : BinOp xorb :=
     TBOpInj := xorb_eq }.
 Add BinOp Op_xorb.
 
+Instance Op_eqb : BinOp eqb :=
+  { TBOp := eqb; TBOpInj := ltac:(reflexivity) }.
+Add BinOp Op_eqb.
+
 Instance Op_negb : UnOp negb :=
   { TUOp := negb ; TUOpInj := ltac:(reflexivity)}.
 Add UnOp Op_negb.
@@ -65,6 +70,7 @@ Add CstOp Op_false.
 
 Instance Op_Zeqb : BinOp Z.eqb :=
   { TBOp := Z.eqb ; TBOpInj := ltac:(reflexivity)}.
+Add BinOp Op_Zeqb.
 
 Instance Op_Zleb : BinOp Z.leb :=
   { TBOp := Z.leb;
@@ -82,6 +88,7 @@ Instance Op_Zltb : BinOp Z.ltb :=
   { TBOp := Z.ltb ;
     TBOpInj := ltac:(reflexivity)
   }.
+Add BinOp Op_Zltb.
 
 Instance Op_Zgtb : BinOp Z.gtb :=
   { TBOp := Z.gtb;
@@ -137,3 +144,38 @@ Instance Op_nat_ltb : BinOp Nat.ltb :=
     TBOpInj := Z_of_nat_ltb_iff
   }.
 Add BinOp Op_nat_ltb.
+
+Lemma b2n_b2z :  forall x,  Z.of_nat (Nat.b2n x) = Z.b2z x.
+Proof.
+  intro.
+  destruct x ; reflexivity.
+Qed.
+
+Instance Op_b2n : UnOp Nat.b2n :=
+  { TUOp := Z.b2z;
+    TUOpInj := b2n_b2z }.
+Add UnOp Op_b2n.
+
+Instance Op_b2z : UnOp Z.b2z :=
+  { TUOp := Z.b2z;
+    TUOpInj := ltac:(reflexivity) }.
+Add UnOp Op_b2z.
+
+Lemma b2z_spec : forall b, (b = true /\ Z.b2z b = 1) \/ (b = false /\ Z.b2z b = 0).
+Proof.
+  destruct b ; simpl; intuition congruence.
+Qed.
+
+Instance b2zSpec : UnOpSpec Z.b2z :=
+  {| UPred := fun b r => (b = true /\ r = 1) \/ (b = false /\ r = 0);
+     USpec := b2z_spec
+  |}.
+Add UnOpSpec b2zSpec.
+
+Ltac elim_bool_cstr :=
+  repeat match goal with
+         | C : ?B = true \/ ?B = false |- _ =>
+           destruct C ; subst
+         end.
+
+Ltac Zify.zify_post_hook ::= elim_bool_cstr.
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index 65083791ca..37eef12381 100644
--- a/theories/micromega/ZifyClasses.v
+++ b/theories/micromega/ZifyClasses.v
@@ -90,15 +90,15 @@ Class PropUOp (Op : Prop -> Prop) :=
     NB1: The Ltac code is currently limited to (Op: Z -> Z -> Z)
     NB2: This is not sufficient to cope with [Z.div] or [Z.mod]
  *)
-Class BinOpSpec {S T: Type} (Op : T -> T -> T) {I : InjTyp S T} :=
+Class BinOpSpec {T1 T2 T3: Type} (Op : T1 -> T2 -> T3)  :=
   mkbspec {
-      BPred : T -> T -> T -> Prop;
+      BPred : T1 -> T2 -> T3 -> Prop;
       BSpec : forall x y, BPred x y (Op x y)
     }.
 
-Class UnOpSpec {S T: Type} (Op : T -> T) {I : InjTyp S T} :=
+Class UnOpSpec {T1 T2: Type} (Op : T1 -> T2)  :=
   mkuspec {
-      UPred : T -> T -> Prop;
+      UPred : T1 -> T2 -> Prop;
       USpec : forall x, UPred x (Op x)
     }.
 
@@ -220,8 +220,6 @@ Proof.
   exact (fun H => proj1 IFF H).
 Qed.
 
-Definition identity (A : Type) : A -> A := fun x => x.
-
 (** Registering constants for use by the plugin *)
 Register eq_iff      as ZifyClasses.eq_iff.
 Register target_prop as ZifyClasses.target_prop.
@@ -265,6 +263,4 @@ Register iff_morph as ZifyClasses.iff_morph.
 Register impl_morph as ZifyClasses.impl_morph.
 Register not as ZifyClasses.not.
 Register not_morph as ZifyClasses.not_morph.
-
-(** Identify function *)
-Register identity as ZifyClasses.identity.
+Register True as ZifyClasses.True.
diff --git a/theories/micromega/ZifyComparison.v b/theories/micromega/ZifyComparison.v
index 9b37f10841..b8d38adcc5 100644
--- a/theories/micromega/ZifyComparison.v
+++ b/theories/micromega/ZifyComparison.v
@@ -79,4 +79,4 @@ Instance ZcompareSpec : BinOpSpec ZcompareZ :=
                            /\
                            (x < y  -> r = -1)
               ; BSpec := Zcompare_spec|}.
-Add Spec ZcompareSpec.
+Add BinOpSpec ZcompareSpec.
diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v
index 5b15dc072a..e5d0312f3d 100644
--- a/theories/micromega/ZifyInst.v
+++ b/theories/micromega/ZifyInst.v
@@ -459,45 +459,24 @@ Add UnOp Op_Z_to_nat.
 
 (** Specification of derived operators over Z *)
 
-Lemma z_max_spec : forall n m,
-    n <= Z.max n m /\ m <= Z.max n m /\ (Z.max n m = n \/ Z.max n m = m).
-Proof.
-  intros.
-  generalize (Z.le_max_l n m).
-  generalize (Z.le_max_r n m).
-  generalize (Z.max_spec_le n m).
-  intuition idtac.
-Qed.
-
 Instance ZmaxSpec : BinOpSpec Z.max :=
   {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec|}.
-Add Spec ZmaxSpec.
-
-Lemma z_min_spec : forall n m,
-    Z.min n m <= n /\ Z.min n m <= m /\ (Z.min n m = n \/ Z.min n m = m).
-Proof.
-  intros.
-  generalize (Z.le_min_l n m).
-  generalize (Z.le_min_r n m).
-  generalize (Z.min_spec_le n m).
-  intuition idtac.
-Qed.
-
+Add BinOpSpec ZmaxSpec.
 
 Instance ZminSpec : BinOpSpec Z.min :=
   {| BPred := fun n m r => n < m /\ r = n \/ m <= n /\ r = m ;
      BSpec := Z.min_spec |}.
-Add Spec ZminSpec.
+Add BinOpSpec ZminSpec.
 
 Instance ZsgnSpec : UnOpSpec Z.sgn :=
   {| UPred := fun n r : Z => 0 < n /\ r = 1 \/ 0 = n /\ r = 0 \/ n < 0 /\ r = - (1) ;
      USpec := Z.sgn_spec|}.
-Add Spec ZsgnSpec.
+Add UnOpSpec ZsgnSpec.
 
 Instance ZabsSpec : UnOpSpec Z.abs :=
   {| UPred := fun n r: Z =>  0 <= n /\ r = n \/ n < 0 /\ r = - n ;
      USpec := Z.abs_spec|}.
-Add Spec ZabsSpec.
+Add UnOpSpec ZabsSpec.
 
 (** Saturate positivity constraints *)