Merge PR #10207: Partly revert micromega parsing using typeclasses.

Reviewed-by: vbgl

10 files changed, 277 insertions, 138 deletions

diff --git a/plugins/micromega/DeclConstant.v b/plugins/micromega/DeclConstant.v
index 47fcac6481..4e8fe5a8ff 100644
--- a/plugins/micromega/DeclConstant.v
+++ b/plugins/micromega/DeclConstant.v
@@ -62,6 +62,7 @@ Instance DZO: DeclaredConstant Z0 := {}.
 Instance DZpos: DeclaredConstant Zpos := {}.
 Instance DZneg: DeclaredConstant Zneg := {}.
 Instance DZpow_pos : DeclaredConstant Z.pow_pos := {}.
+Instance DZpow     : DeclaredConstant Z.pow     := {}.
 
 Require Import QArith.
 
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 6112eda200..830cbdf7f6 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -55,7 +55,7 @@ Extract Constant Rinv   => "fun x -> 1 / x".
     extraction is only performed as a test in the test suite. *)
 (*Extraction "micromega.ml"
            Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
-           ZMicromega.cnfZ ZMicromega.bound_problem_fr QMicromega.cnfQ
+           ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ
            List.map simpl_cone (*map_cone  indexes*)
            denorm Qpower vm_add
    normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index ab218a1778..953690c510 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -75,6 +75,21 @@ Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z :=
 
 Definition eval_expr := eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x => x) (pow_N 1 Z.mul).
 
+Fixpoint Zeval_const  (e: PExpr Z) : option Z :=
+  match e with
+  | PEc c => Some c
+  | PEX _ x => None
+  | PEadd e1 e2 => map_option2 (fun x y => Some (x + y))
+                               (Zeval_const e1) (Zeval_const e2)
+  | PEmul e1 e2 => map_option2 (fun x y => Some (x * y))
+                               (Zeval_const e1) (Zeval_const e2)
+  | PEpow e1 n  => map_option (fun x => Some (Z.pow x (Z.of_N n)))
+                                 (Zeval_const e1)
+  | PEsub e1 e2 => map_option2 (fun x y => Some (x - y))
+                               (Zeval_const e1)  (Zeval_const e2)
+  | PEopp e   => map_option (fun x => Some (Z.opp x)) (Zeval_const e)
+  end.
+
 Lemma ZNpower : forall r n, r ^ Z.of_N n = pow_N 1 Z.mul r n.
 Proof.
   destruct n.
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index de9dec0f74..bed9e55ac0 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -346,7 +346,9 @@ struct
   let coq_PsatzC  = lazy (constant "PsatzC")
   let coq_PsatzZ    = lazy (constant "PsatzZ")
 
-  let coq_GT     = lazy (m_constant "GT")
+  (*  let coq_GT     = lazy (m_constant "GT")*)
+
+  let coq_DeclaredConstant = lazy (m_constant "DeclaredConstant")
 
   let coq_TT = lazy
    (gen_constant_in_modules "ZMicromega"
@@ -462,13 +464,24 @@ struct
       what to consider as a constant (see [parse_constant])
    *)
 
-  let is_ground_term env sigma term =
-    let typ =     Retyping.get_type_of env sigma term in
-    try
-    ignore (Typeclasses.resolve_one_typeclass env sigma (EConstr.mkApp(Lazy.force coq_GT,[| typ;term|]))) ;
-      true
-    with
-    | Not_found -> false
+  let is_declared_term env evd t =
+    match EConstr.kind evd t with
+    | Const _ | Construct _ -> (* Restrict typeclass resolution to trivial cases *)
+       begin
+       let typ = Retyping.get_type_of env evd t in
+       try
+         ignore (Typeclasses.resolve_one_typeclass env evd (EConstr.mkApp(Lazy.force coq_DeclaredConstant,[| typ;t|]))) ; true
+       with Not_found -> false
+       end
+    |  _ -> false
+
+  let rec is_ground_term env evd term =
+    match EConstr.kind evd term with
+    | App(c,args) ->
+       is_declared_term env evd c &&
+         Array.for_all (is_ground_term env evd) args
+    | Const _ | Construct _ -> is_declared_term env evd term
+    |  _      -> false
 
 
   let parse_z sigma term =
@@ -674,26 +687,28 @@ struct
 
   let parse_zop gl (op,args) =
     let sigma = gl.sigma in
