Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: xts761.mco Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                                                                      *)
(* Micromega: A reflexive tactic using the Positivstellensatz           *)
(*                                                                      *)
(*  Frédéric Besson (Irisa/Inria) 2006-2011                             *)
(*                                                                      *)
(************************************************************************)

Require Import List.
Require Import Bool.
Require Import OrderedRing.
Require Import RingMicromega.
Require  FSetPositive FSetEqProperties.
Require Import ZCoeff.
Require Import Refl.
Require Import ZArith.
(*Declare ML Module "micromega_plugin".*)

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.

Require Import EnvRing.

Open Scope Z_scope.

Lemma Zsor : SOR 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt.
Proof.
  constructor ; intros ; subst ; try (intuition (auto  with zarith)).
  apply Zsth.
  apply Zth.
  destruct (Z.lt_trichotomy n m) ; intuition.
  apply Z.mul_pos_pos ; auto.
Qed.

Lemma ZSORaddon :
  SORaddon 0 1 Z.add Z.mul Z.sub Z.opp  (@eq Z) Z.le (* ring elements *)
  0%Z 1%Z Z.add Z.mul Z.sub Z.opp (* coefficients *)
  Zeq_bool Z.leb
  (fun x => x) (fun x => x) (pow_N 1 Z.mul).
Proof.
  constructor.
  constructor ; intros ; try reflexivity.
  apply Zeq_bool_eq ; auto.
  constructor.
  reflexivity.
  intros x y.
  apply Zeq_bool_neq ; auto.
  apply Zle_bool_imp_le.
Qed.

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.
Proof.
  destruct n.
  reflexivity.
  simpl.
  unfold Z.pow_pos.
  replace (pow_pos Z.mul r p) with (1 * (pow_pos Z.mul r p)) by ring.
  generalize 1.
  induction p; simpl ; intros ; repeat rewrite IHp ; ring.
Qed.

Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = eval_expr env e.
Proof.
  induction e ; simpl ; try congruence.
  reflexivity.
  rewrite ZNpower. congruence.
Qed.

Definition Zeval_op2 (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_formula (env : PolEnv Z) (f : Formula Z):=
  let (lhs, op, rhs) := f in
    (Zeval_op2 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 f, Zeval_formula env f <-> Zeval_formula' env f.
Proof.
  destruct f ; simpl.
  rewrite Zeval_expr_compat. rewrite Zeval_expr_compat.
  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)).
  destruct Fop ; simpl; intros ; intuition (auto with zarith).
Qed.

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).
Proof.
  intros.
  apply (eval_nformula_dec Zsor).
Qed.

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.
Proof.
  intros l cm H.
  intro.
  unfold eval_nformula.
  apply (checker_nf_sound Zsor ZSORaddon l cm).
  unfold ZWeakChecker in H.
  exact H.
Qed.

Definition psub  := psub Z0  Z.add Z.sub Z.opp Zeq_bool.
Declare Equivalent Keys psub RingMicromega.psub.

Definition padd  := padd Z0  Z.add Zeq_bool.
Declare Equivalent Keys padd RingMicromega.padd.

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.
Declare Equivalent Keys normZ RingMicromega.norm.

Definition eval_pol := eval_pol Z.add Z.mul (fun x => x).
Declare Equivalent Keys eval_pol RingMicromega.eval_pol.

Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub  lhs rhs) = eval_pol env lhs - eval_pol env rhs.
Proof.
  intros.
  apply (eval_pol_sub Zsor ZSORaddon).
Qed.

Lemma eval_pol_add : forall env lhs rhs, eval_pol env (padd  lhs rhs) = eval_pol env lhs + eval_pol env rhs.
Proof.
  intros.
  apply (eval_pol_add Zsor ZSORaddon).
Qed.

Lemma eval_pol_mul : forall env lhs rhs, eval_pol env (pmul  lhs rhs) = eval_pol env lhs * eval_pol env rhs.
Proof.
  intros.
  apply (eval_pol_mul Zsor ZSORaddon).
Qed.

Lemma eval_pol_norm : forall env e, eval_expr env e = eval_pol env (normZ e) .
Proof.
  intros.
  apply (eval_pol_norm Zsor ZSORaddon).
Qed.

Definition xnormalise (t:Formula Z) : list (NFormula Z)  :=
  let (lhs,o,rhs) := t in
    let lhs := normZ lhs in
      let rhs := normZ rhs in
    match o with
      | OpEq =>
        ((psub lhs (padd  rhs (Pc 1))),NonStrict)::((psub rhs (padd lhs (Pc 1))),NonStrict)::nil
      | OpNEq => (psub lhs rhs,Equal) :: nil
      | OpGt   => (psub rhs lhs,NonStrict) :: nil
      | OpLt => (psub lhs rhs,NonStrict) :: nil
      | OpGe => (psub rhs (padd lhs (Pc 1)),NonStrict) :: nil
      | OpLe => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil
    end.

Require Import Coq.micromega.Tauto BinNums.

Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T :=
  List.map  (fun x => (x,tg)::nil) (xnormalise t).

Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env t.
Proof.
  unfold normalise, xnormalise; cbn -[padd]; intros T env t tg.
  rewrite Zeval_formula_compat.
  unfold eval_cnf, eval_clause.
  destruct t as [lhs o rhs]; case_eq o; cbn -[padd];
    repeat rewrite eval_pol_sub;
      repeat rewrite eval_pol_add;
      repeat 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 z1 z2 ; intros ; subst;
    intuition (auto with zarith).
