Prepare move of micromega_eval.v to Corelib

Author: proux01

test-suite/output/MExtraction.out

@@ -18,7 +18,7 @@
    Don't forget to update it in Rocq core when editing this MExtraction.v file
    or MExtraction.out *)
 
-From Stdlib Require Import micromega_checker.
+From Stdlib Require Import micromega_eval micromega_checker.
 From Stdlib Require Extraction.
 From Stdlib Require Import ZMicromega.
 From Stdlib Require Import QMicromega.
@@ -57,7 +57,7 @@ Extract Constant Rinv   => "fun x -> 1 / x".
 (** In order to avoid annoying build dependencies the actual
     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
+           Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula GFmap
            Tauto.abst_form
            ZMicromega.cnfZ  ZMicromega.Zeval_const QMicromega.cnfQ
            List.map simpl_cone (*map_cone  indexes*)

test-suite/output/MExtraction.v

@@ -11,7 +11,7 @@
    For big polynomials, this is inefficient -- linear access.
    I have modified the code to use binary trees -- logarithmic access.  *)
 
-From Stdlib Require Export micromega_formula micromega_witness.
+From Stdlib Require Export micromega_formula micromega_witness micromega_eval.
 From Stdlib Require Export micromega_checker.
 From Stdlib Require Import Setoid Morphisms Env BinPos BinNat BinInt.
 From Stdlib Require Export Ring_theory.
@@ -681,16 +681,8 @@ Qed.
 
  (** evaluation of polynomial expressions towards R *)
 
- Fixpoint PEeval (l:Env R) (pe:PExpr) : R :=
-   match pe with
-   | PEc c => phi c
-   | PEX j => nth j l
-   | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
-   | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2)
-   | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2)
-   | PEopp pe1 => - (PEeval l pe1)
-   | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n)
-   end.
+ #[local] Notation PEeval := (PEeval
+   radd rmul rsub ropp phi Cp_phi rpow (@nth R)).
 
  (** Correctness proofs *)
 
@@ -794,3 +786,6 @@ Section POWER.
  End NORM_SUBST_REC.
 
 End MakeRingPol.
+
+Notation PEeval := (fun add mul sub opp phi pow_phi pow => PEeval
+  add mul sub opp phi pow_phi pow (@Env.nth _)).

theories/micromega/EnvRing.v

@@ -64,31 +64,8 @@ Qed.
 (*Definition Zeval_expr :=  eval_pexpr 0 Z.add Z.mul Z.sub Z.opp  (fun x => x) (fun x => Z.of_N x) (Z.pow).*)
 From Stdlib Require Import EnvRing.
 
-Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q :=
-  match e with
-    | PEc c =>  c
-    | PEX j =>  env j
-    | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2)
-    | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
-    | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
-    | PEopp pe1 => - (Qeval_expr env pe1)
-    | PEpow pe1 n => Qpower (Qeval_expr env pe1)  (Z.of_N n)
-  end.
-
-Lemma Qeval_expr_simpl : forall env e,
-  Qeval_expr env e =
-  match e with
-    | PEc c =>  c
-    | PEX j =>  env j
-    | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2)
-    | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
-    | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
-    | PEopp pe1 => - (Qeval_expr env pe1)
-    | PEpow pe1 n => Qpower (Qeval_expr env pe1)  (Z.of_N n)
-  end.
-Proof.
-  destruct e ; reflexivity.
-Qed.
+#[local] Notation Qeval_expr := (PEeval
+  Qplus Qmult Qminus Qopp id Z.of_N Qpower).
 
 Definition Qeval_expr' := eval_pexpr  Qplus Qmult Qminus Qopp (fun x => x) (fun x => x) (pow_N 1 Qmult).
 
@@ -100,10 +77,9 @@ Qed.
 
 Lemma Qeval_expr_compat : forall env e, Qeval_expr env e = Qeval_expr' env e.
 Proof.
-  induction e ; simpl ; subst ; try congruence.
-  - reflexivity.
-  - rewrite IHe.
-    apply QNpower.
+  induction e ; simpl ; subst ; try congruence; try reflexivity.
+  rewrite IHe.
+  apply QNpower.
 Qed.
 
 Definition Qeval_pop2 (o : Op2) : Q -> Q -> Prop :=

theories/micromega/QMicromega.v

@@ -440,7 +440,7 @@ Definition Reval_formula' :=
 
 Lemma Reval_pop2_eval_op2 : forall o e1 e2,
   Reval_pop2 o e1 e2  <->
-  eval_op2 eq Rle Rlt o e1 e2.
+  eval_op2 isProp eq (fun x y => x <> y) Rle Rlt o e1 e2.
 Proof.
   destruct o ; simpl ; try tauto.
   split.