-    match EConstr.kind sigma op with
-    | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1))
-    | Ind((n,0),_) ->
-        if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z)
-        then (Mc.OpEq, args.(1), args.(2))
-        else raise ParseError
-    |   _ -> failwith "parse_zop"
+    match args with
+    | [| a1 ; a2|] ->  assoc_const sigma op zop_table, a1, a2
+    | [| ty ; a1 ; a2|] ->
+       if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl ty (Lazy.force coq_Z)
+       then (Mc.OpEq, args.(1), args.(2))
+       else raise ParseError
+    |  _ -> raise ParseError
 
   let parse_rop gl (op,args) =
     let sigma = gl.sigma in
-    match EConstr.kind sigma op with
-     | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1))
-     | Ind((n,0),_) ->
-        if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R)
-        then (Mc.OpEq, args.(1), args.(2))
-        else raise ParseError
-    |   _ -> failwith "parse_zop"
+    match args with
+    | [| a1 ; a2|] -> assoc_const sigma op rop_table, a1 , a2
+    | [| ty ; a1 ; a2|] ->
+       if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl ty (Lazy.force coq_R)
+       then (Mc.OpEq, a1, a2)
+       else raise ParseError
+    |   _ -> raise ParseError
 
   let parse_qop gl (op,args) =
-    (assoc_const gl.sigma op qop_table, args.(0) , args.(1))
+    if Array.length args = 2
+    then (assoc_const gl.sigma op qop_table, args.(0) , args.(1))
+    else raise ParseError
 
   type 'a op =
     | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr)
@@ -804,7 +819,7 @@ struct
       (op expr1 expr2,env) in
 
        try (Mc.PEc (parse_constant gl term) , env)
-       with ParseError -> 
+       with ParseError ->
          match EConstr.kind gl.sigma term with
            | App(t,args) ->
                (
@@ -820,7 +835,7 @@ struct
                            let (expr,env) = parse_expr env args.(0) in
                            let power = (parse_exp expr args.(1)) in
                            (power  , env)
-			 with e when CErrors.noncritical e ->
+                         with ParseError ->
                            (* if the exponent is a variable *)
                            let (env,n) = Env.compute_rank_add env  term in (Mc.PEX n, env)
                               end
@@ -858,19 +873,48 @@ struct
       coq_Ropp   , Opp ;
       coq_Rpower , Power]
 
-  (** [parse_constant parse gl t] returns the reification of term [t].
+  let parse_constant parse gl t =   parse gl.sigma t
+
+  (** [parse_more_constant parse gl t] returns the reification of term [t].
       If [t] is a ground term, then it is first reduced to normal form
       before using a 'syntactic' parser *)
-  let parse_constant parse gl t =
-    if  is_ground_term gl.env gl.sigma t
-    then
-      parse gl.sigma (Redexpr.cbv_vm gl.env gl.sigma t)
-    else raise ParseError
+  let parse_more_constant parse gl t =
+    try
+      parse gl t
+    with ParseError  ->
+      begin
+        if debug then Feedback.msg_debug Pp.(str "try harder");
+        if is_ground_term gl.env gl.sigma t
+        then parse gl (Redexpr.cbv_vm gl.env gl.sigma t)
+        else raise ParseError
+      end
 
   let zconstant = parse_constant parse_z
   let qconstant = parse_constant parse_q
   let nconstant = parse_constant parse_nat
 
+  (** [parse_more_zexpr parse_constant gl] improves the parsing of exponent
+      which can be arithmetic expressions (without variables).
+      [parse_constant_expr] returns a constant if the argument is an expression without variables. *)
+
+  let rec parse_zexpr gl =
+    parse_expr gl
+      zconstant
+      (fun expr (x:EConstr.t) ->
+        let z = parse_zconstant gl x in
+        match z with
+        | Mc.Zneg _ -> Mc.PEc Mc.Z0
+        |   _     ->  Mc.PEpow(expr, Mc.Z.to_N z)
+    )
+    zop_spec
+  and parse_zconstant  gl e =
+    let (e,_) = parse_zexpr  gl (Env.empty gl) e in
+    match Mc.zeval_const e with
+    | None -> raise ParseError
+    | Some z -> z
+
+
+
   (* NB: R is a different story.
      Because it is axiomatised, reducing would not be effective.
      Therefore, there is a specific parser for constant over R
@@ -905,7 +949,7 @@ struct
              let b = rconstant args.(1) in
              f a b
            with
-	      ParseError -> 
+              ParseError ->
 		match op with
 		| op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) ->
                   let arg = rconstant args.(0) in
@@ -913,12 +957,12 @@ struct
                   then raise ParseError (* This is a division by zero -- no semantics *)
                   else Mc.CInv(arg) 
                 | op when EConstr.eq_constr sigma op (Lazy.force coq_Rpower) ->
-                     Mc.CPow(rconstant args.(0) , Mc.Inr (nconstant gl args.(1)))
+                     Mc.CPow(rconstant args.(0) , Mc.Inr (parse_more_constant nconstant gl args.(1)))
                 | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR)  ->
                      Mc.CQ (qconstant gl args.(0))
                 | op when EConstr.eq_constr sigma op   (Lazy.force coq_IZR)  ->