Qed.

Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z)  :=
  let (lhs,o,rhs) := t in
    let lhs := normZ lhs in
      let rhs := normZ rhs in
    match o with
      | OpEq  => (psub lhs rhs,Equal) :: nil
      | OpNEq => ((psub lhs (padd rhs (Pc 1))),NonStrict)::((psub rhs (padd lhs (Pc 1))),NonStrict)::nil
      | OpGt  => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil
      | OpLt  => (psub rhs (padd lhs (Pc 1)),NonStrict) :: nil
      | OpGe  => (psub lhs rhs,NonStrict) :: nil
      | OpLe  => (psub rhs lhs,NonStrict) :: nil
    end.

Definition negate {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T :=
  List.map  (fun x => (x,tg)::nil) (xnegate t).

Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env t.
Proof.
Proof.
  Opaque padd.
  intros T env t tg.
  rewrite Zeval_formula_compat.
  unfold negate, xnegate  ; simpl.
  unfold eval_cnf,eval_clause.
  destruct t as [lhs o rhs]; case_eq o; unfold eval_tt ; simpl;
    repeat rewrite eval_pol_sub;
      repeat rewrite eval_pol_add;
      repeat 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 z1 z2 ; intros ; subst;
    intuition (auto with zarith).
  Transparent padd.
Qed.

Definition Zunsat := check_inconsistent 0  Zeq_bool Z.leb.

Definition Zdeduce := nformula_plus_nformula 0 Z.add Zeq_bool.

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

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

(* To get a complete checker, the proof format has to be enriched *)

Require Import Zdiv.
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.
Proof.
  unfold ceiling.
  intros.
  apply Zdivide_mod in H.
  case_eq (Z.div_eucl a b).
  intros.
  change z with (fst (z,z0)).
  rewrite <- H0.
  change (fst (Z.div_eucl a b)) with (Z.div a b).
  change z0 with (snd (z,z0)).
  rewrite <- H0.
  change (snd (Z.div_eucl a b)) with (Z.modulo a b).
  rewrite H.
  reflexivity.
Qed.

Lemma narrow_interval_lower_bound a b x :
  a > 0 -> a * x  >= b -> x >= ceiling b a.
Proof.
  rewrite !Z.ge_le_iff.
  unfold ceiling.
  intros Ha H.
  generalize (Z_div_mod b a Ha).
  destruct (Z.div_eucl b a) as (q,r). intros (->,(H1,H2)).
  destruct r as [|r|r].
  - rewrite Z.add_0_r in H.
    apply Z.mul_le_mono_pos_l in H; auto with zarith.
  - assert (0 < Z.pos r) by easy.
    rewrite Z.add_1_r, Z.le_succ_l.
    apply Z.mul_lt_mono_pos_l with a; auto with zarith.
  - now elim H1.
Qed.

(** 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
| EnumProof : ZWitness -> ZWitness -> list ZArithProof -> ZArithProof
(*| ExProof   : positive -> positive -> positive -> ZArithProof  ExProof z t x : exists z t, x = z - t /\ z >= 0 /\ t >= 0 *)
.
(*| SplitProof :   PolC Z -> ZArithProof -> ZArithProof -> ZArithProof.*)

(* n/d <= x  -> d*x - n >= 0 *)

(* In order to compute the 'cut', we need to express a polynomial P as a * Q + b.
   - b is the constant
   - a is the gcd of the other coefficient.
*)
Require Import Znumtheory.

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

Lemma isZ0_0 : forall x, isZ0 x = true <-> x = 0.
Proof.
  destruct x ; simpl ; intuition congruence.
Qed.

Lemma isZ0_n0 : forall x, isZ0 x = false <-> x <> 0.
Proof.
  destruct x ; simpl ; intuition congruence.
Qed.

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.

(*Eval compute in (Zgcd_pol ((PX (Pc (-2)) 1 (Pc 4)))).*)

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).
Proof.
  intros until 2.
  induction H0.
  (* Pc *)
  simpl.
  intros.
  apply Zdivide_Zdiv_eq ; auto.
  (* Pinj *)
  simpl.
  intros.
  apply IHZdivide_pol.
  (* PX *)
  simpl.
  intros.
  rewrite IHZdivide_pol1.
  rewrite IHZdivide_pol2.
  ring.
Qed.

Lemma Zgcd_pol_ge : forall p, fst (Zgcd_pol p) >= 0.
Proof.
  induction p.
  simpl. auto with zarith.
  simpl. auto.
  simpl.
  case_eq (Zgcd_pol p1).
  case_eq (Zgcd_pol p3).
  intros.
  simpl.
  unfold ZgcdM.
  generalize (Z.gcd_nonneg z1 z2).
  generalize (Zmax_spec (Z.gcd z1 z2) 1).
  generalize (Z.gcd_nonneg (Z.max (Z.gcd z1 z2) 1) z).
  generalize (Zmax_spec (Z.gcd (Z.max (Z.gcd z1 z2) 1) z) 1).
  auto with zarith.
Qed.

Lemma Zdivide_pol_Zdivide : forall p x y, Zdivide_pol x p -> (y | x) ->  Zdivide_pol y p.
Proof.
  intros.
  induction H.
  constructor.
  apply Z.divide_trans with (1:= H0) ; assumption.
  constructor. auto.
  constructor ; auto.
Qed.

Lemma Zdivide_pol_one : forall p, Zdivide_pol 1 p.
Proof.
  induction p ; constructor ; auto.
  exists c. ring.
Qed.

Lemma Zgcd_minus : forall a b c, (a | c - b ) -> (Z.gcd a b | c).
Proof.
  intros a b c (q,Hq).
  destruct (Zgcd_is_gcd a b) as [(a',Ha) (b',Hb) _].
  set (g:=Z.gcd a b) in *; clearbody g.
  exists (q * a' + b').
  symmetry in Hq. rewrite <- Z.add_move_r in Hq.
  rewrite <- Hq, Hb, Ha. ring.
Qed.

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.
Proof.
  induction p.
  simpl.
  intros. inversion H0.
  constructor.
  apply Zgcd_minus ; auto.
  intros.
  constructor.
  simpl in H0. inversion H0 ; subst; clear H0.
  apply IHp ; auto.
  simpl. intros.
  inv H0.
  constructor.
  apply Zdivide_pol_Zdivide with (1:= H3).
  destruct (Zgcd_is_gcd a b) ; assumption.
  apply IHp2 ; assumption.
Qed.

Lemma Zdivide_pol_sub_0 : forall p a,
  Zdivide_pol a (PsubC Z.sub p 0) ->
   Zdivide_pol a p.
Proof.
  induction p.
  simpl.
  intros. inversion H.
  constructor.  replace (c - 0) with c in H1 ; auto with zarith.
  intros.
  constructor.
  simpl in H. inversion H ; subst; clear H.
  apply IHp ; auto.
  simpl. intros.
  inv H.
  constructor. auto.
  apply IHp2 ; assumption.
Qed.

Lemma Zgcd_pol_div : forall p g c,
  Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Z.sub p c).
