Library Stdlib.micromega.ZMicromega

From Stdlib Require Import List.
From Stdlib Require Import Bool.
From Stdlib Require Import OrderedRing.
From Stdlib Require Import RingMicromega.
From Stdlib Require Import ZArithRing.
From Stdlib Require Import ZCoeff.
From Stdlib Require Import Refl.
From Stdlib Require Import BinInt.
From Stdlib Require InitialRing.
From Stdlib.micromega Require Import Tauto.
Local Open Scope Z_scope.

Ltac flatten_bool :=
  repeat match goal with
           [ id : (_ && _)%bool = true |- _ ] => destruct (andb_prop _ _ id); clear id
         | [ id : (_ || _)%bool = true |- _ ] => destruct (orb_prop _ _ id); clear id
         end.

Ltac inv H := inversion H ; try subst ; clear H.

Lemma eq_le_iff : forall x, 0 = x <-> (0 <= x /\ x <= 0).

Lemma lt_le_iff x : 0 < x <-> 0 <= x - 1.

Lemma le_0_iff x y : x <= y <-> 0 <= y - x.

Lemma le_neg x : ((0 <= x) -> False) <-> 0 < -x.

Lemma eq_cnf x : (0 <= x - 1 -> False) /\ (0 <= -1 - x -> False) <-> x = 0.
From Stdlib Require Import EnvRing.
Lemma Zsor : SOR 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt.

Lemma ZSORaddon :
  SORaddon 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le
  0%Z 1%Z Z.add Z.mul Z.sub Z.opp
  Z.eqb Z.leb
  (fun x => x) (fun x => x) (pow_N 1 Z.mul).

Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z :=
  match e with
    | PEc c => c
    | PEX x => env x
    | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2
    | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2
    | PEpow e1 n => Z.pow (Zeval_expr env e1) (Z.of_N n)
    | PEsub e1 e2 => (Zeval_expr env e1) - (Zeval_expr env e2)
    | PEopp e => Z.opp (Zeval_expr env e)
  end.

Strategy expand [ Zeval_expr ].

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.

Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = eval_expr env e.

Definition Zeval_pop2 (o : Op2) : Z -> Z -> Prop :=
match o with
| OpEq => @eq Z
| OpNEq => fun x y => ~ x = y
| OpLe => Z.le
| OpGe => Z.ge
| OpLt => Z.lt
| OpGt => Z.gt
end.

Definition Zeval_bop2 (o : Op2) : Z -> Z -> bool :=
match o with
| OpEq => Z.eqb
| OpNEq => fun x y => negb (Z.eqb x y)
| OpLe => Z.leb
| OpGe => Z.geb
| OpLt => Z.ltb
| OpGt => Z.gtb
end.

Lemma pop2_bop2 :
  forall (op : Op2) (q1 q2 : Z), is_true (Zeval_bop2 op q1 q2) <-> Zeval_pop2 op q1 q2.

Definition Zeval_op2 (k: Tauto.kind) : Op2 -> Z -> Z -> Tauto.rtyp k:=
  if k as k0 return (Op2 -> Z -> Z -> Tauto.rtyp k0)
  then Zeval_pop2 else Zeval_bop2.

Lemma Zeval_op2_hold : forall k op q1 q2,
    Tauto.hold k (Zeval_op2 k op q1 q2) <-> Zeval_pop2 op q1 q2.

Definition Zeval_formula (env : PolEnv Z) (k: Tauto.kind) (f : Formula Z):=
  let (lhs, op, rhs) := f in
    (Zeval_op2 k op) (Zeval_expr env lhs) (Zeval_expr env rhs).

Definition Zeval_formula' :=
  eval_formula Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt (fun x => x) (fun x => x) (pow_N 1 Z.mul).

Lemma Zeval_formula_compat : forall env k f, Tauto.hold k (Zeval_formula env k f) <-> Zeval_formula env Tauto.isProp f.

Lemma Zeval_formula_compat' : forall env f, Zeval_formula env Tauto.isProp f <-> Zeval_formula' env f.

Definition eval_nformula :=
  eval_nformula 0 Z.add Z.mul (@eq Z) Z.le Z.lt (fun x => x) .