-                     Mc.CZ (zconstant gl args.(0))
-		| _ ->  raise ParseError
+                     Mc.CZ (parse_more_constant zconstant gl args.(0))
+                | _ ->  raise ParseError
 	end
       |  _ -> raise ParseError in
 
@@ -934,14 +978,6 @@ struct
       res
 
 
-  let parse_zexpr gl =  parse_expr gl
-    zconstant
-    (fun expr x ->
-      let exp = (zconstant gl x) in
-        match exp with
-          | Mc.Zneg _ -> Mc.PEc Mc.Z0
-          |   _     ->  Mc.PEpow(expr, Mc.Z.to_N exp))
-    zop_spec
 
   let parse_qexpr gl =  parse_expr gl
    qconstant
@@ -952,7 +988,7 @@ struct
               begin
                 match expr with
                 | Mc.PEc q -> Mc.PEc (Mc.qpower q exp)
-                |     _    -> print_string "parse_qexpr parse error" ; flush stdout ; raise ParseError
+                |     _    -> raise ParseError
               end
           | _     ->  let exp = Mc.Z.to_N  exp in
                         Mc.PEpow(expr,exp))
@@ -1031,14 +1067,16 @@ struct
           let g,env,tg = xparse_formula env tg b in
           mkformula_binary mkIff term f g,env,tg
         | _ -> parse_atom env tg term)
-      | Prod(typ,a,b) when EConstr.Vars.noccurn sigma 1 b ->
+      | Prod(typ,a,b) when typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b ->
         let f,env,tg = xparse_formula env tg a in
         let g,env,tg = xparse_formula env tg b in
         mkformula_binary mkI term f g,env,tg
-      | _ when EConstr.eq_constr sigma term (Lazy.force coq_True) -> (Mc.TT,env,tg)
-      | _ when EConstr.eq_constr sigma term (Lazy.force coq_False) -> Mc.(FF,env,tg)
-      | _ when is_prop term -> Mc.X(term),env,tg
-      | _ -> raise ParseError
+      | _ -> if EConstr.eq_constr sigma term (Lazy.force coq_True)
+             then (Mc.TT,env,tg)
+             else if EConstr.eq_constr sigma term (Lazy.force coq_False)
+             then Mc.(FF,env,tg)
+             else if is_prop term then Mc.X(term),env,tg
+             else raise ParseError
     in
     xparse_formula env tg  ((*Reductionops.whd_zeta*) term)
 
@@ -1358,19 +1396,11 @@ let rec parse_hyps gl parse_arith env tg hyps =
        let (c,env,tg) = parse_formula gl parse_arith env  tg t in
 	((i,c)::lhyps, env,tg)
       with e when CErrors.noncritical e -> (lhyps,env,tg)
-       (*(if debug then Printf.printf "parse_arith : %s\n" x);*)
-
-
-(*exception ParseError*)
-
-
 
 let parse_goal gl parse_arith (env:Env.t) hyps term =
- (*  try*)
  let (f,env,tg) = parse_formula gl parse_arith env (Tag.from 0) term in
  let (lhyps,env,tg) = parse_hyps gl parse_arith env tg hyps in
   (lhyps,f,env)
-   (*  with Failure x -> raise ParseError*)
 
 (**
   * The datastructures that aggregate theory-dependent proof values.
@@ -1886,7 +1916,7 @@ let micromega_genr prover tac =
          ]
 
     with
-    | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
+    | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
     | Mfourier.TimeOut  -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
     | CsdpNotFound -> flush stdout ;
      Tacticals.New.tclFAIL 0 (Pp.str 
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index b34c3b2b7d..a64a5a84b3 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -230,6 +230,13 @@ module Coq_Pos =
     | XO p -> XO (mul p y)
     | XH -> y
 
+  (** val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1 **)
+
+  let rec iter f x = function
+  | XI n' -> f (iter f (iter f x n') n')
+  | XO n' -> iter f (iter f x n') n'
+  | XH -> f x
+
   (** val size_nat : positive -> nat **)
 
   let rec size_nat = function