Proof.
  induction p ; simpl.
  (* Pc *)
  intros. inv H.
  constructor.
  exists 0. now ring.
  (* Pinj *)
  intros.
  constructor.  apply IHp ; auto.
  (* PX *)
  intros g c.
  case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros.
  inv H1.
  unfold ZgcdM at 1.
  destruct (Zmax_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1];
  destruct HH1 as [HH1 HH1'] ; rewrite HH1'.
  constructor.
  apply Zdivide_pol_Zdivide with (x:= ZgcdM z1 z2).
  unfold ZgcdM.
  destruct (Zmax_spec  (Z.gcd z1 z2)  1) as [HH2 | HH2].
  destruct HH2.
  rewrite H2.
  apply Zdivide_pol_sub ; auto.
  auto with zarith.
  destruct HH2. rewrite H2.
  apply Zdivide_pol_one.
  unfold ZgcdM in HH1. unfold ZgcdM.
  destruct (Zmax_spec  (Z.gcd z1 z2)  1) as [HH2 | HH2].
  destruct HH2. rewrite H2 in *.
  destruct (Zgcd_is_gcd (Z.gcd z1 z2) z); auto.
  destruct HH2. rewrite H2.
  destruct (Zgcd_is_gcd 1  z); auto.
  apply Zdivide_pol_Zdivide with (x:= z).
  apply (IHp2 _ _ H); auto.
  destruct (Zgcd_is_gcd (ZgcdM z1 z2) z); auto.
  constructor. apply Zdivide_pol_one.
  apply Zdivide_pol_one.
Qed.

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.
Proof.
  intros.
  rewrite <- Zdiv_pol_correct ; auto.
  rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon).
  unfold eval_pol. ring.
  (**)
  apply Zgcd_pol_div ; auto.
Qed.

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 (* inconsistent *)
          else (* Could be optimised Zgcd_pol is recomputed *)
            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.
Proof.
  unfold is_pol_Z0.
  destruct p ; try discriminate.
  destruct z ; try discriminate.
  reflexivity.
Qed.

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.