Definition Zeval_op1 (o : Op1) : Z -> Prop :=
match o with
| Equal => fun x : Z => x = 0
| NonEqual => fun x : Z => x <> 0
| Strict => fun x : Z => 0 < x
| NonStrict => fun x : Z => 0 <= x
end.

Lemma Zeval_nformula_dec : forall env d, (eval_nformula env d) \/ ~ (eval_nformula env d).

Definition ZWitness := Psatz Z.

Definition ZWeakChecker := check_normalised_formulas 0 1 Z.add Z.mul Z.eqb Z.leb.

Lemma ZWeakChecker_sound : forall (l : list (NFormula Z)) (cm : ZWitness),
  ZWeakChecker l cm = true ->
  forall env, make_impl (eval_nformula env) l False.

Definition psub := psub Z0 Z.add Z.sub Z.opp Z.eqb.

Definition popp := popp Z.opp.

Definition padd := padd Z0 Z.add Z.eqb.

Definition pmul := pmul 0 1 Z.add Z.mul Z.eqb.

Definition normZ := norm 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb.

Definition eval_pol := eval_pol Z.add Z.mul (fun x => x).

Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub lhs rhs) = eval_pol env lhs - eval_pol env rhs.

Lemma eval_pol_add : forall env lhs rhs, eval_pol env (padd lhs rhs) = eval_pol env lhs + eval_pol env rhs.

Lemma eval_pol_mul : forall env lhs rhs, eval_pol env (pmul lhs rhs) = eval_pol env lhs * eval_pol env rhs.

Lemma eval_pol_norm : forall env e, eval_expr env e = eval_pol env (normZ e) .

Definition Zunsat := check_inconsistent 0 Z.eqb Z.leb.

Definition Zdeduce := nformula_plus_nformula 0 Z.add Z.eqb.

Lemma Zunsat_sound : forall f,
    Zunsat f = true -> forall env, eval_nformula env f -> False.

Definition xnnormalise (t : Formula Z) : NFormula Z :=
  let (lhs,o,rhs) := t in
  let lhs := normZ lhs in
  let rhs := normZ rhs in
  match o with
  | OpEq => (psub rhs lhs, Equal)
  | OpNEq => (psub rhs lhs, NonEqual)
  | OpGt => (psub lhs rhs, Strict)
  | OpLt => (psub rhs lhs, Strict)
  | OpGe => (psub lhs rhs, NonStrict)
  | OpLe => (psub rhs lhs, NonStrict)
  end.

Lemma xnnormalise_correct :
  forall env f,
    eval_nformula env (xnnormalise f) <-> Zeval_formula env Tauto.isProp f.

Definition xnormalise (f: NFormula Z) : list (NFormula Z) :=
  let (e,o) := f in
  match o with
  | Equal => (psub e (Pc 1),NonStrict) :: (psub (Pc (-1)) e, NonStrict) :: nil
  | NonStrict => ((psub (Pc (-1)) e,NonStrict)::nil)
  | Strict => ((psub (Pc 0)) e, NonStrict)::nil
  | NonEqual => (e, Equal)::nil
  end.

Lemma eval_pol_Pc : forall env z,
    eval_pol env (Pc z) = z.

Lemma xnormalise_correct : forall env f,
    (make_conj (fun x => eval_nformula env x -> False) (xnormalise f)) <-> eval_nformula env f.

Definition cnf_of_list {T: Type} (tg : T) (l : list (NFormula Z)) :=
  List.fold_right (fun x acc =>
                     if Zunsat x then acc else ((x,tg)::nil)::acc)
                  (cnf_tt _ _) l.

Lemma cnf_of_list_correct :
  forall {T : Type} (tg:T) (f : list (NFormula Z)) env,
  eval_cnf eval_nformula env (cnf_of_list tg f) <->
  make_conj (fun x : NFormula Z => eval_nformula env x -> False) f.

Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T :=
  let f := xnnormalise t in
  if Zunsat f then cnf_ff _ _
  else cnf_of_list tg (xnormalise f).

Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env Tauto.isProp t.

Definition xnegate (f:NFormula Z) : list (NFormula Z) :=
  let (e,o) := f in
    match o with
      | Equal => (e,Equal) :: nil
      | NonEqual => (psub e (Pc 1),NonStrict) :: (psub (Pc (-1)) e, NonStrict) :: nil
      | NonStrict => (e,NonStrict)::nil
      | Strict => (psub e (Pc 1),NonStrict)::nil
    end.