@@ -512,15 +512,15 @@ From Stdlib.micromega Require Import Tauto.
   Q0 Q1 Qplus Qmult Qminus Qopp Qeq_bool Qle_bool).
 
 Definition RTautoChecker (f : BFormula (Formula Rcst) isProp) (w: list RWitness)  : bool :=
-  micromega_checker.tauto_checker (fun cl => RWeakChecker (List.map fst cl)) (Qcnf_of_GFormula (map_bformula (map_Formula Q_of_Rcst) f)) w.
+  micromega_checker.tauto_checker (fun cl => RWeakChecker (List.map fst cl)) (Qcnf_of_GFormula (GFmap (Fmap Q_of_Rcst) f)) w.
 
 Lemma RTautoChecker_sound : forall f w, RTautoChecker f w = true -> forall env, eval_bf  (Reval_formula env)  f.
 Proof.
   intros f w.
   unfold RTautoChecker.
   intros TC env.
   apply tauto_checker_sound with (eval:=QReval_formula) (eval':=    Qeval_nformula) (env := env) in TC.
-  - change (eval_f e_eKind (QReval_formula env))
+  - change (GFeval eqb e_eKind (QReval_formula env))
       with
       (eval_bf  (QReval_formula env)) in TC.
     rewrite eval_bf_map in TC.

theories/micromega/RMicromega.v

@@ -490,22 +490,15 @@ Qed.
 
 (** Normalisation of formulae **)
 
-Definition eval_op2 (o : Op2) : R -> R -> Prop :=
-match o with
-| OpEq => req
-| OpNEq => fun x y : R => x ~= y
-| OpLe => rle
-| OpGe => fun x y : R => y <= x
-| OpLt => fun x y : R => x < y
-| OpGt => fun x y : R => y < x
-end.
+#[local] Notation eval_op2 := (eval_op2
+  isProp req (fun x y => ~ req x y) rle rlt).
 
 Definition  eval_pexpr : PolEnv -> PExpr C -> R :=
- PEeval rplus rtimes rminus ropp phi pow_phi rpow.
+ PEeval rplus rtimes rminus ropp phi pow_phi rpow (@Env.nth R).
 
-Definition eval_formula (env : PolEnv) (f : Formula C) : Prop :=
-  let (lhs, op, rhs) := f in
-    (eval_op2 op) (eval_pexpr env lhs) (eval_pexpr env rhs).
+#[local] Notation eval_formula := (Feval
+  rplus rtimes rminus ropp isProp req (fun x y => ~ req x y) rle rlt
+  phi pow_phi rpow (@Env.nth R)).
 
 (* We normalize Formulas by moving terms to one side *)
 
@@ -812,30 +805,14 @@ Variable phiS : S -> R.
 
 Variable phi_C_of_S :   forall c,  phiS c =  phi (C_of_S c).
 
-Fixpoint map_PExpr (e : PExpr S) : PExpr C :=
-  match e with
-    | PEc c => PEc (C_of_S c)
-    | PEX p => PEX p
-    | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2)
-    | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2)
-    | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2)
-    | PEopp e     => PEopp (map_PExpr e)
-    | PEpow e n   => PEpow (map_PExpr e) n
-  end.
-
-Definition map_Formula (f : Formula S)  : Formula C :=
-  let (l,o,r) := f in
-    Build_Formula (map_PExpr l) o (map_PExpr r).
-
-
 Definition eval_sexpr : PolEnv -> PExpr S -> R :=
-  PEeval rplus rtimes rminus ropp phiS pow_phi rpow.
+  PEeval rplus rtimes rminus ropp phiS pow_phi rpow (@Env.nth R).
 
 Definition eval_sformula (env : PolEnv) (f : Formula S) : Prop :=
   let (lhs, op, rhs) := f in
     (eval_op2 op) (eval_sexpr env lhs) (eval_sexpr env rhs).
 
-Lemma eval_pexprSC : forall env s, eval_sexpr env s = eval_pexpr env (map_PExpr s).
+Lemma eval_pexprSC : forall env s, eval_sexpr env s = eval_pexpr env (PEmap C_of_S s).
 Proof.
   unfold eval_pexpr, eval_sexpr.
   intros env s;
@@ -847,7 +824,7 @@ Proof.
 Qed.
 
 (** equality might be (too) strong *)
-Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f).
+Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (Fmap C_of_S f).
 Proof.
   intros env f; destruct f.
   simpl.
@@ -901,6 +878,11 @@ Notation padd := Padd (only parsing).
 Notation pmul := Pmul (only parsing).
 Notation popp := Popp (only parsing).
 