Module Vars.
  Import FSetPositive.
  Include PositiveSet.

  Module Facts := FSetEqProperties.EqProperties(PositiveSet).

  Lemma mem_union_l : forall x s s',
      mem x s = true ->
      mem x (union s s') = true.
  Proof.
    intros.
    rewrite Facts.union_mem.
    rewrite H. reflexivity.
  Qed.

  Lemma mem_union_r : forall x s s',
      mem x s' = true ->
      mem x (union s s') = true.
  Proof.
    intros.
    rewrite Facts.union_mem.
    rewrite H. rewrite orb_comm. reflexivity.
  Qed.

  Lemma mem_singleton : forall p,
      mem p (singleton p) = true.
  Proof.
    apply Facts.singleton_mem_1.
  Qed.

  Lemma mem_elements : forall x v,
      mem x v = true <-> List.In x (PositiveSet.elements v).
  Proof.
    intros.
    rewrite Facts.MP.FM.elements_b.
    rewrite existsb_exists.
    unfold Facts.MP.FM.eqb.
    split ; intros.
    - destruct H as (x' & IN & EQ).
    destruct (PositiveSet.E.eq_dec x x') ; try congruence.
    subst ; auto.
    - exists x.
      split ; auto.
      destruct (PositiveSet.E.eq_dec x x) ; congruence.
  Qed.

  Definition max_element (vars : t)  :=
    fold Pos.max vars xH.

  Lemma max_element_max :
    forall x vars, mem x vars = true -> Pos.le x (max_element vars).
  Proof.
    unfold max_element.
    intros.
    rewrite mem_elements in H.
    rewrite PositiveSet.fold_1.
    set (F := (fun (a : positive) (e : PositiveSet.elt) => Pos.max e a)).
    revert H.
    assert  (((x <= 1 -> x <= fold_left F (PositiveSet.elements vars) 1)
             /\
            (List.In x (PositiveSet.elements vars) ->
             x <= fold_left F (PositiveSet.elements vars) 1))%positive).
    {
    revert x.
    generalize xH as acc.
    induction (PositiveSet.elements  vars).
    - simpl. tauto.
    - simpl.
      intros.
      destruct (IHl (F acc a) x).
      split ; intros.
      apply H.
      unfold F.
      rewrite Pos.max_le_iff.
      tauto.
      destruct H1 ; subst.
      apply H.
      unfold F.
      rewrite Pos.max_le_iff.
      simpl.
      left.
      apply Pos.le_refl.
      tauto.
    }
    tauto.
  Qed.

  Definition is_subset (v1 v2 : t) :=
    forall x, mem x v1 = true -> mem x v2 = true.

  Lemma is_subset_union_l : forall v1 v2,
      is_subset v1 (union v1 v2).
  Proof.
    unfold is_subset.
    intros.
    apply mem_union_l; auto.
  Qed.

  Lemma is_subset_union_r : forall v1 v2,
      is_subset v1 (union v2 v1).
  Proof.
    unfold is_subset.
    intros.
    apply mem_union_r; auto.
  Qed.

  End Vars.

Fixpoint vars_of_pexpr (e : PExpr Z) : Vars.t :=
  match e with
  | PEc _ => Vars.empty
  | PEX x => Vars.singleton x
  | PEadd e1 e2 | PEsub e1 e2 | PEmul e1 e2 =>
    let v1 := vars_of_pexpr e1 in
    let v2 := vars_of_pexpr e2 in
    Vars.union v1 v2
  | PEopp c => vars_of_pexpr c
  | PEpow e n => vars_of_pexpr e
  end.

Definition vars_of_formula (f : Formula Z) :=
  match f with
  | Build_Formula l o r =>
    let v1 := vars_of_pexpr l in
    let v2 := vars_of_pexpr r in
    Vars.union v1 v2
  end.

Fixpoint vars_of_bformula {TX : Type} {TG : Type} {ID : Type}
         (F : @GFormula (Formula Z) TX TG ID) : Vars.t :=
  match F with
  | TT  => Vars.empty
  | FF  => Vars.empty
  | X  p => Vars.empty
  | A a t => vars_of_formula a
  | Cj f1 f2 | D f1 f2 | I f1 _ f2 =>
                         let v1 := vars_of_bformula f1 in
                         let v2 := vars_of_bformula f2 in
                         Vars.union v1 v2
  | Tauto.N f     => vars_of_bformula f
  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)).

Section BOUND.
  Context {TX TG ID : Type}.

  Variable tag_of_var : positive -> positive -> option bool -> TG.

  Definition bound_vars  (fr : positive)
             (v : Vars.t) : @GFormula (Formula Z) TX TG ID :=
    Vars.fold (fun k acc =>
                 let y := (xO (fr + k)) in
                 let z := (xI (fr + k)) in
                 Cj
                   (Cj (A (mk_eq_pos k y z) (tag_of_var fr k None))
                       (Cj (A (bound_var y) (tag_of_var fr k (Some false)))
                           (A (bound_var z) (tag_of_var fr k (Some true)))))
                   acc) v TT.

  Definition bound_problem  (F : @GFormula (Formula Z) TX TG ID) : GFormula :=
    let v := vars_of_bformula F in
    I (bound_vars (Pos.succ (Vars.max_element v)) v) None F.

  Definition bound_problem_fr (fr : positive) (F : @GFormula (Formula Z) TX TG ID) : GFormula :=
    let v := vars_of_bformula F in
    I (bound_vars fr v) None F.

End BOUND.

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 e pf1 pf2 =>
      match ZChecker ((e,NonStrict)::l) pf1 , ZChecker ((
*)

    | 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)
    | EnumProof _ _ l => S (List.fold_right (fun pf x => Max.max (bdepth pf) x)   O l)
  end.

Require Import Wf_nat.

Lemma in_bdepth : forall l a b  y, In y l ->  ltof ZArithProof bdepth y (EnumProof a b  l).
Proof.
  induction l.
  (* nil *)
  simpl.
  tauto.
  (* cons *)
  simpl.
  intros.
  destruct H.
  subst.
  unfold ltof.
  simpl.
  generalize (         (fold_right
            (fun (pf : ZArithProof) (x : nat) => Max.max (bdepth pf) x) 0%nat l)).
  intros.
  generalize (bdepth y) ; intros.
  generalize (Max.max_l n0 n) (Max.max_r n0 n).
  auto with zarith.
  generalize (IHl a0 b  y  H).
  unfold ltof.
  simpl.
  generalize (      (fold_right (fun (pf : ZArithProof) (x : nat) => Max.max (bdepth pf) x) 0%nat
         l)).
  intros.
  generalize (Max.max_l (bdepth a) n) (Max.max_r (bdepth a) n).
  auto with zarith.
Qed.

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'.
Proof.
  intros.
  apply (eval_Psatz_Sound Zsor ZSORaddon) with (l:=l) (e:= w) ; auto.
  apply make_conj_in ; auto.
Qed.

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)).
Proof.
  unfold nformula_of_cutting_plane.
  unfold eval_nformula. unfold RingMicromega.eval_nformula.
  unfold eval_op1.
  intros.
  rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon).
  simpl.
  (**)
  unfold makeCuttingPlane in H0.
  revert H0.
  case_eq (Zgcd_pol e) ; intros g c0.
  generalize (Zgt_cases g 0) ; destruct (Z.gtb g 0).
  intros.
  inv H2.
  change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *.
  apply Zgcd_pol_correct_lt with (env:=env) in H1.
  generalize (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0).
  auto with zarith.
  auto with zarith.
  (* g <= 0 *)
  intros. inv H2. auto with zarith.