Definition negate {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T :=
  let f := xnnormalise t in
  if Zunsat f then cnf_tt _ _
  else cnf_of_list tg (xnegate f).

Lemma xnegate_correct : forall env f,
    (make_conj (fun x => eval_nformula env x -> False) (xnegate f)) <-> ~ eval_nformula env f.

Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env Tauto.isProp t.

Definition cnfZ (Annot: Type) (TX : Tauto.kind -> Type) (AF : Type) (k: Tauto.kind) (f : TFormula (Formula Z) Annot TX AF k) :=
  rxcnf Zunsat Zdeduce normalise negate true f.

Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z) Tauto.isProp) : bool :=
  @tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate ZWitness (fun cl => ZWeakChecker (List.map fst cl)) f w.


From Stdlib Require Import Zdiv.
Local Open Scope Z_scope.

Definition ceiling (a b:Z) : Z :=
  let (q,r) := Z.div_eucl a b in
    match r with
      | Z0 => q
      | _ => q + 1
    end.

Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Z.div a b.

Lemma narrow_interval_lower_bound a b x :
  a > 0 -> a * x >= b -> x >= ceiling b a.

Inductive ZArithProof :=
| DoneProof
| RatProof : ZWitness -> ZArithProof -> ZArithProof
| CutProof : ZWitness -> ZArithProof -> ZArithProof
| SplitProof : PolC Z -> ZArithProof -> ZArithProof -> ZArithProof
| EnumProof : ZWitness -> ZWitness -> list ZArithProof -> ZArithProof
| ExProof : positive -> ZArithProof -> ZArithProof

.

Register ZArithProof as micromega.ZArithProof.type.
Register DoneProof as micromega.ZArithProof.DoneProof.
Register RatProof as micromega.ZArithProof.RatProof.
Register CutProof as micromega.ZArithProof.CutProof.
Register SplitProof as micromega.ZArithProof.SplitProof.
Register EnumProof as micromega.ZArithProof.EnumProof.
Register ExProof as micromega.ZArithProof.ExProof.


Definition isZ0 (x:Z) :=
  match x with
    | Z0 => true
    | _ => false
  end.

Lemma isZ0_0 : forall x, isZ0 x = true <-> x = 0.

Lemma isZ0_n0 : forall x, isZ0 x = false <-> x <> 0.

Definition ZgcdM (x y : Z) := Z.max (Z.gcd x y) 1.

Fixpoint Zgcd_pol (p : PolC Z) : (Z * Z) :=
  match p with
    | Pc c => (0,c)
    | Pinj _ p => Zgcd_pol p
    | PX p _ q =>
      let (g1,c1) := Zgcd_pol p in
        let (g2,c2) := Zgcd_pol q in
          (ZgcdM (ZgcdM g1 c1) g2 , c2)
  end.


Fixpoint Zdiv_pol (p:PolC Z) (x:Z) : PolC Z :=
  match p with
    | Pc c => Pc (Z.div c x)
    | Pinj j p => Pinj j (Zdiv_pol p x)
    | PX p j q => PX (Zdiv_pol p x) j (Zdiv_pol q x)
  end.

Inductive Zdivide_pol (x:Z): PolC Z -> Prop :=
| Zdiv_Pc : forall c, (x | c) -> Zdivide_pol x (Pc c)
| Zdiv_Pinj : forall p, Zdivide_pol x p -> forall j, Zdivide_pol x (Pinj j p)
| Zdiv_PX : forall p q, Zdivide_pol x p -> Zdivide_pol x q -> forall j, Zdivide_pol x (PX p j q).

Lemma Zdiv_pol_correct : forall a p, 0 < a -> Zdivide_pol a p ->
  forall env, eval_pol env p = a * eval_pol env (Zdiv_pol p a).

Lemma Zgcd_pol_ge : forall p, fst (Zgcd_pol p) >= 0.

Lemma Zdivide_pol_Zdivide : forall p x y, Zdivide_pol x p -> (y | x) -> Zdivide_pol y p.

Lemma Zdivide_pol_one : forall p, Zdivide_pol 1 p.

Lemma Zgcd_minus : forall a b c, (a | c - b ) -> (Z.gcd a b | c).

