Library Coq.micromega.ZMicromega


Require Import List.
Require Import Bool.
Require Import OrderedRing.
Require Import RingMicromega.
Require Import ZCoeff.
Require Import Refl.
Require Import ZArith_base.
Require Import ZArithRing.
Require Import Ztac.
Require PreOmega.
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 : forall x,
    0 < x <-> 0 <= x - 1.

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

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

Lemma eq_cnf : forall x,
    (0 <= x - 1 -> False) /\ (0 <= -1 - x -> False) <-> x = 0.

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
  Zeq_bool 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.

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 Zeq_bool 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 Zeq_bool.

Definition popp := popp Z.opp.

Definition padd := padd Z0 Z.add Zeq_bool.

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

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

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 Zeq_bool Z.leb.

Definition Zdeduce := nformula_plus_nformula 0 Z.add Zeq_bool.

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.

Ltac iff_ring :=
  match goal with
  | |- ?F 0 ?X <-> ?F 0 ?Y => replace X with Y by ring ; tauto
  end.

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

Require Import Coq.micromega.Tauto BinNums.

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.


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.

Require Import Znumtheory.

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.

NB: narrow_interval_upper_bound is Zdiv.Zdiv_le_lower_bound

Require Import QArith.

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

.


Require Import Znumtheory.

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 (Zeq_bool c Z0)) (negb (Zeq_bool (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 Zeq_bool 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 Zeq_bool 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.

Require Import 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.

Ltac pos_tac :=
  repeat
  match goal with
  | |- false = _ => symmetry
  | |- Pos.eqb ?X ?Y = false => rewrite Pos.eqb_neq ; intro
  | H : @eq positive ?X ?Y |- _ => apply Zpos_eq in H
  | H : context[Z.pos (Pos.succ ?X)] |- _ => rewrite (Pos2Z.inj_succ X) in H
  | H : Pos.leb ?X ?Y = true |- _ => rewrite Pos.leb_le in H ;
                                     apply (Pos2Z.pos_le_pos X Y) in H
  end.

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.

To ease bindings from ml code
Definition make_impl := Refl.make_impl.
Definition make_conj := Refl.make_conj.

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.

Definition prod_pos_nat := prod positive nat.

Notation n_of_Z := Z.to_N (only parsing).