Qed.

Lemma cutting_plane_sound : forall env f p,
  eval_nformula env f ->
  genCuttingPlane f = Some p ->
   eval_nformula env (nformula_of_cutting_plane p).
Proof.
  unfold genCuttingPlane.
  destruct f as [e op].
  destruct op.
  (* Equal *)
  destruct p as [[e' z] op].
  case_eq (Zgcd_pol e) ; intros g c.
  case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))) ; [discriminate|].
  case_eq (makeCuttingPlane e).
  intros.
  inv H3.
  unfold makeCuttingPlane in H.
  rewrite H1 in H.
  revert H.
  change (eval_pol env e = 0) in H2.
  case_eq (Z.gtb g 0).
  intros.
  rewrite <- Zgt_is_gt_bool in H.
  rewrite Zgcd_pol_correct_lt with (1:= H1)  in H2; auto with zarith.
  unfold nformula_of_cutting_plane.
  change (eval_pol env (padd e' (Pc z)) = 0).
  inv H3.
  rewrite eval_pol_add.
  set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub e c) g)) in *; clearbody x.
  simpl.
  rewrite andb_false_iff in H0.
  destruct H0.
  rewrite Zgt_is_gt_bool in H ; congruence.
  rewrite andb_false_iff in H0.
  destruct H0.
  rewrite negb_false_iff in H0.
  apply Zeq_bool_eq in H0.
  subst. simpl.
  rewrite Z.add_0_r, Z.mul_eq_0 in H2.
  intuition auto with zarith.
  rewrite negb_false_iff in H0.
  apply Zeq_bool_eq in H0.
  assert (HH := Zgcd_is_gcd g c).
  rewrite H0 in HH.
  inv HH.
  apply Zdivide_opp_r in H4.
  rewrite Zdivide_ceiling ; auto.
  apply Z.sub_move_0_r.
  apply Z.div_unique_exact ; auto with zarith.
  intros.
  unfold nformula_of_cutting_plane.
  inv H3.
  change (eval_pol env (padd e' (Pc 0)) = 0).
  rewrite eval_pol_add.
  simpl.
  auto with zarith.
  (* NonEqual *)
  intros.
  inv H0.
  unfold eval_nformula in *.
  unfold RingMicromega.eval_nformula in *.
  unfold nformula_of_cutting_plane.
  unfold eval_op1 in *.
  rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon).
  simpl. auto with zarith.
  (* Strict *)
  destruct p as [[e' z] op].
  case_eq (makeCuttingPlane (PsubC Z.sub e 1)).
  intros.
  inv H1.
  apply makeCuttingPlane_ns_sound with (env:=env) (2:= H).
  simpl in *.
  rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon).
  auto with zarith.
  (* NonStrict *)
  destruct p as [[e' z] op].
  case_eq (makeCuttingPlane e).
  intros.
  inv H1.
  apply makeCuttingPlane_ns_sound with (env:=env) (2:= H).
  assumption.
Qed.

Lemma  genCuttingPlaneNone : forall env f,
  genCuttingPlane f = None ->
  eval_nformula env f -> False.
Proof.
  unfold genCuttingPlane.
  destruct f.
  destruct o.
  case_eq (Zgcd_pol p) ; intros g c.
  case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))).
  intros.
  flatten_bool.
  rewrite negb_true_iff in H5.
  apply Zeq_bool_neq in H5.
  rewrite <- Zgt_is_gt_bool in H3.
  rewrite negb_true_iff in H.
  apply Zeq_bool_neq in H.
  change (eval_pol env p = 0) in H2.
  rewrite Zgcd_pol_correct_lt with (1:= H0) in H2; auto with zarith.
  set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) in *; clearbody x.
  contradict H5.
  apply Zis_gcd_gcd; auto with zarith.
  constructor; auto with zarith.
  exists (-x).
  rewrite Z.mul_opp_l, Z.mul_comm; auto with zarith.
  (**)
  destruct (makeCuttingPlane p);  discriminate.
  discriminate.
  destruct (makeCuttingPlane (PsubC Z.sub p 1)) ; discriminate.
  destruct (makeCuttingPlane p) ; discriminate.