+Notation eval_formula :=
+  (fun add mul sub opp eqProp le lt phi pow_phi pow => Feval
+     add mul sub opp isProp eqProp (fun x y => ~ eqProp x y) le lt
+     phi pow_phi pow (@Env.nth _)).
+
 (* Local Variables: *)
 (* coding: utf-8 *)
 (* End: *)

theories/micromega/RingMicromega.v

@@ -14,7 +14,7 @@
 (*                                                                      *)
 (************************************************************************)
 
-From Stdlib Require Export micromega_formula micromega_witness.
+From Stdlib Require Export micromega_formula micromega_witness micromega_eval.
 From Stdlib Require Export micromega_checker.
 From Stdlib Require Import List.
 From Stdlib Require Import Refl.
@@ -29,6 +29,9 @@ Inductive Trace (A : Type) :=
 | merge : Trace A -> Trace A -> Trace A
 .
 
+#[local] Notation eIFF := (eIFF eqb).
+#[local] Notation eval_f := (GFeval eqb).
+
 Section S.
   Context {TA  : Type}. (* type of interpreted atoms *)
   Context {TX  : kind -> Type}. (* type of uninterpreted terms (Prop) *)
@@ -105,45 +108,7 @@ Section S.
 
     Variable ea : forall (k: kind), TA -> eKind k.
 
-    Definition eTT (k: kind) : eKind k :=
-      if k as k' return  eKind k' then True else true.
-
-    Definition eFF (k: kind) : eKind k :=
-      if k as k' return  eKind k' then False else false.
-
-    Definition eAND (k: kind) : eKind k -> eKind k -> eKind k :=
-      if k as k' return eKind k' -> eKind k' -> eKind k'
-      then and else andb.
-
-    Definition eOR (k: kind) : eKind k -> eKind k -> eKind k :=
-      if k as k' return eKind k' -> eKind k' -> eKind k'
-      then or else orb.
-
-    Definition eIMPL (k: kind) : eKind k -> eKind k -> eKind k :=
-      if k as k' return eKind k' -> eKind k' -> eKind k'
-      then (fun x y => x -> y) else implb.
-
-    Definition eIFF (k: kind) : eKind k -> eKind k -> eKind k :=
-      if k as k' return eKind k' -> eKind k' -> eKind k'
-      then iff else eqb.
-
-    Definition eNOT (k: kind) : eKind k -> eKind k :=
-      if k as k' return eKind k' -> eKind k'
-      then not else negb.
-
-    Fixpoint eval_f (k: kind) (f:GFormula k) {struct f}: eKind k :=
-      match f in micromega_formula.GFormula k' return eKind k' with
-      | TT tk => eTT tk
-      | FF tk => eFF tk
-      | A k a _ =>  ea k a
-      | X k p => ex  p
-      | @AND _ _ _ _ k e1 e2 => eAND k (eval_f  e1) (eval_f e2)
-      | @OR _ _ _ _ k e1 e2  => eOR k (eval_f e1) (eval_f e2)
-      | @NOT _ _ _ _ k e     => eNOT k (eval_f e)
-      | @IMPL _ _ _ _ k f1 _ f2 => eIMPL k (eval_f f1)  (eval_f f2)
-      | @IFF _ _ _ _ k f1 f2    => eIFF k (eval_f f1) (eval_f f2)
-      | EQ f1 f2    => (eval_f f1) = (eval_f f2)
-      end.
+    #[local] Notation eval_f := (eval_f ex ea).
 
     Lemma eval_f_rew : forall k (f:GFormula k),
         eval_f f =
@@ -164,7 +129,7 @@ Section S.
     Qed.
 
   End EVAL.
-
+  #[local] Notation eval_f := (eval_f ex).
 
   Definition hold (k: kind) : eKind k ->  Prop :=
     if k as k0 return (eKind k0 -> Prop) then fun x  => x else is_true.
@@ -259,37 +224,6 @@ Section S.
 
 End S.
 
