Ajout de la contrib sur les graphes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1857 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 417 insertions, 0 deletions

diff --git a/contrib/graphs/zcgraph.v b/contrib/graphs/zcgraph.v
new file mode 100644
index 000000000..64d1f9555
--- /dev/null
+++ b/contrib/graphs/zcgraph.v
@@ -0,0 +1,417 @@
+
+(*s The decision procedure is instantiated for Z *)
+
+Require cgraph.
+Require ZArith.
+Require Addr.
+Require Addec.
+
+Inductive ZCGForm : Set :=
+      ZCGle : ad -> ad -> ZCGForm (* x<=y *)
+    | ZCGge : ad -> ad -> ZCGForm (* x>=y *)
+    | ZCGlt : ad -> ad -> ZCGForm (* x<y *)
+    | ZCGgt : ad -> ad -> ZCGForm (* x>y *)
+    | ZCGlep : ad -> ad -> Z -> ZCGForm (* x<=y+k *)
+    | ZCGgep : ad -> ad -> Z -> ZCGForm (* x>=y+k *)
+    | ZCGltp : ad -> ad -> Z -> ZCGForm (* x<y+k *)
+    | ZCGgtp : ad -> ad -> Z -> ZCGForm (* x>y+k *)
+    | ZCGlem : ad -> ad -> Z -> ZCGForm (* x+k<=y *)
+    | ZCGgem : ad -> ad -> Z -> ZCGForm (* x+k>=y *)
+    | ZCGltm : ad -> ad -> Z -> ZCGForm (* x+k<y *)
+    | ZCGgtm : ad -> ad -> Z -> ZCGForm (* x+k>y *)
+    | ZCGlepm : ad -> ad -> Z -> Z -> ZCGForm (* x+k<=y+k' *)
+    | ZCGgepm : ad -> ad -> Z -> Z -> ZCGForm (* x+k>=y+k' *)
+    | ZCGltpm : ad -> ad -> Z -> Z -> ZCGForm (* x+k<y+k' *)
+    | ZCGgtpm : ad -> ad -> Z -> Z -> ZCGForm (* x+k>y+k' *)
+    | ZCGeq : ad -> ad -> ZCGForm (* x=y *)
+    | ZCGeqp : ad -> ad -> Z -> ZCGForm (* x=y+k *)
+    | ZCGeqm : ad -> ad -> Z -> ZCGForm (* x+k=y *)
+    | ZCGeqpm : ad -> ad -> Z -> Z -> ZCGForm (* x+k=y+k' *)
+    | ZCGzylem : ad -> Z -> ZCGForm (* k<=y *)
+    | ZCGzygem : ad -> Z -> ZCGForm (* k>=y *)
+    | ZCGzyltm : ad -> Z -> ZCGForm (* k<y *)
+    | ZCGzygtm : ad -> Z -> ZCGForm (* k>y *)
+    | ZCGzylepm : ad -> Z -> Z -> ZCGForm (* k<=y+k' *)
+    | ZCGzygepm : ad -> Z -> Z -> ZCGForm (* k>=y+k' *)
+    | ZCGzyltpm : ad -> Z -> Z -> ZCGForm (* k<y+k' *)
+    | ZCGzygtpm : ad -> Z -> Z -> ZCGForm (* k>y+k' *)
+    | ZCGzyeqm : ad -> Z -> ZCGForm (* k=y *)
+    | ZCGzyeqpm : ad -> Z -> Z -> ZCGForm (* k=y+k' *)
+    | ZCGxzlep : ad -> Z -> ZCGForm (* x<=k *)
+    | ZCGxzgep : ad -> Z -> ZCGForm (* x>=k *)
+    | ZCGxzltp : ad -> Z -> ZCGForm (* x<k *)
+    | ZCGxzgtp : ad -> Z -> ZCGForm (* x>k *)
+    | ZCGxzlepm : ad -> Z -> Z -> ZCGForm (* x+k<=k' *)
+    | ZCGxzgepm : ad -> Z -> Z -> ZCGForm (* x+k>=k' *)
+    | ZCGxzltpm : ad -> Z -> Z -> ZCGForm (* x+k<k' *)
+    | ZCGxzgtpm : ad -> Z -> Z -> ZCGForm (* x+k>k' *)
+    | ZCGxzeqp : ad -> Z -> ZCGForm (* x=k *)
+    | ZCGxzeqpm : ad -> Z -> Z -> ZCGForm (* x+k=k' *)
+    | ZCGzzlep : Z -> Z -> ZCGForm (* k<=k' *)
+    | ZCGzzltp : Z -> Z -> ZCGForm (* k<k' *)
+    | ZCGzzgep : Z -> Z -> ZCGForm (* k>=k' *)
+    | ZCGzzgtp : Z -> Z -> ZCGForm (* k>k' *)
+    | ZCGzzeq : Z -> Z -> ZCGForm (* k=k' *)
+    | ZCGand : ZCGForm -> ZCGForm -> ZCGForm
+    | ZCGor : ZCGForm -> ZCGForm -> ZCGForm
+    | ZCGimp : ZCGForm -> ZCGForm -> ZCGForm
+    | ZCGnot : ZCGForm -> ZCGForm
+    | ZCGiff : ZCGForm -> ZCGForm -> ZCGForm.
+
+Definition ZCG_eval := (CGeval Z Zplus Zle_bool).
+
+(*s Translation of formula on Z into a constraint graph formula. 
+    we reserve [ad_z] as the "zero" variable, 
+    i.e., the one that is anchored at the value `0`. *)
+
+Fixpoint ZCGtranslate [f:ZCGForm] : (CGForm Z) :=
+  Cases f of
+      (ZCGle x y) => (CGleq Z x y `0`)
+    | (ZCGge x y) => (CGleq Z y x `0`)
+    | (ZCGlt x y) => (CGleq Z x y `-1`)
+    | (ZCGgt x y) => (CGleq Z y x `-1`)
+    | (ZCGlep x y k) => (CGleq Z x y k)
+    | (ZCGgep x y k) => (CGleq Z y x (Zopp k))
+    | (ZCGltp x y k) => (CGleq Z x y `k-1`)
+    | (ZCGgtp x y k) => (CGleq Z y x (Zopp `k+1`))
+    | (ZCGlem x y k) => (CGleq Z x y (Zopp k))
+    | (ZCGgem x y k) => (CGleq Z y x k)
+    | (ZCGltm x y k) => (CGleq Z x y (Zopp `k+1`))
+    | (ZCGgtm x y k) => (CGleq Z y x `k-1`)
+    | (ZCGlepm x y k k') => (CGleq Z x y `k'-k`)
+    | (ZCGgepm x y k k') => (CGleq Z y x `k-k'`)
+    | (ZCGltpm x y k k') => (CGleq Z x y `k'-k-1`)
+    | (ZCGgtpm x y k k') => (CGleq Z y x `k-k'-1`)
+    | (ZCGeq x y) => (CGeq Z x y `0`)
+    | (ZCGeqp x y k) => (CGeq Z x y k)
+    | (ZCGeqm x y k) => (CGeq Z y x k)
+    | (ZCGeqpm x y k k') => (CGeq Z x y `k'-k`)
+    | (ZCGzylem y k) => (CGleq Z ad_z y (Zopp k)) 
+    | (ZCGzygem y k) => (CGleq Z y ad_z k) 
+    | (ZCGzyltm y k) => (CGleq Z ad_z y (Zopp `k+1`))
+    | (ZCGzygtm y k) => (CGleq Z y ad_z `k-1`)
+    | (ZCGzylepm y k k') => (CGleq Z ad_z y `k'-k`)
+    | (ZCGzygepm y k k') => (CGleq Z y ad_z `k-k'`)
+    | (ZCGzyltpm y k k') => (CGleq Z ad_z y `k'-k-1`)
+    | (ZCGzygtpm y k k') => (CGleq Z y ad_z `k-k'-1`)
+    | (ZCGzyeqm y k) => (CGeq Z y ad_z k)
+    | (ZCGzyeqpm y k k') => (CGeq Z y ad_z `k-k'`)
+    | (ZCGxzlep x k) => (CGleq Z x ad_z k)
+    | (ZCGxzgep x k) => (CGleq Z ad_z x (Zopp k))
+    | (ZCGxzltp x k) => (CGleq Z x ad_z `k-1`)
+    | (ZCGxzgtp x k) => (CGleq Z ad_z x (Zopp `k+1`))
+    | (ZCGxzlepm x k k') => (CGleq Z x ad_z `k'-k`)
+    | (ZCGxzgepm x k k') => (CGleq Z ad_z x `k-k'`)
+    | (ZCGxzltpm x k k') => (CGleq Z x ad_z `k'-k-1`)
+    | (ZCGxzgtpm x k k') => (CGleq Z ad_z x `k-k'-1`)
+    | (ZCGxzeqp x k) => (CGeq Z x ad_z k)
+    | (ZCGxzeqpm x k k') => (CGeq Z x ad_z `k'-k`)
+    | (ZCGzzlep k k') => (CGleq Z ad_z ad_z `k'-k`)
+    | (ZCGzzltp k k') => (CGleq Z ad_z ad_z `k'-k-1`)
+    | (ZCGzzgep k k') => (CGleq Z ad_z ad_z `k-k'`)
+    | (ZCGzzgtp k k') => (CGleq Z ad_z ad_z `k-k'-1`)
+    | (ZCGzzeq k k') => (CGeq Z ad_z ad_z `k-k'`)
+    | (ZCGand f0 f1) => (CGand Z (ZCGtranslate f0) (ZCGtranslate f1))
+    | (ZCGor f0 f1) => (CGor Z (ZCGtranslate f0) (ZCGtranslate f1))
+    | (ZCGimp f0 f1) => (CGimp Z (ZCGtranslate f0) (ZCGtranslate f1))
+    | (ZCGnot f0) => (CGnot Z (ZCGtranslate f0))
+    | (ZCGiff f0 f1) => (CGand Z (CGimp Z (ZCGtranslate f0) (ZCGtranslate f1))
+                                 (CGimp Z (ZCGtranslate f1) (ZCGtranslate f0)))
+  end.
+
+Section ZCGevalDef.
+
+  Variable rho : ad -> Z.
+
+Fixpoint ZCGeval [f:ZCGForm] : Prop :=
+    Cases f of
+      (ZCGle x y) => `(rho x)<=(rho y)`
+    | (ZCGge x y) => `(rho x)>=(rho y)`
+    | (ZCGlt x y) => `(rho x)<(rho y)`
+    | (ZCGgt x y) => `(rho x)>(rho y)`
+    | (ZCGlep x y k) => `(rho x)<=(rho y)+k`
+    | (ZCGgep x y k) => `(rho x)>=(rho y)+k`
+    | (ZCGltp x y k) => `(rho x)<(rho y)+k`
+    | (ZCGgtp x y k) => `(rho x)>(rho y)+k`
+    | (ZCGlem x y k) => `(rho x)+k<=(rho y)`
+    | (ZCGgem x y k) => `(rho x)+k>=(rho y)`
+    | (ZCGltm x y k) => `(rho x)+k<(rho y)`
+    | (ZCGgtm x y k) => `(rho x)+k>(rho y)`
+    | (ZCGlepm x y k k') => `(rho x)+k<=(rho y)+k'`
+    | (ZCGgepm x y k k') => `(rho x)+k>=(rho y)+k'`
+    | (ZCGltpm x y k k') => `(rho x)+k<(rho y)+k'`
+    | (ZCGgtpm x y k k') => `(rho x)+k>(rho y)+k'`
+    | (ZCGeq x y) => `(rho x)=(rho y)`
+    | (ZCGeqp x y k) => `(rho x)=(rho y)+k`
+    | (ZCGeqm x y k) => `(rho x)+k=(rho y)`
+    | (ZCGeqpm x y k k') => `(rho x)+k=(rho y)+k'`
+    | (ZCGzylem y k) => `k<=(rho y)`
+    | (ZCGzygem y k) => `k>=(rho y)`
+    | (ZCGzyltm y k) => `k<(rho y)`
+    | (ZCGzygtm y k) => `k>(rho y)`
+    | (ZCGzylepm y k k') => `k<=(rho y)+k'`
+    | (ZCGzygepm y k k') => `k>=(rho y)+k'`
+    | (ZCGzyltpm y k k') => `k<(rho y)+k'`
+    | (ZCGzygtpm y k k') => `k>(rho y)+k'`
+    | (ZCGzyeqm y k) => `k=(rho y)`
+    | (ZCGzyeqpm y k k') => `k=(rho y)+k'`
+    | (ZCGxzlep x k) => `(rho x)<=k`
+    | (ZCGxzgep x k) => `(rho x)>=k`
+    | (ZCGxzltp x k) => `(rho x)<k`
+    | (ZCGxzgtp x k) => `(rho x)>k`
+    | (ZCGxzlepm x k k') => `(rho x)+k<=k'`
+    | (ZCGxzgepm x k k') => `(rho x)+k>=k'`
+    | (ZCGxzltpm x k k') => `(rho x)+k<k'`
+    | (ZCGxzgtpm x k k') => `(rho x)+k>k'`
+    | (ZCGxzeqp x k) => `(rho x)=k`
+    | (ZCGxzeqpm x k k') => `(rho x)+k=k'`
+    | (ZCGzzlep k k') => `k<=k'`
+    | (ZCGzzltp k k') => `k<k'`
+    | (ZCGzzgep k k') => `k>=k'`
+    | (ZCGzzgtp k k') => `k>k'`
+    | (ZCGzzeq k k') => `k=k'`
+    | (ZCGand f0 f1) => (ZCGeval f0) /\ (ZCGeval f1)
+    | (ZCGor f0 f1) => (ZCGeval f0) \/ (ZCGeval f1)
+    | (ZCGimp f0 f1) => (ZCGeval f0) -> (ZCGeval f1)
+    | (ZCGnot f0) => ~(ZCGeval f0)
+    | (ZCGiff f0 f1) => (ZCGeval f0) <-> (ZCGeval f1)
+  end.
+
+  Variable Zrho_zero : (rho ad_z)=ZERO.
+
+Lemma ZCGeval_correct 
+  : (f:ZCGForm) (ZCGeval f) <-> (ZCG_eval rho (ZCGtranslate f)).
+  Proof.
+    Induction f; Simpl. Intros. Rewrite Zero_right. Apply Zle_is_le_bool.
+    Intros. Rewrite Zero_right. Apply Zge_is_le_bool.
+    Intros. Exact (Zlt_is_le_bool (rho a) (rho a0)).
+    Intros. Exact (Zgt_is_le_bool (rho a) (rho a0)).
+    Intros. Apply Zle_is_le_bool.
+    Intros. Apply iff_trans with b:=`(rho a0)+z <= (rho a)`. Apply Zge_iff_le.
+    Apply iff_trans with b:=`(rho a0) <= (rho a)-z`. Apply Zle_plus_swap.
+    Unfold Zminus. Apply Zle_is_le_bool.
+    Intros. Apply iff_trans with b:=(Zle_bool (rho a) `(rho a0)+z-1`)=true. Apply Zlt_is_le_bool.
+    Unfold 1 Zminus. Rewrite Zplus_assoc_r. Split; Intro; Assumption.
+    Intros. Apply iff_trans with b:=`(rho a0)+z < (rho a)`. Apply Zgt_iff_lt.
+    Apply iff_trans with `(rho a0) < (rho a)-z`. Apply Zlt_plus_swap.
+    Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool (rho a0) `(rho a)-z`).
+    Intros. Apply iff_trans with b:=`(rho a) <= (rho a0)-z`. Apply Zle_plus_swap.
+    Unfold Zminus. Apply Zle_is_le_bool.
+    Intros. Apply Zge_is_le_bool.
+    Intros. Apply iff_trans with b:=`(rho a) < (rho a0)-z`. Apply Zlt_plus_swap.
+    Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool (rho a) `(rho a0)-z`).
+    Intros. Unfold Zminus. Rewrite Zplus_assoc_l. Exact (Zgt_is_le_bool `(rho a)+z` (rho a0)).
+    Intros. Apply iff_trans with b:=`(rho a) <= (rho a0)+z0-z`. Apply Zle_plus_swap.
+    Unfold 1 Zminus. Rewrite Zplus_assoc_r. Unfold Zminus. Apply Zle_is_le_bool.
+    Intros. Apply iff_trans with b:=`(rho a0)+z0 <= (rho a)+z`. Apply Zge_iff_le.
+    Apply iff_trans with b:=`(rho a0) <= (rho a)+z-z0`. Apply Zle_plus_swap.
+    Unfold 1 Zminus. Rewrite Zplus_assoc_r. Unfold Zminus. Apply Zle_is_le_bool.
+    Intros. Apply iff_trans with b:=`(rho a) < (rho a0)+z0-z`. Apply Zlt_plus_swap.
+    Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold 1 Zminus. Rewrite Zplus_assoc_r.
+    Exact (Zlt_is_le_bool (rho a) `(rho a0)+(z0+ -z)`).
+    Intros. Apply iff_trans with b:=`(rho a0)+z0 < (rho a)+z`. Apply Zgt_iff_lt.
+    Apply iff_trans with b:=`(rho a0) < (rho a)+z-z0`. Apply Zlt_plus_swap.
+    Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold 1 Zminus. Rewrite Zplus_assoc_r.
+    Exact (Zlt_is_le_bool (rho a0) `(rho a)+(z+ -z0)`).
+    Intros. Rewrite Zero_right. Split; Intro; Assumption.
+    Split; Intro; Assumption.
+    Split; Intro; Apply sym_eq; Assumption.
+    Intros. Unfold Zminus. Rewrite Zplus_assoc_l. Exact (Zeq_plus_swap (rho a) `(rho a0)+z0` z).
+    Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z <= (rho a)`. Rewrite Zero_left.
+    Split; Intro; Assumption.
+    Apply iff_trans with b:=`0 <= (rho a)-z`. Apply Zle_plus_swap.
+    Unfold Zminus. Apply Zle_is_le_bool.
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zge_is_le_bool.
+    Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z < (rho a)`. Rewrite Zero_left.
+    Split; Intro; Assumption.
+    Apply iff_trans with b:=`0 < (rho a)-z`. Apply Zlt_plus_swap.
+    Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool `0` `(rho a)-z`).
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zgt_is_le_bool.
+    Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z <= (rho a)+z0`. Rewrite Zero_left.
+    Split; Intro; Assumption.
+    Apply iff_trans with b:=`0 <= (rho a)+z0-z`. Apply Zle_plus_swap.
+    Unfold 2 Zminus. Rewrite Zplus_assoc_l. Exact (Zle_is_le_bool `0` `(rho a)+z0-z`).
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a)+z0 <= z`.
+    Apply Zge_iff_le.
+    Apply iff_trans with b:=`(rho a) <= z-z0`. Apply Zle_plus_swap.
+    Apply Zle_is_le_bool.
+    Rewrite Zrho_zero. Intros. Apply iff_trans with `0+z < (rho a)+z0`. Rewrite Zero_left.
+    Split; Intro; Assumption.
+    Apply iff_trans with b:=`0 < (rho a)+z0-z`. Apply Zlt_plus_swap.
+    Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold Zminus. Rewrite Zplus_assoc_l.
+    Exact (Zlt_is_le_bool `0` `(rho a)+z0+ -z`).
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a)+z0 < z`.
+    Apply Zgt_iff_lt.
+    Apply iff_trans with b:=`(rho a) < z-z0`. Apply Zlt_plus_swap.
+    Apply Zlt_is_le_bool.
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Split; Intro; Apply sym_eq; Assumption.
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with `(rho a)+z0 = z`.
+    Split; Intro; Apply sym_eq; Assumption.
+    Apply Zeq_plus_swap.
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zle_is_le_bool.
+    Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z <= (rho a)`. Rewrite Zero_left.
+    Apply Zge_iff_le.
+    Apply iff_trans with b:=`0 <= (rho a)-z`. Apply Zle_plus_swap.
+    Exact (Zle_is_le_bool `0` `(rho a)-z`).
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zlt_is_le_bool.
+    Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z < (rho a)`. Rewrite Zero_left.
+    Apply Zgt_iff_lt.
+    Apply iff_trans with b:=`0 < (rho a)-z`. Apply Zlt_plus_swap.
+    Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool `0` `(rho a)-z`).
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a) <= z0-z`.
+    Apply Zle_plus_swap.
+    Apply Zle_is_le_bool. 
+    Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z0 <= (rho a)+z`. Rewrite Zero_left.
+    Apply Zge_iff_le.
+    Apply iff_trans with b:=`0 <= (rho a)+z-z0`. Apply Zle_plus_swap.
+    Unfold 2 Zminus. Rewrite Zplus_assoc_l. Exact (Zle_is_le_bool `0` `(rho a)+z-z0`).
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a) < z0-z`.
+    Apply Zlt_plus_swap.
+    Apply Zlt_is_le_bool.
+    Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z0 < (rho a)+z`. Rewrite Zero_left.
+    Apply Zgt_iff_lt.
+    Apply iff_trans with b:=`0 < (rho a)+z-z0`. Apply Zlt_plus_swap.
+    Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold Zminus. Rewrite Zplus_assoc_l.
+    Exact (Zlt_is_le_bool `0` `(rho a)+z+ -z0`).
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Split; Intro; Assumption.
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zeq_plus_swap.
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z <= z0`.
+    Rewrite Zero_left. Split; Intro; Assumption.
+    Apply iff_trans with b:=`0 <= z0-z`. Apply Zle_plus_swap.
+    Apply Zle_is_le_bool.
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z < z0`.
+    Rewrite Zero_left. Split; Intro; Assumption.
+    Apply iff_trans with b:=`0 < z0-z`. Apply Zlt_plus_swap.
+    Apply Zlt_is_le_bool.
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z0 <= z`.
+    Rewrite Zero_left. Apply Zge_iff_le.
+    Apply iff_trans with b:=`0 <= z-z0`. Apply Zle_plus_swap.
+    Apply Zle_is_le_bool.
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z0 < z`.
+    Rewrite Zero_left. Apply Zgt_iff_lt.
+    Apply iff_trans with b:=`0 < z-z0`. Apply Zlt_plus_swap.
+    Apply Zlt_is_le_bool.
+    Rewrite Zrho_zero. Intros. Rewrite Zero_left. Split. Intro. Rewrite H. Apply Zminus_n_n.
+    Intro. Rewrite <- (Zero_left z0). Rewrite H. Unfold Zminus. Rewrite Zplus_assoc_r.
+    Rewrite Zplus_inverse_l. Rewrite Zero_right. Reflexivity.
+    Intros. Elim H. Intros. Elim H0. Intros. Split. Intro. Elim H5. Intros. Split. Apply H1.
+    Assumption.
+    Apply H3. Assumption.
+    Intro. Elim H5. Intros. Split. Apply H2. Assumption.
+    Apply H4. Assumption.
+    Intros. Elim H. Intros. Elim H0. Intros. Split. Intro. Elim H5. Intro. Left . Apply H1.
+    Assumption.
+    Intro. Right . Apply H3. Assumption.
+    Intro. Elim H5. Intro. Left . Apply H2. Assumption.
+    Intro. Right . Apply H4. Assumption.
+    Intros. Elim H. Intros. Elim H0. Intros. Split. Intros. Apply H3. Apply H5. Apply H2.
+    Assumption.
+    Intros. Apply H4. Apply H5. Apply H1. Assumption.
+    Unfold not. Intros. Elim H. Intros. Split. Intros. Apply H2. Apply H1. Assumption.
+    Intros. Apply H2. Apply H0. Assumption.
+    Intros. Fold (ZCG_eval rho (ZCGtranslate z))<->(ZCG_eval rho (ZCGtranslate z0)). Split.
+    Intro. Apply iff_trans with b:=(ZCGeval z). Apply iff_sym. Assumption.
+    Apply iff_trans with b:=(ZCGeval z0). Assumption.
+    Assumption.
+    Intro. Apply iff_trans with b:=(ZCG_eval rho (ZCGtranslate z)). Assumption.
+    Apply iff_trans with b:=(ZCG_eval rho (ZCGtranslate z0)). Assumption.
+    Apply iff_sym. Assumption.
+  Qed.
+
+End ZCGevalDef.
+
+Definition ZCG_solve 
+ := [f:ZCGForm] (CG_solve Z ZERO Zplus Zopp Zle_bool `1` (ZCGtranslate f)).
+
+Theorem ZCG_solve_correct :
+      	(f:ZCGForm) (ZCG_solve f)=true ->
+          {rho:ad->Z | (ZCGeval rho f) /\ (rho ad_z)=`0`}.
+Proof.
+  Intros.
+  Elim (CG_solve_correct_anchored Z ZERO Zplus Zopp Zle_bool Zero_right
+       Zero_left Zplus_assoc_r Zplus_inverse_r Zle_bool_refl
+       Zle_bool_antisym Zle_bool_trans Zle_bool_total
+       Zle_bool_plus_mono `1` Zone_pos Zone_min_pos ad_z `0` ? H).
+  Intros rho H0. Split with rho. Elim H0. Intros. Split.
+  Apply (proj2 ? ? (ZCGeval_correct rho H2 f)). Assumption.
+  Assumption.
+Qed.
+
+Theorem ZCG_solve_complete
+   : (f:ZCGForm) (rho:ad->Z) 
+     (ZCGeval rho f) -> (rho ad_z)=`0` -> (ZCG_solve f)=true.
+Proof.
+  Intros. Unfold ZCG_solve.
+  Apply (CG_solve_complete Z ZERO Zplus Zopp Zle_bool Zero_right
+        Zero_left Zplus_assoc_r Zplus_inverse_r Zle_bool_refl
+        Zle_bool_antisym Zle_bool_trans Zle_bool_total
+        Zle_bool_plus_mono `1` Zone_pos Zone_min_pos (ZCGtranslate f)
+        rho).
+  Apply (proj1 ? ? (ZCGeval_correct rho H0 f)). Assumption.
+Qed.
+
+Definition ZCG_prove 
+  := [f:ZCGForm] (CG_prove Z ZERO Zplus Zopp Zle_bool `1` (ZCGtranslate f)).
+
+Theorem ZCG_prove_correct 
+  : (f:ZCGForm) (ZCG_prove f)=true ->
+    (rho:ad->Z) (rho ad_z)=`0` -> (ZCGeval rho f).
+Proof.
+  Intros. Apply (proj2 ? ? (ZCGeval_correct rho H0 f)).
+  Exact (CG_prove_correct Z ZERO Zplus Zopp Zle_bool Zero_right Zero_left
+        Zplus_assoc_r Zplus_inverse_r Zle_bool_refl Zle_bool_antisym
+        Zle_bool_trans Zle_bool_total Zle_bool_plus_mono `1` Zone_pos
+        Zone_min_pos ? H rho).
+Qed.
+
+Theorem ZCG_prove_complete 
+  : (f:ZCGForm)
+    ((rho:ad->Z) (rho ad_z)=`0` -> (ZCGeval rho f)) -> (ZCG_prove f)=true.
+Proof.
+  Intros. Unfold ZCG_prove.
+  Apply (CG_prove_complete_anchored Z ZERO Zplus Zopp Zle_bool Zero_right
+        Zero_left Zplus_assoc_r Zplus_inverse_r Zle_bool_refl
+        Zle_bool_antisym Zle_bool_trans Zle_bool_total
+        Zle_bool_plus_mono `1` Zone_pos Zone_min_pos (ZCGtranslate f)
+        ad_z `0`).
+  Intros. Exact (proj1 ? ? (ZCGeval_correct rho H0 f) (H rho H0)).
+Qed.
+
+(*i Tests:
+
+  Definition v := [n:Z] Cases n of
+                            (POS p) => (ad_x p)
+			  | _ => ad_z
+			end.
+
+  Lemma test1 : (x,y:Z) `x<=y` -> `x<=y+1`.
+  Proof.
+    Intros.
+    Cut (rho:ad->Z) (rho ad_z)=`0` ->
+          (ZCGeval rho (ZCGimp (ZCGle (v`1`) (v`2`)) (ZCGlep (v`1`) (v`2`) `1`))).
+    Intro.
+    Exact (H0 [a:ad]Case (ad_eq a (v`1`)) of x
+                    Case (ad_eq a (v`2`)) of y
+                    `0` end end
+              (refl_equal ? ?)
+              H).
+
+    Intros. Apply ZCG_prove_correct. Compute. Reflexivity.
+    Assumption.
+   Qed.
+
+  Lemma test2 : (x,y:Z) ~(`x<=y` -> `x<=y-1`).
+  Proof.
+    Intros.
+    Cut (rho:ad->Z) (rho ad_z)=`0` ->
+          (ZCGeval rho (ZCGnot (ZCGimp (ZCGle (v `1`) (v `2`)) (ZCGlep (v `1`) (v `2`) `-1`)))).
+    Intro.
+    Exact (H [a:ad] Case (ad_eq a (v `1`)) of x
+                    Case (ad_eq a (v `2`)) of y
+                    `0` end end (refl_equal ? ?)).
+    Intros. Apply ZCG_prove_correct. Compute. (* fails: remains to prove false=true; indeed,
+    test2 is not provable. *)
+    <Your Tactic Text here>
+    <Your Tactic Text here>
+
+i*)