Lemma Zdivide_pol_sub : forall p a b,
  0 < Z.gcd a b ->
  Zdivide_pol a (PsubC Z.sub p b) ->
   Zdivide_pol (Z.gcd a b) p.

Lemma Zdivide_pol_sub_0 : forall p a,
  Zdivide_pol a (PsubC Z.sub p 0) ->
   Zdivide_pol a p.

Lemma Zgcd_pol_div : forall p g c,
  Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Z.sub p c).

Lemma Zgcd_pol_correct_lt : forall p env g c, Zgcd_pol p = (g,c) -> 0 < g -> eval_pol env p = g * (eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) + c.

Definition makeCuttingPlane (p : PolC Z) : PolC Z * Z :=
  let (g,c) := Zgcd_pol p in
    if Z.gtb g Z0
      then (Zdiv_pol (PsubC Z.sub p c) g , Z.opp (ceiling (Z.opp c) g))
      else (p,Z0).

Definition genCuttingPlane (f : NFormula Z) : option (PolC Z * Z * Op1) :=
  let (e,op) := f in
    match op with
      | Equal => let (g,c) := Zgcd_pol e in
        if andb (Z.gtb g Z0) (andb (negb (Z.eqb c Z0)) (negb (Z.eqb (Z.gcd g c) g)))
          then None
          else
            let (p,c) := makeCuttingPlane e in
              Some (p,c,Equal)
      | NonEqual => Some (e,Z0,op)
      | Strict => let (p,c) := makeCuttingPlane (PsubC Z.sub e 1) in
        Some (p,c,NonStrict)
      | NonStrict => let (p,c) := makeCuttingPlane e in
        Some (p,c,NonStrict)
    end.

Definition nformula_of_cutting_plane (t : PolC Z * Z * Op1) : NFormula Z :=
  let (e_z, o) := t in
    let (e,z) := e_z in
      (padd e (Pc z) , o).

Definition is_pol_Z0 (p : PolC Z) : bool :=
  match p with
    | Pc Z0 => true
    | _ => false
  end.

Lemma is_pol_Z0_eval_pol : forall p, is_pol_Z0 p = true -> forall env, eval_pol env p = 0.

Definition eval_Psatz : list (NFormula Z) -> ZWitness -> option (NFormula Z) :=
  eval_Psatz 0 1 Z.add Z.mul Z.eqb Z.leb.

Definition valid_cut_sign (op:Op1) :=
  match op with
    | Equal => true
    | NonStrict => true
    | _ => false
  end.

Definition bound_var (v : positive) : Formula Z :=
  Build_Formula (PEX v) OpGe (PEc 0).

Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z :=
  Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)).

Fixpoint vars (jmp : positive) (p : Pol Z) : list positive :=
  match p with
  | Pc c => nil
  | Pinj j p => vars (Pos.add j jmp) p
  | PX p j q => jmp::(vars jmp p)++vars (Pos.succ jmp) q
  end.

Fixpoint max_var (jmp : positive) (p : Pol Z) : positive :=
  match p with
  | Pc _ => jmp
  | Pinj j p => max_var (Pos.add j jmp) p
  | PX p j q => Pos.max (max_var jmp p) (max_var (Pos.succ jmp) q)
  end.

Lemma pos_le_add : forall y x,
    (x <= y + x)%positive.

Lemma max_var_le : forall p v,
    (v <= max_var v p)%positive.

Lemma max_var_correct : forall p j v,
    In v (vars j p) -> Pos.le v (max_var j p).

Definition max_var_nformulae (l : list (NFormula Z)) :=
  List.fold_left (fun acc f => Pos.max acc (max_var xH (fst f))) l xH.