-Section MAPATOMS.
-  Context {TA TA':Type}.
-  Context {TX  : kind -> Type}.
-  Context {AA  : Type}.
-  Context {AF  : Type}.
-
-  Fixpoint map_bformula (k: kind)(fct : TA -> TA') (f : @GFormula TA TX AA AF k) : @GFormula TA' TX AA AF k:=
-    match f with
-    | TT k => TT k
-    | FF k => FF k
-    | X k p => X k p
-    | A k a t => A k (fct a) t
-    | AND f1 f2 => AND (map_bformula fct f1) (map_bformula fct f2)
-    | OR f1 f2 => OR (map_bformula fct f1) (map_bformula fct f2)
-    | NOT f     => NOT (map_bformula fct f)
-    | IMPL f1 a f2 => IMPL (map_bformula fct f1) a (map_bformula fct f2)
-    | IFF f1 f2 => IFF (map_bformula fct f1) (map_bformula fct f2)
-    | EQ f1 f2  => EQ (map_bformula fct f1) (map_bformula fct f2)
-    end.
-
-End MAPATOMS.
-
-Lemma map_simpl : forall A B f l, @map A B f l = match l with
-                                                 | nil => nil
-                                                 | a :: l=> (f a) :: (@map A B f l)
-                                                 end.
-Proof.
-  intros A B f l; destruct l ; reflexivity.
-Qed.
-
-
 Section S.
   (** A cnf tracking annotations of atoms. *)
 
@@ -1871,7 +1805,7 @@ Section S.
           tauto.
   Qed.
 
-  Lemma tauto_checker_sound : forall t w, tauto_checker (@xcnf true isProp t) w = true -> forall env, @eval_f _ _ _ unit e_eKind (eval env) _ t.
+  Lemma tauto_checker_sound : forall t w, tauto_checker (@xcnf true isProp t) w = true -> forall env, @GFeval eqb _ _ _ unit e_eKind (eval env) _ t.
   Proof.
     unfold tauto_checker.
     intros t w H env.
@@ -1880,10 +1814,10 @@ Section S.
     eapply cnf_checker_sound ; eauto.
   Qed.
 
-  Definition eval_bf {A : Type} (ea : forall (k: kind), A -> eKind k) (k: kind) (f: BFormula A k) := eval_f e_eKind ea f.
+  #[local] Notation eval_bf := (BFeval eqb).
 
   Lemma eval_bf_map : forall T U (fct: T-> U) env (k: kind) (f:BFormula T k) ,
-      eval_bf env  (map_bformula fct f)  = eval_bf (fun b x => env b (fct x)) f.
+      eval_bf env  (GFmap fct f)  = eval_bf (fun b x => env b (fct x)) f.
   Proof.
     intros T U fct env k f;
       induction f as [| | | |? ? IHf1 ? IHf2|? ? IHf1 ? IHf2|? ? IHf
@@ -1894,6 +1828,7 @@ Section S.
 
 
 End S.
+Notation eval_bf := (BFeval eqb).
 
 Notation tauto_checker :=
   (fun term term' annot unsat deduce normalise negate witness check f =>

theories/micromega/Tauto.v

@@ -218,11 +218,11 @@ Proof.
   destruct f as [Flhs  Fop Frhs].
   repeat rewrite Zeval_expr_compat.
   unfold Zeval_formula' ; simpl.
-  unfold eval_expr.
-  generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
-        (fun x : N => x) (pow_N 1 Z.mul) env Flhs).
-  generalize ((eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
-        (fun x : N => x) (pow_N 1 Z.mul) env Frhs)).
+  unfold eval_expr, eval_pexpr.
+  generalize (micromega_eval.PEeval Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
+        (fun x : N => x) (pow_N 1 Z.mul) (@Env.nth Z) env Flhs).
+  generalize (micromega_eval.PEeval Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
+        (fun x : N => x) (pow_N 1 Z.mul) (@Env.nth Z) env Frhs).
   destruct Fop ; simpl; intros;
     intuition auto using Z.le_ge, Z.ge_le, Z.lt_gt, Z.gt_lt.
 Qed.
@@ -340,11 +340,11 @@ Proof.
   destruct f as [lhs o rhs].
   destruct o eqn:O ; cbn ; rewrite ?eval_pol_sub;
     rewrite <- !eval_pol_norm ; simpl in *;
-      unfold eval_expr;
-      generalize (   eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
-                                 (fun x : N => x) (pow_N 1 Z.mul) env lhs);
-      generalize (eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
-                              (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros z z0.
+      unfold eval_expr, eval_pexpr;
+      generalize (micromega_eval.PEeval Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
+                                 (fun x : N => x) (pow_N 1 Z.mul) (@Env.nth Z) env lhs);
+      generalize (micromega_eval.PEeval Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
+                              (fun x : N => x) (pow_N 1 Z.mul) (@Env.nth Z) env rhs); intros z z0.
   - split ; intros.
     + assert (z0 + (z - z0) = z0 + 0) as H0 by congruence.
       rewrite Z.add_0_r in H0.
@@ -1781,7 +1781,7 @@ Definition leaf := @VarMap.Elt Z.
 
 Definition coneMember := ZWitness.
 
-Definition eval := eval_formula.
+Definition eval := Feval.
 
 #[deprecated(note="Use [prod positive nat]", since="9.0")]
 Definition prod_pos_nat := prod positive nat.