@@ -398,6 +405,18 @@ module Z =
        | Zpos y' -> Zneg (Coq_Pos.mul x' y')
        | Zneg y' -> Zpos (Coq_Pos.mul x' y'))
 
+  (** val pow_pos : z -> positive -> z **)
+
+  let pow_pos z0 =
+    Coq_Pos.iter (mul z0) (Zpos XH)
+
+  (** val pow : z -> z -> z **)
+
+  let pow x = function
+  | Z0 -> Zpos XH
+  | Zpos p -> pow_pos x p
+  | Zneg _ -> Z0
+
   (** val compare : z -> z -> comparison **)
 
   let compare x y =
@@ -460,6 +479,12 @@ module Z =
   | O -> Z0
   | S n1 -> Zpos (Coq_Pos.of_succ_nat n1)
 
+  (** val of_N : n -> z **)
+
+  let of_N = function
+  | N0 -> Z0
+  | Npos p -> Zpos p
+
   (** val pos_div_eucl : positive -> z -> z * z **)
 
   let rec pos_div_eucl a b =
@@ -1642,6 +1667,21 @@ let rec vm_add default x v = function
    | XO p -> Branch ((vm_add default p v l), o, r)
    | XH -> Branch (l, v, r))
 
+(** val zeval_const : z pExpr -> z option **)
+
+let rec zeval_const = function
+| PEc c -> Some c
+| PEX _ -> None
+| PEadd (e1, e2) ->
+  map_option2 (fun x y -> Some (Z.add x y)) (zeval_const e1) (zeval_const e2)
+| PEsub (e1, e2) ->
+  map_option2 (fun x y -> Some (Z.sub x y)) (zeval_const e1) (zeval_const e2)
+| PEmul (e1, e2) ->
+  map_option2 (fun x y -> Some (Z.mul x y)) (zeval_const e1) (zeval_const e2)
+| PEopp e0 -> map_option (fun x -> Some (Z.opp x)) (zeval_const e0)
+| PEpow (e1, n0) ->
+  map_option (fun x -> Some (Z.pow x (Z.of_N n0))) (zeval_const e1)
+
 type zWitness = z psatz
 
 (** val zWeakChecker : z nFormula list -> z psatz -> bool **)
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 5de6caac0b..64cb3a8355 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -86,6 +86,8 @@ module Coq_Pos :
 
   val mul : positive -> positive -> positive
 
+  val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1
+
   val size_nat : positive -> nat
 
   val compare_cont : comparison -> positive -> positive -> comparison
@@ -124,6 +126,10 @@ module Z :
 
   val mul : z -> z -> z
 
+  val pow_pos : z -> positive -> z
+
+  val pow : z -> z -> z
+
   val compare : z -> z -> comparison
 
   val leb : z -> z -> bool
@@ -140,6 +146,8 @@ module Z :
 
   val of_nat : nat -> z
 
+  val of_N : n -> z
+
   val pos_div_eucl : positive -> z -> z * z
 
   val div_eucl : z -> z -> z * z
@@ -179,20 +187,20 @@ val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
 val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
 
 val paddI :
-  ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1
-  pol -> 'a1 pol
+  ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol
+  -> 'a1 pol
 
 val psubI :
   ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol ->
   positive -> 'a1 pol -> 'a1 pol
 
 val paddX :
-  'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol ->
-  positive -> 'a1 pol -> 'a1 pol
+  'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive ->
+  'a1 pol -> 'a1 pol
 
 val psubX :
-  'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) ->
-  'a1 pol -> positive -> 'a1 pol -> 'a1 pol
+  'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1
+  pol -> positive -> 'a1 pol -> 'a1 pol
 
 val padd :
   'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
@@ -205,20 +213,19 @@ val pmulC_aux :
   'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol
 
 val pmulC :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1
-  pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol
 
 val pmulI :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol ->
-  'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1
+  pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
 
 val pmul :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) ->
-  'a1 pol -> 'a1 pol -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1
+  pol -> 'a1 pol -> 'a1 pol
 
 val psquare :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) ->
-  'a1 pol -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1
+  pol -> 'a1 pol
 
 type 'c pExpr =
 | PEc of 'c
@@ -232,16 +239,16 @@ type 'c pExpr =
 val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol
 
 val ppow_pos :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) ->