Section MaxVar.

  Definition F (acc : positive) (f : Pol Z * Op1) := Pos.max acc (max_var 1 (fst f)).

  Lemma max_var_nformulae_mono_aux :
    forall l v acc,
      (v <= acc ->
       v <= fold_left F l acc)%positive.

  Lemma max_var_nformulae_mono_aux' :
    forall l acc acc',
      (acc <= acc' ->
       fold_left F l acc <= fold_left F l acc')%positive.

  Lemma max_var_nformulae_correct_aux : forall l p o v,
      In (p,o) l -> In v (vars xH p) -> Pos.le v (fold_left F l 1)%positive.

End MaxVar.

Lemma max_var_nformalae_correct : forall l p o v,
      In (p,o) l -> In v (vars xH p) -> Pos.le v (max_var_nformulae l)%positive.

Fixpoint max_var_psatz (w : Psatz Z) : positive :=
  match w with
  | PsatzIn _ n => xH
  | PsatzSquare p => max_var xH (Psquare 0 1 Z.add Z.mul Z.eqb p)
  | PsatzMulC p w => Pos.max (max_var xH p) (max_var_psatz w)
  | PsatzMulE w1 w2 => Pos.max (max_var_psatz w1) (max_var_psatz w2)
  | PsatzAdd w1 w2 => Pos.max (max_var_psatz w1) (max_var_psatz w2)
  | _ => xH
  end.

Fixpoint max_var_prf (w : ZArithProof) : positive :=
  match w with
  | DoneProof => xH
  | RatProof w pf | CutProof w pf => Pos.max (max_var_psatz w) (max_var_prf pf)
  | SplitProof p pf1 pf2 => Pos.max (max_var xH p) (Pos.max (max_var_prf pf1) (max_var_prf pf1))
  | EnumProof w1 w2 l => List.fold_left
                           (fun acc prf => Pos.max acc (max_var_prf prf)) l
                           (Pos.max (max_var_psatz w1) (max_var_psatz w2))
  | ExProof _ pf => max_var_prf pf
  end.

Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool :=
  match pf with
    | DoneProof => false
    | RatProof w pf =>
      match eval_Psatz l w with
        | None => false
        | Some f =>
          if Zunsat f then true
            else ZChecker (f::l) pf
      end
    | CutProof w pf =>
      match eval_Psatz l w with
        | None => false
        | Some f =>
          match genCuttingPlane f with
            | None => true
            | Some cp => ZChecker (nformula_of_cutting_plane cp::l) pf
          end
      end
    | SplitProof p pf1 pf2 =>
      match genCuttingPlane (p,NonStrict) , genCuttingPlane (popp p, NonStrict) with
      | None , _ | _ , None => false
      | Some cp1 , Some cp2 =>
        ZChecker (nformula_of_cutting_plane cp1::l) pf1
        &&
        ZChecker (nformula_of_cutting_plane cp2::l) pf2
      end
    | ExProof x prf =>
      let fr := max_var_nformulae l in
      if Pos.leb x fr then
      let z := Pos.succ fr in
      let t := Pos.succ z in
      let nfx := xnnormalise (mk_eq_pos x z t) in
      let posz := xnnormalise (bound_var z) in
      let post := xnnormalise (bound_var t) in
      ZChecker (nfx::posz::post::l) prf
      else false
      | EnumProof w1 w2 pf =>
       match eval_Psatz l w1 , eval_Psatz l w2 with
         | Some f1 , Some f2 =>
           match genCuttingPlane f1 , genCuttingPlane f2 with
             |Some (e1,z1,op1) , Some (e2,z2,op2) =>
               if (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd e1 e2))
                 then
                   (fix label (pfs:list ZArithProof) :=
                   fun lb ub =>
                     match pfs with
                       | nil => if Z.gtb lb ub then true else false
                       | pf::rsr => andb (ZChecker ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Z.add lb 1%Z) ub)
                     end) pf (Z.opp z1) z2
                  else false
              | _ , _ => true
           end
          | _ , _ => false
    end
end.

Fixpoint bdepth (pf : ZArithProof) : nat :=
  match pf with
    | DoneProof => O
    | RatProof _ p => S (bdepth p)
    | CutProof _ p => S (bdepth p)
    | SplitProof _ p1 p2 => S (Nat.max (bdepth p1) (bdepth p2))
    | EnumProof _ _ l => S (List.fold_right (fun pf x => Nat.max (bdepth pf) x) O l)
    | ExProof _ p => S (bdepth p)
  end.

From Stdlib Require Import PeanoNat Wf_nat.

Lemma in_bdepth : forall l a b y, In y l -> ltof ZArithProof bdepth y (EnumProof a b l).

Lemma ltof_bdepth_split_l :
  forall p pf1 pf2,
         ltof ZArithProof bdepth pf1 (SplitProof p pf1 pf2).

Lemma ltof_bdepth_split_r :
  forall p pf1 pf2,
         ltof ZArithProof bdepth pf2 (SplitProof p pf1 pf2).