Qed.

Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl  (eval_nformula env)  l False.
Proof.
  induction w    using (well_founded_ind (well_founded_ltof _ bdepth)).
  destruct w as [ | w pf | w pf | w1 w2 pf].
  (* DoneProof *)
  simpl. discriminate.
  (* RatProof *)
  simpl.
  intro l. case_eq (eval_Psatz l w) ; [| discriminate].
  intros f Hf.
  case_eq (Zunsat f).
  intros.
  apply (checker_nf_sound Zsor ZSORaddon l w).
  unfold check_normalised_formulas.  unfold eval_Psatz in Hf. rewrite Hf.
  unfold Zunsat in H0. assumption.
  intros.
  assert (make_impl  (eval_nformula env) (f::l) False).
   apply H with (2:= H1).
   unfold ltof.
   simpl.
   auto with arith.
  destruct f.
  rewrite <- make_conj_impl in H2.
  rewrite make_conj_cons in H2.
  rewrite <- make_conj_impl.
  intro.
  apply H2.
  split ; auto.
  apply eval_Psatz_sound with (2:= Hf) ; assumption.
  (* CutProof *)
  simpl.
  intro l.
  case_eq (eval_Psatz l w) ; [ | discriminate].
  intros f' Hlc.
  case_eq (genCuttingPlane f').
  intros.
  assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False).
   eapply (H pf) ; auto.
   unfold ltof.
   simpl.
   auto with arith.
  rewrite <- make_conj_impl in H2.
  rewrite make_conj_cons in H2.
  rewrite <- make_conj_impl.
  intro.
  apply H2.
  split ; auto.
  apply eval_Psatz_sound with (env:=env) in Hlc.
  apply cutting_plane_sound with (1:= Hlc) (2:= H0).
  auto.
  (* genCuttingPlane = None *)
  intros.
  rewrite <- make_conj_impl.
  intros.
  apply eval_Psatz_sound with (2:= Hlc) in H2.
  apply genCuttingPlaneNone with (2:= H2) ; auto.
  (* EnumProof *)
  intro.
  simpl.
  case_eq (eval_Psatz l w1) ; [  | discriminate].
  case_eq (eval_Psatz l w2) ; [  | discriminate].
  intros f1 Hf1 f2 Hf2.
  case_eq (genCuttingPlane f2).
  destruct p as [ [p1 z1] op1].
  case_eq (genCuttingPlane f1).
  destruct p as [ [p2 z2] op2].
  case_eq (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd p1 p2)).
  intros Hcond.
  flatten_bool.
  rename H1 into HZ0.
  rename H2 into Hop1.
  rename H3 into Hop2.
  intros HCutL HCutR Hfix env.
  (* get the bounds of the enum *)
  rewrite <- make_conj_impl.
  intro.
  assert (-z1 <= eval_pol env p1 <= z2).
   split.
   apply  eval_Psatz_sound with (env:=env) in Hf2 ; auto.
   apply cutting_plane_sound with (1:= Hf2) in HCutR.
   unfold nformula_of_cutting_plane in HCutR.
   unfold eval_nformula in HCutR.
   unfold RingMicromega.eval_nformula in HCutR.
   change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutR.
   unfold eval_op1 in HCutR.
   destruct op1 ; simpl in Hop1 ; try discriminate;
     rewrite eval_pol_add in HCutR; simpl in HCutR; auto with zarith.
   (**)
   apply is_pol_Z0_eval_pol with (env := env) in HZ0.
   rewrite eval_pol_add in HZ0.
   replace (eval_pol env p1) with (- eval_pol env p2) by omega.
   apply  eval_Psatz_sound with (env:=env) in Hf1 ; auto.
   apply cutting_plane_sound with (1:= Hf1) in HCutL.
   unfold nformula_of_cutting_plane in HCutL.
   unfold eval_nformula in HCutL.
   unfold RingMicromega.eval_nformula in HCutL.
   change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutL.
   unfold eval_op1 in HCutL.
   rewrite eval_pol_add in HCutL. simpl in HCutL.
   destruct op2 ; simpl in Hop2 ; try discriminate ;  omega.
  revert Hfix.
  match goal with
    | |- context[?F pf (-z1) z2 = true] => set (FF := F)
  end.
  intros.
  assert (HH :forall x, -z1 <= x <= z2 -> exists pr,
    (In pr pf /\
      ZChecker  ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z).
  clear HZ0 Hop1 Hop2 HCutL HCutR H0 H1.
  revert Hfix.
  generalize (-z1). clear z1. intro z1.
  revert z1 z2.
  induction pf;simpl ;intros.
  generalize (Zgt_cases z1 z2).
  destruct (Z.gtb z1 z2).
  intros.
  apply False_ind ; omega.
  discriminate.
  flatten_bool.
  assert (HH:(x = z1 \/ z1 +1 <=x)%Z) by omega.
  destruct HH.
  subst.
  exists a ; auto.
  assert (z1 + 1 <= x <= z2)%Z by omega.
  elim IHpf with (2:=H2) (3:= H4).
  destruct H4.
  intros.
  exists x0 ; split;tauto.
  intros until 1.
  apply H ; auto.
  unfold ltof in *.
  simpl in *.
  zify. omega.
  (*/asser *)
  destruct (HH _ H1) as [pr [Hin Hcheker]].
  assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False).
   apply (H pr);auto.
   apply in_bdepth ; auto.
  rewrite <- make_conj_impl in H2.
  apply H2.
  rewrite  make_conj_cons.
  split ;auto.
  unfold  eval_nformula.
  unfold RingMicromega.eval_nformula.
  simpl.
  rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon).
  unfold eval_pol. ring.
  discriminate.
  (* No cutting plane *)
  intros.
  rewrite <- make_conj_impl.
  intros.
  apply eval_Psatz_sound with (2:= Hf1) in H3.
  apply genCuttingPlaneNone with (2:= H3) ; auto.
  (* No Cutting plane (bis) *)
  intros.
  rewrite <- make_conj_impl.
  intros.
  apply eval_Psatz_sound with (2:= Hf2) in H2.
  apply genCuttingPlaneNone with (2:= H2) ; auto.