-  ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1
+  pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol
 
 val ppow_N :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) ->
-  ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1
+  pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
 
 val norm_aux :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) ->
-  ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1
+  -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
 
 type ('tA, 'tX, 'aA, 'aF) gFormula =
 | TT
@@ -253,8 +260,7 @@ type ('tA, 'tX, 'aA, 'aF) gFormula =
 | N of ('tA, 'tX, 'aA, 'aF) gFormula
 | I of ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula
 
-val mapX :
-  ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula
+val mapX : ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula
 
 val foldA : ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5
 
@@ -278,37 +284,36 @@ val cnf_tt : ('a1, 'a2) cnf
 val cnf_ff : ('a1, 'a2) cnf
 
 val add_term :
-  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause ->
-  ('a1, 'a2) clause option
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> ('a1,
+  'a2) clause option
 
 val or_clause :
-  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2)
-  clause -> ('a1, 'a2) clause option
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) clause ->
+  ('a1, 'a2) clause option
 
 val or_clause_cnf :
-  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf
-  -> ('a1, 'a2) cnf
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf ->
+  ('a1, 'a2) cnf
 
 val or_cnf :
-  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf ->
-  ('a1, 'a2) cnf
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1,
+  'a2) cnf
 
 val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
 
 type ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula
 
 val xcnf :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) ->
-  ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2,
-  'a3) cnf
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 ->
+  'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
 
 val radd_term :
   ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause ->
   (('a1, 'a2) clause, 'a2 list) sum
 
 val ror_clause :
-  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause
-  -> (('a1, 'a2) clause, 'a2 list) sum
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause ->
+  (('a1, 'a2) clause, 'a2 list) sum
 
 val ror_clause_cnf :
   ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause
@@ -319,17 +324,16 @@ val ror_cnf :
   clause list -> ('a1, 'a2) cnf * 'a2 list
 
 val rxcnf :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) ->
-  ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2,
-  'a3) cnf * 'a3 list
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 ->
+  'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3
+  list
 
-val cnf_checker :
-  (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool
+val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool
 
 val tauto_checker :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) ->
-  ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, __,
-  'a3, unit0) gFormula -> 'a4 list -> bool
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 ->
+  'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, __, 'a3, unit0)
+  gFormula -> 'a4 list -> bool
 
 val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
 
@@ -363,27 +367,27 @@ val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option
 val map_option2 : ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option
 
 val pexpr_times_nformula :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) ->
-  'a1 polC -> 'a1 nFormula -> 'a1 nFormula option
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1
+  polC -> 'a1 nFormula -> 'a1 nFormula option
 
 val nformula_times_nformula :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) ->
-  'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1
+  nFormula -> 'a1 nFormula -> 'a1 nFormula option
 
 val nformula_plus_nformula :
-  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula
-  -> 'a1 nFormula option
+  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula ->
+  'a1 nFormula option
 
 val eval_Psatz :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) ->
-  ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1
+  -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option
 
 val check_inconsistent :
   'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool
 
 val check_normalised_formulas :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) ->
-  ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1
+  -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool
 
 type op2 =
 | OpEq
@@ -396,8 +400,8 @@ type op2 =
 type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
 
 val norm :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) ->
-  ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1
+  -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
 
 val psub0 :
   'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 ->
@@ -407,20 +411,20 @@ val padd0 :
   'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
 
 val xnormalise :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) ->
-  ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1
+  -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list
 
 val cnf_normalise :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) ->
-  ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1
+  -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
 
 val xnegate :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) ->
-  ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1
+  -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list
 
 val cnf_negate :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) ->
-  ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1
+  -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
 
 val xdenorm : positive -> 'a1 pol -> 'a1 pExpr
 
@@ -475,6 +479,8 @@ val singleton : 'a1 -> positive -> 'a1 -> 'a1 t
 
 val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t
 
+val zeval_const : z pExpr -> z option
+
 type zWitness = z psatz
 
 val zWeakChecker : z nFormula list -> z psatz -> bool
@@ -563,12 +569,12 @@ val bound_var : positive -> z formula
 val mk_eq_pos : positive -> positive -> positive -> z formula
 
 val bound_vars :