Lemma eval_Psatz_sound : forall env w l f',
  make_conj (eval_nformula env) l ->
  eval_Psatz l w = Some f' -> eval_nformula env f'.

Lemma makeCuttingPlane_ns_sound : forall env e e' c,
  eval_nformula env (e, NonStrict) ->
  makeCuttingPlane e = (e',c) ->
  eval_nformula env (nformula_of_cutting_plane (e', c, NonStrict)).

Lemma cutting_plane_sound : forall env f p,
  eval_nformula env f ->
  genCuttingPlane f = Some p ->
   eval_nformula env (nformula_of_cutting_plane p).

Lemma genCuttingPlaneNone : forall env f,
  genCuttingPlane f = None ->
  eval_nformula env f -> False.

Lemma eval_nformula_mk_eq_pos : forall env x z t,
    env x = env z - env t ->
    eval_nformula env (xnnormalise (mk_eq_pos x z t)).

Lemma eval_nformula_bound_var : forall env x,
    env x >= 0 ->
    eval_nformula env (xnnormalise (bound_var x)).

Definition agree_env (fr : positive) (env env' : positive -> Z) : Prop :=
  forall x, Pos.le x fr -> env x = env' x.

Lemma agree_env_subset : forall v1 v2 env env',
    agree_env v1 env env' ->
    Pos.le v2 v1 ->
    agree_env v2 env env'.

Lemma agree_env_jump : forall fr j env env',
    agree_env (fr + j) env env' ->
    agree_env fr (Env.jump j env) (Env.jump j env').

Lemma agree_env_tail : forall fr env env',
    agree_env (Pos.succ fr) env env' ->
    agree_env fr (Env.tail env) (Env.tail env').

Lemma max_var_acc : forall p i j,
    (max_var (i + j) p = max_var i p + j)%positive.

Lemma agree_env_eval_nformula :
  forall env env' e
         (AGREE : agree_env (max_var xH (fst e)) env env'),
    eval_nformula env e <-> eval_nformula env' e.

Lemma agree_env_eval_nformulae :
  forall env env' l
         (AGREE : agree_env (max_var_nformulae l) env env'),
         make_conj (eval_nformula env) l <->
         make_conj (eval_nformula env') l.

Lemma eq_true_iff_eq :
  forall b1 b2 : bool, (b1 = true <-> b2 = true) <-> b1 = b2.

Lemma eval_nformula_split : forall env p,
    eval_nformula env (p,NonStrict) \/ eval_nformula env (popp p,NonStrict).

Lemma ZChecker_sound : forall w l,
    ZChecker l w = true -> forall env, make_impl (eval_nformula env) l False.

Definition ZTautoChecker (f : BFormula (Formula Z) Tauto.isProp) (w: list ZArithProof): bool :=
  @tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate ZArithProof (fun cl => ZChecker (List.map fst cl)) f w.

Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_bf (Zeval_formula env) f.
Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof) : list nat :=
  match pt with
    | DoneProof => acc
    | RatProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt
    | CutProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt
    | SplitProof p pt1 pt2 => xhyps_of_pt (S base) (xhyps_of_pt (S base) acc pt1) pt2
    | EnumProof c1 c2 l =>
      let acc := xhyps_of_psatz base (xhyps_of_psatz base acc c2) c1 in
        List.fold_left (xhyps_of_pt (S base)) l acc
    | ExProof _ pt => xhyps_of_pt (S (S (S base ))) acc pt
  end.

Definition hyps_of_pt (pt : ZArithProof) : list nat := xhyps_of_pt 0 nil pt.

Open Scope Z_scope.

Definition make_impl := Refl.make_impl.
Definition make_conj := Refl.make_conj.

From Stdlib Require VarMap.

Definition env := PolEnv Z.
Definition node := @VarMap.Branch Z.
Definition empty := @VarMap.Empty Z.
Definition leaf := @VarMap.Elt Z.

Definition coneMember := ZWitness.

Definition eval := eval_formula.

#[deprecated(note="Use [prod positive nat]", since="9.0")]
Definition prod_pos_nat := prod positive nat.

#[deprecated(use=Z.to_N, since="9.0")]
Notation n_of_Z := Z.to_N (only parsing).