Qed.

Definition ZTautoChecker  (f : BFormula (Formula Z)) (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_f (fun x => x) (Zeval_formula env)  f.
Proof.
  intros f w.
  unfold ZTautoChecker.
  apply tauto_checker_sound with (eval' := eval_nformula).
  - apply Zeval_nformula_dec.
  - intros until env.
  unfold eval_nformula. unfold RingMicromega.eval_nformula.
  destruct t.
  apply (check_inconsistent_sound Zsor ZSORaddon) ; auto.
  - unfold Zdeduce. apply (nformula_plus_nformula_correct Zsor ZSORaddon).
  -
    intros env t tg.
    rewrite normalise_correct ; auto.
  -
    intros env t tg.
    rewrite negate_correct ; auto.
  - intros t w0.
    unfold eval_tt.
    intros.
    rewrite make_impl_map with (eval := eval_nformula env).
    eapply ZChecker_sound; eauto.
    tauto.
Qed.

Record is_diff_env_elt (fr : positive) (env env' : positive -> Z) (x:positive):=
  {
    eq_env  : env x = env' x;
    eq_diff : env x = env' (xO (fr+ x)) - env' (xI (fr + x));
    pos_xO  : env' (xO (fr+x)) >= 0;
    pos_xI  : env' (xI (fr+x)) >= 0;
  }.

Definition is_diff_env  (s : Vars.t) (env env' : positive -> Z) :=
  let fr := Pos.succ (Vars.max_element s) in
  forall x, Vars.mem x s = true ->
            is_diff_env_elt fr env env' x.

Definition mk_diff_env  (s : Vars.t) (env : positive -> Z) :=
  let fr := Vars.max_element s in
  fun x =>
    if Pos.leb x fr
    then env x
    else
      let fr' := Pos.succ fr in
      match x with
      | xO x => if Z.leb (env (x - fr')%positive) 0
                then 0 else env (x -fr')%positive
      | xI x => if Z.leb (env (x - fr')%positive) 0
                then - (env (x - fr')%positive) else 0
      | xH   => 0
      end.

Lemma le_xO : forall x, (x <= xO x)%positive.
Proof.
  intros.
  change x with (1 * x)%positive at 1.
  change (xO x) with (2 * x)%positive.
  apply Pos.mul_le_mono.
  compute. congruence.
  apply Pos.le_refl.
Qed.

Lemma leb_xO_false :
  (forall x y,  x <=? y = false ->
             xO x <=? y = false)%positive.
Proof.
  intros.
  rewrite Pos.leb_nle in *.
  intro. apply H.
  eapply Pos.le_trans ; eauto.
  apply le_xO.
Qed.

Lemma leb_xI_false :
  (forall x y,  x <=? y = false ->
             xI x <=? y = false)%positive.
Proof.
  intros.
  rewrite Pos.leb_nle in *.
  intro. apply H.
  eapply Pos.le_trans ; eauto.
  generalize (le_xO x).
  intros.
  eapply Pos.le_trans ; eauto.
  change (xI x) with (Pos.succ (xO x))%positive.
  apply Pos.lt_le_incl.
  apply Pos.lt_succ_diag_r.
Qed.

Lemma is_diff_env_ex : forall s env,
    is_diff_env s env (mk_diff_env s env).
Proof.
  intros.
  unfold is_diff_env, mk_diff_env.
  intros.
  assert
    ((Pos.succ (Vars.max_element s) + x <=? Vars.max_element s  = false)%positive).
  {
      rewrite Pos.leb_nle.
      intro.
      eapply (Pos.lt_irrefl (Pos.succ (Vars.max_element s) + x)).
      eapply Pos.le_lt_trans ; eauto.
      generalize (Pos.lt_succ_diag_r (Vars.max_element s)).
      intro.
      eapply Pos.lt_trans ; eauto.
      apply Pos.lt_add_r.
  }
  constructor.
  - apply Vars.max_element_max in H.
    rewrite <- Pos.leb_le   in H.
    rewrite H. auto.
  -
    rewrite  leb_xO_false by auto.
    rewrite leb_xI_false by auto.
    rewrite Pos.add_comm.
    rewrite Pos.add_sub.
    destruct (env x <=? 0); ring.
  - rewrite  leb_xO_false by auto.
    rewrite Pos.add_comm.
    rewrite Pos.add_sub.
    destruct (env x <=? 0) eqn:EQ.
    apply Z.le_ge.
    apply Z.le_refl.
    rewrite Z.leb_gt in EQ.
    apply Z.le_ge.
    apply Z.lt_le_incl.
    auto.
  - rewrite  leb_xI_false by auto.
    rewrite Pos.add_comm.
    rewrite Pos.add_sub.
    destruct (env x <=? 0) eqn:EQ.
    rewrite Z.leb_le in EQ.
    apply Z.le_ge.
    apply Z.opp_nonneg_nonpos; auto.
    apply Z.le_ge.
    apply Z.le_refl.
Qed.

Lemma env_bounds : forall tg env s,
    let fr := Pos.succ (Vars.max_element s) in
    exists env', is_diff_env s env env'
                   /\
                   eval_bf  (Zeval_formula env') (bound_vars tg fr s).
Proof.
  intros.
  assert (DIFF:=is_diff_env_ex s env).
  exists (mk_diff_env s env). split ; auto.
  unfold bound_vars.
  rewrite FSetPositive.PositiveSet.fold_1.
  revert DIFF.
  set (env' := mk_diff_env s env).
  intro.
  assert (ACC : eval_bf  (Zeval_formula env') TT ).
  {
    simpl. auto.
  }
  revert ACC.
  match goal with
  | |- context[@TT ?A ?B ?C ?D] => generalize (@TT A B C D) as acc
  end.
  unfold is_diff_env in DIFF.
  assert (DIFFL : forall x, In x (FSetPositive.PositiveSet.elements s) ->
                            (x < fr)%positive /\
                            is_diff_env_elt fr env env' x).
  {
    intros.
    rewrite <- Vars.mem_elements in H.
    split.
    apply Vars.max_element_max in H.
    unfold fr in *.
    eapply Pos.le_lt_trans ; eauto.
    apply Pos.lt_succ_diag_r.
    apply DIFF; auto.
  }
  clear DIFF.
  match goal with
  | |- context[fold_left ?F _ _] =>
    set (FUN := F)
  end.
  induction (FSetPositive.PositiveSet.elements s).
  - simpl; auto.
  - simpl.
    intros.
    eapply IHl ; eauto.
    + intros. apply DIFFL.
      simpl ; auto.
    + unfold FUN.
      simpl.
      split ; auto.
      assert (HYP : (a < fr /\ is_diff_env_elt fr env env' a)%positive).
      {
        apply DIFFL.
        simpl.  tauto.
      }
      destruct HYP as (LT & DIFF).
      destruct DIFF.
      rewrite <- eq_env0.
      tauto.
Qed.

Definition agree_env (v : Vars.t) (env env' : positive -> Z) : Prop :=
  forall x, Vars.mem x v = true -> env x = env' x.

Lemma agree_env_subset : forall s1 s2 env env',
    agree_env s1 env env' ->
    Vars.is_subset s2 s1 ->
    agree_env s2 env env'.
Proof.
  unfold agree_env.
  intros.
  apply H. apply H0; auto.
Qed.

Lemma agree_env_union : forall s1 s2 env env',
    agree_env (Vars.union s1 s2) env env' ->
    agree_env s1 env env' /\ agree_env s2 env env'.
Proof.
  split;
  eapply agree_env_subset; eauto.
  apply Vars.is_subset_union_l.
  apply Vars.is_subset_union_r.
Qed.

Lemma agree_env_eval_expr :
  forall env env' e
         (AGREE : agree_env (vars_of_pexpr e)  env env'),
  Zeval_expr env e =  Zeval_expr env' e.
Proof.
  induction e; simpl;intros;
    try (apply agree_env_union in AGREE; destruct AGREE);  try f_equal ; auto.
  - intros ; apply AGREE.
    apply Vars.mem_singleton.
Qed.

Lemma agree_env_eval_bf :
  forall env env' f
         (AGREE: agree_env (vars_of_bformula f) env env'),
    eval_bf (Zeval_formula env') f <->
    eval_bf (Zeval_formula env) f.
Proof.
  induction f; simpl; intros ;
    try (apply agree_env_union in AGREE; destruct AGREE) ; try intuition fail.
  -
    unfold Zeval_formula.
    destruct t.
    simpl in * ; intros.
    apply agree_env_union in AGREE ; destruct AGREE.
    rewrite <- agree_env_eval_expr with (env:=env) by auto.
    rewrite <- agree_env_eval_expr with (e:= Frhs) (env:=env) by auto.
    tauto.
Qed.

Lemma bound_problem_sound : forall tg f,
    (forall env' : PolEnv Z,
        eval_bf  (Zeval_formula env')
                 (bound_problem tg f)) ->
    forall env,
      eval_bf (Zeval_formula env) f.
Proof.
  intros.
  unfold bound_problem in H.
  destruct (env_bounds tg env (vars_of_bformula f))
           as (env' & DIFF & EVAL).
  simpl in H.
  apply H in EVAL.
  eapply agree_env_eval_bf ; eauto.
  unfold is_diff_env, agree_env in *.
  intros.
  apply DIFF in H0.
  destruct H0.
  intuition.
Qed.

Definition ZTautoCheckerExt (f : BFormula (Formula Z)) (w : list ZArithProof) : bool :=
  ZTautoChecker (bound_problem (fun _ _ _ => tt) f) w.

Lemma ZTautoCheckerExt_sound : forall f w, ZTautoCheckerExt f w = true -> forall env, eval_bf (Zeval_formula env)  f.
Proof.
  intros.
  unfold ZTautoCheckerExt in H.
  specialize (ZTautoChecker_sound _ _ H).
  intros ; apply bound_problem_sound with (tg:= fun _ _ _ => tt); auto.
Qed.

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
    | 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
  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 varmap_type := VarMap.t Z. *)
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).

(* Local Variables: *)
(* coding: utf-8 *)
(* End: *)

¤ Dauer der Verarbeitung: 0.32 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.