-  (positive -> positive -> bool option -> 'a2) -> positive -> Vars.t -> (z formula,
-  'a1, 'a2, 'a3) gFormula
+  (positive -> positive -> bool option -> 'a2) -> positive -> Vars.t -> (z formula, 'a1,
+  'a2, 'a3) gFormula
 
 val bound_problem_fr :
-  (positive -> positive -> bool option -> 'a2) -> positive -> (z formula, 'a1, 'a2,
-  'a3) gFormula -> (z formula, 'a1, 'a2, 'a3) gFormula
+  (positive -> positive -> bool option -> 'a2) -> positive -> (z formula, 'a1, 'a2, 'a3)
+  gFormula -> (z formula, 'a1, 'a2, 'a3) gFormula
 
 val zChecker : z nFormula list -> zArithProof -> bool
 
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 695f000cb1..23d7b141a4 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -359,7 +359,10 @@ Ltac zify_positive_rel :=
 
 Ltac zify_positive_op :=
  match goal with
-  (* Zneg -> -Zpos (except for numbers) *)
+ (* Z.pow_pos -> Z.pow *)
+ | H : context [ Z.pow_pos ?a ?b ] |- _ => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) in H
+ | |- context [ Z.pow_pos ?a ?b ]  => change (Z.pow_pos a b) with (Z.pow a (Z.pos b))
+ (* Zneg -> -Zpos (except for numbers) *)
   | H : context [ Zneg ?a ] |- _ =>
      let isp := isPcst a in
      match isp with
@@ -377,6 +380,10 @@ Ltac zify_positive_op :=
   | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H
   | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a)
 
+  (* Z.power_pos *)
+  | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H
+  | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a)
+
   (* Pos.add -> Z.add *)
   | H : context [ Zpos (?a + ?b) ] |- _ => change (Zpos (a+b)) with (Zpos a + Zpos b) in H
   | |- context [ Zpos (?a + ?b) ] => change (Zpos (a+b)) with (Zpos a + Zpos b)
diff --git a/test-suite/micromega/bug_10158.v b/test-suite/micromega/bug_10158.v
new file mode 100644
index 0000000000..2c8f798f12
--- /dev/null
+++ b/test-suite/micromega/bug_10158.v
@@ -0,0 +1,48 @@
+Require Import ZArith_base.
+Require Import Coq.micromega.Lia.
+
+Open Scope Z_scope.
+
+Fixpoint fib (n: nat) : Z :=
+  match n with
+  | O => 1
+  | S O => 1
+  | S (S n as p) => fib p + fib n
+  end.
+
+Axiom fib_47_computed: fib 47 = 2971215073.
+
+Lemma fib_bound:
+  fib 47 < 2 ^ 32.
+Proof.
+  pose proof fib_47_computed.
+  lia.
+Qed.
+
+Require Import Reals.
+Require Import Coq.micromega.Lra.
+
+Open Scope R_scope.
+
+Fixpoint fibr (n: nat) : R :=
+  match n with
+  | O => 1
+  | S O => 1
+  | S (S n as p) => fibr p + fibr n
+  end.
+
+Axiom fibr_47_computed: fibr 47 = 2971215073.
+
+Lemma fibr_bound:
+  fibr 47 < 2 ^ 32.
+Proof.
+  pose proof fibr_47_computed.
+  lra.
+Qed.
+
+Lemma fibr_bound':
+  fibr 47 < IZR (Z.pow_pos 2  32).
+Proof.
+  pose proof fibr_47_computed.
+  lra.
+Qed.
diff --git a/test-suite/micromega/rsyntax.v b/test-suite/micromega/rsyntax.v
index 02b98b562f..f02d93f911 100644
--- a/test-suite/micromega/rsyntax.v
+++ b/test-suite/micromega/rsyntax.v
@@ -57,15 +57,7 @@ Require Import Lia.
 
 Goal ( 1 ^ (2 + 2) = 1)%Z.
 Proof.
-  Fail lia.
-  reflexivity.
-Qed.
-
-Instance DZplus : DeclaredConstant Z.add := {}.
-
-Goal ( 1 ^ (2 + 2) = 1)%Z.
-Proof.
-  lia.
+  lia. (* exponent is a constant expr *)
 Qed.
 
 
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
index 7429a521b3..c0ef9b392d 100644
--- a/test-suite/output/MExtraction.v
+++ b/test-suite/output/MExtraction.v
@@ -7,8 +7,8 @@ Require Import QMicromega.
 Require Import RMicromega.
 
 Recursive Extraction
-           Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
-           ZMicromega.cnfZ ZMicromega.bound_problem_fr QMicromega.cnfQ
+Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
+           ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ
            List.map simpl_cone (*map_cone  indexes*)
            denorm Qpower vm_add
    normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.