(*
 *  Seplog is an implementation of separation logic (an extension of Hoare
 *  logic by John C. Reynolds, Peter W. O'Hearn, and colleagues) in the
 *  Coq proof assistant (version 8, http://coq.inria.fr) together with a
 *  sample verification of the heap manager of the Topsy operating system
 *  (version 2, http://www.topsy.net). More information is available at
 *  http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/seplog.
 *
 *  Copyright (c) 2005, 2006 Reynald Affeldt and Nicolas Marti
 *
 *  This program is free software; you can redistribute it and/or modify
 *  it under the terms of the GNU General Public License as published by
 *  the Free Software Foundation; either version 2 of the License, or
 *  (at your option) any later version.
 *
 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *  GNU General Public License for more details.
 *
 *  You should have received a copy of the GNU General Public License
 *  along with this program; if not, write to the Free Software
 *  Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
 *)


Load seplog_header.



(***********************************)

Fixpoint inb (A: Set) (B: A -> A -> bool) (l: list A) (a: A) {struct l}: bool :=
	match l with
		nil => false
		| hd::tl => if (B a hd) then true else (inb A B tl a)
	end.
Implicit Arguments inb.

Fixpoint add_elt_list (A: Set) (B: A -> A -> bool) (l: list A) (a: A) {struct l}: list A :=
      match l with 
         nil => a::nil
         | hd::tl => if (B hd a) then l else hd::(add_elt_list A B tl a)
      end.
Implicit Arguments add_elt_list.

Fixpoint app_list (A: Set) (B: A -> A -> bool) (l1 l2: list A){struct l1}: list A :=
      match l1 with 
         nil => l2
         | hd::tl => app_list A B tl (add_elt_list B l2 hd)
      end.
Implicit Arguments app_list.

(***********************************)
Notation "e << e'" := (neg_b (ge_b e e')) (at level 78) : sep_scope.
Notation "e <<= e'" := (neg_b (gt_b e e')) (at level 78) : sep_scope.
Notation "! e" := (neg_b e) (at level 78) : sep_scope.
Notation " s '|b=' b " := (eval_b b s = true) (right associativity, at level 80).
Notation " s '|b!=' b " := (eval_b b s = false) (right associativity, at level 80).
Notation " b1 =b> b2 " := ((!b1) ||| b2) (right associativity, at level 80).
(***********************************)

Definition constraint := expr.

Definition andlist  := list constraint.

Definition orlist := list andlist.


Definition constraint_semantic (c: constraint) : expr_b := (nat_e 0) >>= c.

Fixpoint andlist_semantic (l: andlist) : expr_b:=
 match l with
   nil => true_b
   | hd::tl => (constraint_semantic hd) &&& (andlist_semantic tl)
 end.
Fixpoint orlist_semantic (l: orlist) : expr_b:=
 match l with
   nil => ! true_b
   | hd::tl => (andlist_semantic hd) ||| (orlist_semantic tl)
 end.


(***********************************)


Lemma expr_b_neg_involutive: forall a,
 (forall s, eval_b (!! a) s = eval_b a s).
intros.
simpl.
rewrite negb_elim.
auto.
Qed.


Lemma eval_b_destruct: forall b s,
 eval_b b s = true \/ eval_b b s = false.
intros.
destruct eval_b; auto.
Qed.

Lemma expr_b_eq: forall b1 b2 s,
  ((s |b= b1) <-> (s |b= b2)) -> (eval_b b1 s = eval_b b2 s).
intros.
inversion_clear H.
generalize (eval_b_destruct b1 s); intro X; inversion_clear X.
generalize (eval_b_destruct b2 s); intro X; inversion_clear X.
rewrite H; rewrite H2; auto.
intuition.
rewrite H3 in H2; discriminate.
generalize (eval_b_destruct b2 s); intro X; inversion_clear X.
intuition.
rewrite H3 in H; discriminate.
rewrite H; rewrite H2; auto.
Qed.

Lemma expr_b_eq': forall b1 b2 s,
  (eval_b b1 s = eval_b b2 s) -> ((s |b= b1) <-> (s |b= b2)).
intros.
split; intros.
rewrite H in H0.
auto.
rewrite <- H in H0.
auto.
Qed.

Definition option_app (A: Set) (l1 l2: option (list A)) : option (list A) :=
  match l1 with
     None => None
     | Some l1' =>   match l2 with
                                    None => None
                                    | Some l2' => Some (l1' ++ l2')
                                end
  end.
Implicit Arguments option_app.

(***********************************)

Definition dnf_expr_b1 (a:expr_b) : expr_b :=
   match a with
      | e1 == e2 => (e2 >>= e1) &&& (e1 >>= e2)
      | e1 >> e2 =>  e1 >>=  (e2 +e (nat_e 1))
      | _ => a
   end.


Definition dnf_expr_b2 (a:expr_b) : expr_b :=
   match a with
      |  a1 &&& (a2 ||| a3) => (a1 &&& a2) ||| (a1 &&& a3)
      | (a2 ||| a3) &&& a1 => (a1 &&&  a2) |||  (a1  &&&  a3)
      | _ => dnf_expr_b1 a
   end.


Lemma dnf_expr_b2_correct: forall a,
 (forall s, eval_b a s = eval_b (dnf_expr_b2 a) s).
destruct a; (intros; apply expr_b_eq; split; (intros; try Omega_exprb)).
destruct a1; destruct a2; try Omega_exprb.
destruct a1; destruct a2; try Omega_exprb.
Qed.


Definition dnf_expr_b3 (a:expr_b) : expr_b :=
   match a with
      | ! (! a') => (a')
      | ! (a1 &&& a2) => (!a1) ||| (!a2)
      | ! (a1 ||| a2) => (! a1) &&& (! a2)
      | ! (e1 >> e2) => (e2 >>= e1)
      | ! (e1 >>= e2) => (e2 >> e1)
      | ! (e1 == e2) => (e2 >> e1) ||| (e1 >> e2)
      | (e1 =/= e2) => (e2 >> e1) ||| (e1 >> e2)
      | _ => dnf_expr_b2 a
   end.


Lemma dnf_expr_b3_correct: forall a,
 (forall s, eval_b a s = eval_b (dnf_expr_b3 a) s).
destruct a; (intros; apply expr_b_eq; split; (intros; try Omega_exprb)).
destruct a; try Omega_exprb.
rewrite expr_b_neg_involutive in H; auto.
simpl.
simpl in H.
destruct (eval_b a1 s); destruct (eval_b a2 s); (auto || (simpl in H; inversion H)).
destruct a; try Omega_exprb.
destruct a1; destruct a2; try Omega_exprb.
destruct a1; destruct a2; try Omega_exprb.
Qed.

Fixpoint dnf_expr_rec (a: expr_b) : expr_b :=
  match a with
      | a1 &&& a2 => dnf_expr_b2 ((dnf_expr_rec a1) &&& (dnf_expr_rec a2))
      | a1 ||| a2 => (dnf_expr_rec a1) ||| (dnf_expr_rec a2)
      | _ =>  dnf_expr_b3 a
  end.


Lemma dnf_expr_rec_correct: forall a,
 (forall s, eval_b a s = eval_b (dnf_expr_rec a) s).
induction a; (intros; apply expr_b_eq; split; (intros; try Omega_exprb)).
(* ! *)
rewrite dnf_expr_b3_correct in H.
intuition.
rewrite dnf_expr_b3_correct.
intuition.
(* &&& *)
cut (s |b= (dnf_expr_b2 ((dnf_expr_rec a1) &&& (dnf_expr_rec a2)))).
intuition.
rewrite <- dnf_expr_b2_correct.
simpl in H.
simpl eval_b.
rewrite <- IHa1; rewrite <- IHa2; auto.
assert (s |b= (dnf_expr_b2 ((dnf_expr_rec a1) &&& (dnf_expr_rec a2)))).
intuition.
rewrite <- dnf_expr_b2_correct in H0.
simpl eval_b in H0.
simpl.
rewrite IHa1; rewrite IHa2; auto.
(* ||| *)
cut (s |b= ((dnf_expr_rec a1) ||| (dnf_expr_rec a2))).
intuition.
simpl in H.
simpl eval_b.
rewrite <- IHa1; rewrite <- IHa2; auto.
assert (s |b= (((dnf_expr_rec a1) ||| (dnf_expr_rec a2)))).
intuition.
simpl eval_b in H0.
simpl.
rewrite IHa1; rewrite IHa2; auto.
Qed.

Fixpoint expr_b_size (a: expr_b) : nat :=
  match a with 
    true_b => 1
    | eq_b e1 e2 => 1
    | neq_b e1 e2 => 1
    | ge_b e1 e2 => 1
    | gt_b e1 e2 => 1
    | and_b e1 e2 => 1 + ((expr_b_size e1) * (expr_b_size e2))
    | or_b e1 e2 => 1 + ((expr_b_size e1) + (expr_b_size e2))
    | neg_b e => 1 + (expr_b_size e)
  end.

Fixpoint dnf_expr_fp (a: expr_b) (size: nat) {struct size}: expr_b :=
   match size with
     0 => dnf_expr_rec a
     | S n => dnf_expr_fp (dnf_expr_rec a) n
   end.


Lemma dnf_expr_fp_correct: forall n a,
 (forall s, eval_b a s = eval_b (dnf_expr_fp a n) s).
induction n.
simpl; intros.
apply dnf_expr_rec_correct.
simpl; intros.
rewrite <- (IHn (dnf_expr_rec a) s).
apply dnf_expr_rec_correct.
Qed.

Definition dnf_expr_b (a:expr_b) : expr_b := dnf_expr_fp a (expr_b_size a).


Lemma dnf_expr_b_correct: forall a,
 (forall s, eval_b a s = eval_b (dnf_expr_b a) s).
intros.
unfold dnf_expr_b.
apply dnf_expr_fp_correct.
Qed.

Definition dnf_expr_b2constraint (b: expr_b) : option constraint :=
    match b with
       e1 >>= e2 => Some (e2 -e e1)
       | _ => None
    end.


Lemma dnf_expr_b2constraint_correct: forall b b',
  dnf_expr_b2constraint b = Some b' ->
 (forall s, eval_b b s = eval_b (constraint_semantic b') s).
destruct b; (simpl; intros; try inversion H).
simpl.
generalize (Zge_cases (eval e s) (eval e0 s)); intros.
generalize (Zge_cases 0 (eval e0 s - eval e s)); intros.

destruct (Zge_bool (eval e s) (eval e0 s)); destruct (Zge_bool 0 (eval e0 s - eval e s)); auto.
assert (0 >= eval e0 s - eval e s)%Z.
intuition.
contradiction.
assert (0 < eval e0 s - eval e s)%Z.
intuition.
contradiction.
Qed.

Fixpoint dnf_expr_b2andlist (b: expr_b) : option andlist :=
   match b with
      b1 &&& b2 => option_app (dnf_expr_b2andlist b1) (dnf_expr_b2andlist b2)
      | _ => match (dnf_expr_b2constraint b) with
                     None => None
                     | Some b' => Some (b'::nil)
                 end
   end.

Lemma dnf_expr_b2andlist_notempty: forall b b',
 dnf_expr_b2andlist b = Some b' -> 
 b' <> nil.
induction b; intros; simpl in H; try discriminate.
injection H; intros; subst b'; clear H.
red; intros; discriminate.
destruct (dnf_expr_b2andlist b1); destruct (dnf_expr_b2andlist b2); simpl in H; try discriminate.
injection H; intros; subst b'; clear H.
generalize (IHb1 a); intros.
intuition.
destruct a; intuition; discriminate.
Qed.

Lemma andlist_semantic_app: forall l1 l2 s,
 eval_b (andlist_semantic (l1 ++ l2)) s =
 eval_b ((andlist_semantic l1) &&& (andlist_semantic l2)) s.
induction l1.
intuition.
intros.
simpl andlist_semantic.
apply expr_b_eq; split; intros; try Omega_exprb.
assert (A1: (s |b= constraint_semantic a) /\ s |b= andlist_semantic (l1 ++ l2)).
split; Omega_exprb.
inversion_clear A1.
rewrite IHl1 in H1.
Omega_exprb.
cut ((s |b= constraint_semantic a) /\ s |b= andlist_semantic (l1 ++ l2)).
intros.
inversion_clear H0.
Omega_exprb.
split; try Omega_exprb.
rewrite IHl1.
Omega_exprb.
Qed.


Lemma dnf_expr_bool2andlist_correct: forall b b',
 dnf_expr_b2andlist b = Some b' ->
 (forall s, eval_b b s = eval_b (andlist_semantic b') s).
induction b; intros; simpl in H; try discriminate.
injection H; intros; subst b'.
simpl andlist_semantic.
cutrewrite (eval_b (constraint_semantic (e0 -e e) &&& true_b) s = eval_b (constraint_semantic (e0 -e e)) s).
rewrite (dnf_expr_b2constraint_correct (e >>= e0) (e0 -e e)).
auto.
auto.
apply expr_b_eq; split; intros; Omega_exprb.
destruct (dnf_expr_b2andlist b1); destruct (dnf_expr_b2andlist b2); simpl in H; try discriminate.
injection H; intros; subst b'; clear H.
rewrite andlist_semantic_app.
simpl.
rewrite (IHb2  a0); auto.
rewrite (IHb1 a); auto.
Qed.


Fixpoint dnf_expr_b2orlist (b: expr_b) : option orlist :=
   match b with
      b1 ||| b2 => option_app (dnf_expr_b2orlist b1) (dnf_expr_b2orlist b2)
      | _ => match (dnf_expr_b2andlist b) with
                     None => None
                     | Some b' => Some (b'::nil)
                 end
   end.

Lemma dnf_expr_b2orlist_notempty: forall b b',
 dnf_expr_b2orlist b = Some b' -> 
 b' <> nil.
induction b; intros; simpl in H; try discriminate.
injection H; intros; subst b'; clear H.
red; intros; discriminate.
generalize (dnf_expr_b2andlist_notempty b1); generalize (dnf_expr_b2andlist_notempty b2); intros.
destruct (dnf_expr_b2andlist b1); destruct (dnf_expr_b2andlist b2); simpl in H; try discriminate.
injection H; intros; subst b'; clear H.
generalize (H1 a); intros.
intuition.
destruct a; intuition; discriminate.
destruct (dnf_expr_b2orlist b1); destruct (dnf_expr_b2orlist b2); simpl in H; try discriminate.
injection H; intros; subst b'; clear H.
generalize (IHb1 o); intros.
intuition.
destruct o; intuition; discriminate.
Qed.

Lemma orlist_semantic_app: forall l1 l2 s,
 l1 <> nil ->
 l2 <> nil ->
 eval_b (orlist_semantic (l1 ++ l2)) s =
 eval_b ((orlist_semantic l1) ||| (orlist_semantic l2)) s.
induction l1.
intuition.
intros.
destruct l1; simpl orlist_semantic.
destruct l2; try tauto; simpl andlist_semantic; simpl orlist_semantic.
apply expr_b_eq; split; intros; Omega_exprb.
destruct l2; try tauto; simpl andlist_semantic; simpl orlist_semantic.
simpl orlist_semantic in IHl1.
assert (a0::l1 <> nil); [red;  intro; discriminate | idtac].
generalize (IHl1 (a1::l2) s H1 H0); intros.
generalize (expr_b_eq' _ _ _ H2); clear H2; intros.
inversion_clear H2.
eapply expr_b_eq; split; intros.
clear H4; Eval_b_hyp_clean; inversion_clear H4; Eval_b_goal ; intuition.
assert (A1 : s |b= andlist_semantic a0 ||| orlist_semantic (l1 ++ a1 :: l2)); [Omega_exprb | generalize (H3 A1); clear H3 A1; intros; Omega_exprb].
clear H3.
simpl orlist_semantic in H4.
Eval_b_hyp_clean; Eval_b_goal.
assert ( expr_b_sem (andlist_semantic a) s \/ (expr_b_sem (andlist_semantic a0) s \/ (expr_b_sem (orlist_semantic l1) s) \/ expr_b_sem (andlist_semantic a1) s \/ expr_b_sem (orlist_semantic l2) s) ).
intuition.
inversion_clear H2; [intuition |
assert (A1: s |b= (andlist_semantic a0 ||| orlist_semantic l1) ||| (andlist_semantic a1 ||| orlist_semantic l2)); [Omega_exprb | generalize (H4 A1); clear H4 A1; intros; Omega_exprb]
].
Qed.

Lemma dnf_expr_b2orlist_correct: forall b b',
 dnf_expr_b2orlist b = Some b' ->
 (forall s, eval_b b s = eval_b (orlist_semantic b') s).
induction b; intros; simpl in H; try discriminate.
(*>>=*)
injection H; intros; subst b'.
simpl orlist_semantic.
apply expr_b_eq; split; intros; Eval_b_hyp_clean; Eval_b_goal; intuition.
(* /\ *)
generalize (dnf_expr_b2andlist_notempty b1); generalize (dnf_expr_b2andlist_notempty b2); intros.
generalize (dnf_expr_bool2andlist_correct b1); generalize (dnf_expr_bool2andlist_correct b2); intros.
destruct (dnf_expr_b2andlist b1); destruct (dnf_expr_b2andlist b2); simpl in H; try discriminate.
injection H; intros; subst b'; clear H.
simpl orlist_semantic.
apply expr_b_eq; split; intros.
cut (s |b= andlist_semantic (a ++ a0)); [intros; Eval_b_hyp_clean; Eval_b_goal; intuition | idtac].
rewrite andlist_semantic_app.
simpl; simpl in H; rewrite <- (H2 a0); [rewrite <- (H3 a); auto | auto].
assert (s |b= andlist_semantic (a ++ a0)); [intros; Eval_b_hyp_clean; Eval_b_goal; intuition | idtac].
rewrite andlist_semantic_app in H4.
simpl; simpl in H4; rewrite <- (H2 a0) in H4; [rewrite <- (H3 a) in H4; auto | auto].
(* \/ *)
generalize (dnf_expr_b2orlist_notempty b1); generalize (dnf_expr_b2orlist_notempty b2); intros.
destruct (dnf_expr_b2orlist b1); destruct (dnf_expr_b2orlist b2); simpl in H; try discriminate.
injection H; intros; subst b'; clear H.
rewrite orlist_semantic_app; [idtac | apply H1; auto | apply H0; auto].
simpl; rewrite (IHb1 o); auto; rewrite (IHb2 o0); auto.
Qed.

Definition expr_b2constraints (b: expr_b) : option orlist :=
      dnf_expr_b2orlist (dnf_expr_b b).

Lemma expr_b2constraints_correct: forall b x,
  expr_b2constraints b = Some x ->
  (forall s, eval_b b s = eval_b (orlist_semantic x) s).
intros.
unfold expr_b2constraints in H.
rewrite (dnf_expr_b_correct b s).
rewrite (dnf_expr_b2orlist_correct _ _ H).
auto.
Qed.

(***********************************)

Fixpoint expr_compute (e: expr) : option Z :=
   match e with
      var_e x => None
      | int_e x => Some x
      | e1 +e e2 => match (expr_compute e1) with
                                               None => None
                                               | Some e1' => match (expr_compute e2) with
                                                                            None => None
                                                                            | Some e2' => Some (e1' + e2')%Z
                                                                         end
                                           end
      | e1 -e e2 => match (expr_compute e1) with
                                               None => None
                                               | Some e1' => match (expr_compute e2) with
                                                                            None => None
                                                                            | Some e2' => Some (e1' - e2')%Z
                                                                         end
                                           end
      | e1 *e e2 => match (expr_compute e1) with
                                               None => match (expr_compute e2) with
                                                                            None => None
                                                                            | Some e2' => if (Zeq_bool e2' 0%Z) then (Some 0%Z) else None
                                                                         end
                                               | Some e1' => if (Zeq_bool e1' 0%Z) then (Some 0%Z) else 
                                                                         match (expr_compute e2) with
                                                                            None => None
                                                                            | Some e2' => Some (e1' * e2')%Z
                                                                         end
                                           end
     | _ => None
   end.

Lemma expr_compute_correct: forall e z,
 expr_compute e = Some z ->
 (forall s, eval e s = z).
induction e; intros; simpl in H; try discriminate; simpl.
injection H; intros; auto.
destruct (expr_compute e1); destruct (expr_compute e2); simpl in H; try discriminate; injection H; intros; subst z.
rewrite (IHe1 z0); auto; rewrite (IHe2 z1); auto.
destruct (expr_compute e1); destruct (expr_compute e2); simpl in H; try discriminate; injection H; intros; subst z.
rewrite (IHe1 z0); auto; rewrite (IHe2 z1); auto.
destruct (expr_compute e1); destruct (expr_compute e2); simpl in H; try discriminate.
generalize (Zeq_bool_classic z0 0); intro X; inversion_clear X; rewrite H0 in H; injection H; intros; subst z.
rewrite (IHe1 z0); auto; rewrite (IHe2 z1); auto.
rewrite (Zeq_bool_true _ _ H0); ring.
rewrite (IHe1 z0); auto; rewrite (IHe2 z1); auto.
generalize (Zeq_bool_classic z0 0); intro X; inversion_clear X; rewrite H0 in H; try ((injection H; intros; subst z) || inversion H).
rewrite (IHe1 z0); auto.
rewrite (Zeq_bool_true _ _ H0); ring.
generalize (Zeq_bool_classic z0 0); intro X; inversion_clear X; rewrite H0 in H; try ((injection H; intros; subst z) || inversion H).
rewrite (IHe2 z0); auto.
rewrite (Zeq_bool_true _ _ H0); ring.
Qed.

Fixpoint expr_var_fact' (e: expr) (v: nat) {struct e}: (expr * expr) :=
   match e with
      var_e x => if (beq_nat x v) then ((nat_e 1),(nat_e 0)) else ((nat_e 0),(var_e x))
      | int_e x => ((nat_e 0),(int_e x))
      | e1 +e e2 => match (expr_var_fact' e1 v) with
                            | (e11,e12) => match (expr_var_fact' e2 v) with
                                            | (e21,e22) => ((e11 +e e21),(e12 +e e22))
                          		   end
                          end
      | e1 -e e2 => match (expr_var_fact' e1 v) with
                                               | (e11,e12) => match (expr_var_fact' e2 v) with
                                                                            | (e21,e22) => ((e11 -e e21),(e12 -e e22))
                                                                         end
                                           end
      | e1 *e e2 => match (expr_var_fact' e1 v) with
                           | (e11,e12) => match (expr_var_fact' e2 v) with
                                | (e21,e22) => ((((e12 *e e21) +e (e11 *e e22)) +e ((var_e v) *e (e11 *e e21))),(e12 *e e22))
                                          end
                           end
      | e1 /e e2 => ((nat_e 0),(e1 /e e2))
   end.

Lemma expr_var_fact'_correct: forall e v e1 e2,
  expr_var_fact' e v = (e1,e2) ->
     (forall s, eval e s = eval (((var_e v) *e e1) +e e2) s).
induction e; simpl; intros.
generalize (beq_nat_classic v v0); intro X; inversion_clear X.
rewrite H0 in H.
injection H; intros; subst e1 e2.
simpl.
rewrite (beq_nat_true _ _ H0); OmegaZ.
rewrite H0 in H.
injection H; intros; subst e1 e2.
Simpl_eval; OmegaZ.
injection H; intros; subst e1 e2.
Simpl_eval; OmegaZ.
generalize (IHe1 v); intros; clear IHe1.
generalize (IHe2 v); intros; clear IHe2.
destruct (expr_var_fact' e1 v); destruct (expr_var_fact' e2 v); injection H; intros; subst e0 e3.
rewrite (H0 e e4); auto; rewrite (H1 e5 e6); auto. 
simpl; ring.
generalize (IHe1 v); intros; clear IHe1.
generalize (IHe2 v); intros; clear IHe2.
destruct (expr_var_fact' e1 v); destruct (expr_var_fact' e2 v); injection H; intros; subst e0 e3.
rewrite (H0 e e4); auto; rewrite (H1 e5 e6); auto. 
simpl; ring.
generalize (IHe1 v); intros; clear IHe1.
generalize (IHe2 v); intros; clear IHe2.
destruct (expr_var_fact' e1 v); destruct (expr_var_fact' e2 v); injection H; intros; subst e0 e3.
rewrite (H0 e e4); auto; rewrite (H1 e5 e6); auto. 
simpl; ring.
injection H; intros; subst e0 e3.
simpl; ring.
Qed.


Fixpoint simpl_varlist_constraint (c: constraint) (v: list nat) {struct v}: constraint :=
   match v with
      nil => match (expr_compute c) with
                    None => c
                    | Some val => int_e val
                 end
      | hd::tl => match (expr_var_fact' c hd) with
                           (e1,e2) => match (expr_compute e1) with
                                                   None => (e1 *e (var_e hd)) +e (simpl_varlist_constraint e2 tl)
                                                   | Some val => if (Zeq_bool val 0%Z) then 
                                                                                   (simpl_varlist_constraint e2 tl)
                                                                             else
                                                                                   ((int_e val) *e (var_e hd)) +e (simpl_varlist_constraint e2 tl)
                                               end
                           end
   end.

Lemma simpl_varlist_constraint_destruct: forall c v,
  exists c', simpl_varlist_constraint c v = c'.
  intros.
  exists (simpl_varlist_constraint c v).
  auto.
  Qed.
  

Lemma expr_compute_destruct: forall c,
 ((exists z, expr_compute c = Some z) \/ expr_compute c = None).
intros.
destruct expr_compute.
left; exists z; auto.
right; auto.
Qed.


Lemma expr_num_var_fact'_destruct: forall e v,
 exists e1, exists e2, expr_var_fact' e v = (e1,e2).
intros.
destruct expr_var_fact'.
exists e0; exists e1; auto.
Qed. 

Lemma simpl_varlist_constraint_correct: forall v c c',
 simpl_varlist_constraint c v = c' ->
 (forall s, eval c s = eval c' s).
induction v.
simpl.
intros.
generalize (expr_compute_destruct c); intro X; inversion_clear X.
inversion_clear H0.
rewrite H1 in H.
rewrite <- H.
rewrite (expr_compute_correct _ _ H1).
auto.
rewrite H0 in H.
subst c; auto.
simpl in IHv.
simpl; intros.
generalize (expr_num_var_fact'_destruct c a); intro X; inversion_clear X.
inversion_clear H0.
rewrite H1 in H.
generalize (expr_var_fact'_correct _ _ _ _ H1 s); clear H1; intros.
generalize (expr_compute_destruct x); intro X; inversion_clear X.
inversion_clear H1.
rewrite H2 in H.
generalize (expr_compute_correct _ _ H2 s); intros.
generalize (Zeq_bool_classic x1 0); intro X; inversion_clear X.
rewrite H3 in H.
generalize (IHv _ _ H s); intros.
simpl in H0.
generalize (Zeq_bool_true _ _ H3); intros.
rewrite H5 in H1; rewrite H1 in H0.
rewrite H0.
cutrewrite (store.lookup a s * 0 + eval x0 s = eval x0 s)%Z.
auto.
intuition.
rewrite H3 in H.
rewrite H0; rewrite <- H.
simpl.
rewrite <- H1.
generalize (simpl_varlist_constraint_destruct x0 v); intros. 
inversion_clear H4.
generalize (IHv _ _ H5 s); intros.
rewrite H5.
intuition.
rewrite H1 in H.
subst c'.
simpl.
rewrite H0.
simpl.
generalize (simpl_varlist_constraint_destruct x0 v); intros. 
inversion_clear H.
generalize (IHv _ _ H2 s); intros.
intuition.
Qed.


Definition simpl_constraint (c: constraint) : constraint :=
    simpl_varlist_constraint c (expr_var c).

Lemma simpl_constraint_correct: forall c,
 (forall s, eval c s = eval (simpl_constraint c) s).
intros.
unfold simpl_constraint.
generalize (simpl_varlist_constraint_destruct c (expr_var c)); intros.
inversion_clear H.
rewrite H0.
eapply simpl_varlist_constraint_correct.
apply H0.
Qed.

Definition simpl_constraint_var' (c: constraint) (v: nat): constraint :=
  match (expr_var_fact' c v) with
    (e1,e2) => match (expr_compute (simpl_constraint e1)) with
                 None => (e1 *e (var_e v)) +e e2
                 | Some val => if (Zeq_bool val 0%Z) then 
                   e2
                   else
                     ((int_e val) *e (var_e v)) +e e2
               end
  end.

Lemma simpl_constraint_var'_correct: forall c v,
  (forall s, eval c s = eval (simpl_constraint_var' c v) s).
  intros.
  unfold simpl_constraint_var'.
generalize (expr_var_fact'_correct c v); intros.
destruct (expr_var_fact' c v).
generalize (expr_compute_correct (simpl_constraint e)); intros.
destruct (expr_compute (simpl_constraint e)).
generalize (Zeq_bool_classic z 0); intro X; inversion_clear X.
generalize (Zeq_bool_true _ _ H1); intros; subst z.
rewrite H1.
lapply (H e e0); intros; auto.
rewrite H2; clear H2.
lapply (H0 0%Z); intros; auto.
simpl.
rewrite (simpl_constraint_correct e).
rewrite H2.
ring.
rewrite H1.
lapply (H e e0); intros; auto.
rewrite H2; clear H2.
simpl.
rewrite (simpl_constraint_correct e).
lapply (H0 z); intros; auto.
rewrite H2; ring.
lapply (H e e0); intros; auto.
rewrite H1; simpl; ring.
Qed.

Fixpoint simpl_constraint_var_list' (c: constraint) (v: list nat) {struct v}: constraint :=
  match v with
    nil => simpl_constraint c
    | hd::tl => simpl_constraint_var_list' (simpl_constraint_var' c hd) tl
  end.

Lemma simpl_constraint_var_list'_correct: forall v c,
  (forall s, eval c s = eval (simpl_constraint_var_list' c v) s).
  induction v; simpl.
  intros; rewrite simpl_constraint_correct; auto.
  intros; rewrite <- IHv.
  rewrite (simpl_constraint_var'_correct c a); auto.
Qed.

Definition simpl_constraint' (c: constraint) : constraint :=
  simpl_constraint_var_list' c (expr_var c).

Lemma simpl_constraint'_correct: forall c,
  (forall s, eval c s = eval (simpl_constraint' c) s).
  intros; unfold simpl_constraint'; rewrite <- simpl_constraint_var_list'_correct; auto.
Qed.

Definition expr_var_fact (e: expr) (v: nat): (expr * expr) :=
   match (expr_var_fact' e v) with
      (e1,e2) => (simpl_constraint e1,simpl_constraint e2)
   end.

Lemma expr_var_fact_correct: forall c v e1 e2,
 expr_var_fact c v = (e1,e2) ->
 (forall s, eval c s = eval (((var_e v) *e e1) +e e2) s).
intros.
unfold expr_var_fact in H.
generalize (expr_num_var_fact'_destruct c v); intro X.
inversion_clear X.
inversion_clear H0.
rewrite H1 in H.
generalize (expr_var_fact'_correct _ _ _ _ H1 s); intro.
injection H; intros.
generalize (simpl_constraint_correct x0 s); intros.
generalize (simpl_constraint_correct x s); intros.
rewrite H0.
simpl.
rewrite <- H2; rewrite <- H3.
rewrite <- H4; rewrite <- H5.
auto.
Qed.

Fixpoint simpl_andlist (l: andlist): andlist :=
   match l with
      nil => nil
      | hd::tl => (simpl_constraint' hd )::(simpl_andlist tl )
   end.

Lemma simpl_andlist_correct: forall l ,
 (forall s, eval_b (andlist_semantic l) s =   eval_b (andlist_semantic (simpl_andlist l)) s).
induction l.
auto.
simpl andlist_semantic.
intros.
apply expr_b_eq; split; intros.
assert (
(s |b= constraint_semantic a) /\
(s |b= andlist_semantic l)
).
split; Omega_exprb.
clear H; inversion_clear H0.
cut(
(s |b= constraint_semantic (simpl_constraint' a)) /\
(s |b= andlist_semantic (simpl_andlist l))
).
intros.
inversion_clear H0.
Omega_exprb.
split.
simpl.
rewrite <- simpl_constraint'_correct.
simpl in H; auto.
rewrite <- IHl.
auto.
assert(
(s |b= constraint_semantic (simpl_constraint' a)) /\
(s |b= andlist_semantic (simpl_andlist l))
).
split; Omega_exprb.
clear H; inversion_clear H0.
rewrite <- IHl in H1.
assert (s |b= constraint_semantic a).
simpl in H.
rewrite <- simpl_constraint'_correct in H.
auto.
Omega_exprb.
Qed.

Fixpoint simpl_orlist (l: orlist): orlist :=
   match l with
      nil => nil
      | hd::tl => (simpl_andlist hd)::(simpl_orlist tl)
   end.

Lemma simpl_orlist_correct: forall l ,
 (forall s, eval_b (orlist_semantic l) s =   eval_b (orlist_semantic (simpl_orlist l)) s).
induction l.
auto.
simpl orlist_semantic.
intros.
apply expr_b_eq; split; intros.
assert (
(s |b= andlist_semantic a) \/
(s |b= orlist_semantic l)
).
Eval_b_hyp_clean.
inversion_clear H0.
left; Omega_exprb.
right; Omega_exprb.
inversion_clear H0.
rewrite simpl_andlist_correct in H1; Omega_exprb.
rewrite IHl in H1; Omega_exprb.
assert (
(s |b= andlist_semantic (simpl_andlist a)) \/
(s |b= orlist_semantic (simpl_orlist l))
).
Eval_b_hyp_clean.
inversion_clear H0.
left; Omega_exprb.
right; Omega_exprb.
inversion_clear H0.
rewrite <- simpl_andlist_correct in H1; Omega_exprb.
rewrite <- IHl in H1; Omega_exprb.
Qed.

(***********************************)

Definition elim_var_constraint (c1 c2: constraint) (v: nat) : constraint :=
   match (expr_var_fact c1 v) with
      (e11,e12) => match (expr_var_fact c2 v) with
                                (e21,e22) => match (expr_compute (simpl_constraint e11)) with
                                                         None => c2
                                                         | Some e11' => match (expr_compute (simpl_constraint e21)) with
                                                                                     None => c2
                                                                                     | Some e21' => if (andb (Zlt_bool e11' 0%Z) (Zlt_bool 0%Z e21')) then
                                                                                                                        (((e21 *e e12) -e (e11 *e e22)))
                                                                                                              else (if (andb (Zlt_bool 0%Z e11') (Zlt_bool e21' 0%Z)) then
                                                                                                                        (((e11 *e e22) -e (e21 *e e12))) else c2)
                                                                                   end   
                                                      end   
                            end
   end.


Lemma omega_test_lemma1: forall a1 b1 a2 b2 x,
 (a1 < 0 )%Z ->
 (0 < a2 )%Z ->
 (0 >= x * a1 + b1)%Z ->
 (0 >= x * a2 + b2)%Z ->
 (a1 * b2 >= a2 * b1)%Z.
intros.
assert (b1 <= - (x * a1))%Z.
intuition.
assert ((x * a2) <= - b2)%Z.
intuition.
assert (b1 * a2 <= - (x * a1) * a2)%Z.
intuition.
assert ((x * a2) * -a1 <= - b2 * - a1)%Z.
intuition.
assert (x * a2 * - a1 = -(x * a1) * a2)%Z.
ring.
rewrite H7 in H6; clear H7.
assert (b1 * a2 <= - b2 * - a1)%Z.
intuition.
assert (-b2 * - a1 = a1 * b2)%Z.
ring.
rewrite H8 in H7; clear H8.
cutrewrite (a2 * b1 = b1 * a2)%Z.
intuition.
intuition.
Qed.

Lemma elim_var_constraint_correct: forall c1 c2 v,
   (forall s, (s |b=  (constraint_semantic c1) &&& (constraint_semantic c2)) -> (s |b= (constraint_semantic (elim_var_constraint c1 c2 v)))).
intros.
unfold elim_var_constraint.
generalize (expr_var_fact_correct c1 v); intros.
generalize (expr_var_fact_correct c2 v); intros.
destruct (expr_var_fact c1 v); destruct (expr_var_fact c2 v).
generalize (expr_compute_correct (simpl_constraint e)); intros.
generalize (expr_compute_correct (simpl_constraint e1)); intros.
destruct (expr_compute (simpl_constraint e)); destruct (expr_compute (simpl_constraint e1)); auto.
generalize (Zlt_cases z 0); intros.
generalize (Zlt_cases 0 z0); intros.
destruct (Zlt_bool z 0); destruct (Zlt_bool 0 z0).
simpl constraint_semantic.
assert ((s |b= constraint_semantic c1) /\ (s |b= constraint_semantic c2)).
split; Omega_exprb.
inversion_clear H6.
simpl in H7.
simpl in H8.
rewrite (H0 e e0) in H7; auto.
rewrite (H1 e1 e2) in H8; auto.
clear H0 H1.
simpl in H7; simpl in H8.
simpl.
rewrite (simpl_constraint_correct e) in H7; rewrite (H2 z) in H7; auto.
rewrite (simpl_constraint_correct e1) in H8; rewrite (H3 z0) in H8; auto.
rewrite (simpl_constraint_correct e); rewrite (H2 z); auto.
rewrite (simpl_constraint_correct e1); rewrite (H3 z0); auto.
generalize (Zge_cases 0 (store.lookup v s * z + eval e0 s)); intros.
rewrite H7 in H0; clear H7.
generalize (Zge_cases 0 (store.lookup v s * z0 + eval e2 s)); intros.
rewrite H8 in H1; clear H8.
generalize (omega_test_lemma1 _ _ _ _ _ H4 H5 H0 H1); intros.
generalize (Zge_cases 0 (z0 * eval e0 s - z * eval e2 s)); intros.
destruct (Zge_bool 0 (z0 * eval e0 s - z * eval e2 s)).
auto.
intuition.
simpl constraint_semantic.
generalize (Zlt_cases 0 z); intros.
destruct (Zlt_bool 0 z).
intuition.
simpl constraint_semantic.
Omega_exprb.
simpl constraint_semantic.
generalize (Zlt_cases 0 z); intros.
destruct (Zlt_bool 0 z).
generalize (Zlt_cases z0 0); intros.
destruct (Zlt_bool z0 0).
intuition.
simpl constraint_semantic.
Omega_exprb.
simpl constraint_semantic.
Omega_exprb.
simpl constraint_semantic.
generalize (Zlt_cases 0 z); intros.
destruct (Zlt_bool 0 z).
generalize (Zlt_cases z0 0); intros.
destruct (Zlt_bool z0 0).
assert ((s |b= constraint_semantic c1) /\ (s |b= constraint_semantic c2)).
split; Omega_exprb.
simpl constraint_semantic.
clear H4 H5.
inversion_clear H8.
simpl in H4.
simpl in H5.
rewrite (H0 e e0) in H4; auto.
rewrite (H1 e1 e2) in H5; auto.
simpl in H4; simpl in H5.
rewrite (simpl_constraint_correct e) in H4; rewrite (H2 z) in H4; auto.
rewrite (simpl_constraint_correct e1) in H5; rewrite (H3 z0) in H5; auto.
simpl.
rewrite (simpl_constraint_correct e); rewrite (H2 z); auto.
rewrite (simpl_constraint_correct e1); rewrite (H3 z0); auto.
generalize (Zge_cases 0 (store.lookup v s * z + eval e0 s)); intros.
rewrite H4 in H8; clear H4.
generalize (Zge_cases 0 (store.lookup v s * z0 + eval e2 s)); intros.
rewrite H5 in H4; clear H5.
generalize (omega_test_lemma1 _ _ _ _ _ H7 H6 H4 H8); intros.
generalize (Zge_cases 0 (z * eval e2 s - z0 * eval e0 s)); intros.
destruct (Zge_bool 0 (z * eval e2 s - z0 * eval e0 s)).
auto.
intuition.
simpl constraint_semantic.
Omega_exprb.
simpl constraint_semantic.
Omega_exprb.
Omega_exprb.
Omega_exprb.
Omega_exprb.
Qed.

Fixpoint elim_var_andlist' (c: constraint) (l l': andlist) (v: nat) {struct l} : andlist := 
  match l with
     nil => l'
     | hd::tl => if (inb beq_nat (expr_var (simpl_constraint_var_list' hd (v::nil))) v) then
                            (elim_var_andlist' c tl ((elim_var_constraint c hd v)::l') v)
                      else
                            (elim_var_andlist' c tl l' v)
  end.

Lemma elim_var_andlist'_correct: forall l l' c v,
  (forall s, (s |b=  (andlist_semantic (c::l ++ l'))) -> 
                s |b=  (andlist_semantic (elim_var_andlist' c l l' v))).
induction l.
simpl andlist_semantic.
intros; Omega_exprb.
simpl andlist_semantic; simpl andlist_semantic in IHl.
intros.
destruct inb.
assert (
(s |b= constraint_semantic c) /\
(s |b= constraint_semantic a) /\
(s |b= andlist_semantic (l++l'))
).
split; try Omega_exprb.
split; try Omega_exprb.
inversion_clear H0.
inversion_clear H2.
rewrite andlist_semantic_app in H3.
apply IHl.
cut(
(s |b= constraint_semantic c) /\
(s |b=  andlist_semantic (l ++ elim_var_constraint c a v :: l'))
).
intros.
inversion_clear H2.
Omega_exprb.
split; try Omega_exprb.
rewrite andlist_semantic_app.
cut(
(s |b=  andlist_semantic l) /\
(s |b=  andlist_semantic (elim_var_constraint c a v :: l'))
).
intro X; inversion_clear X.
Omega_exprb.
split; try Omega_exprb.
simpl andlist_semantic.
cut(
(s |b= constraint_semantic (elim_var_constraint c a v)) /\
(s |b= andlist_semantic l')
).
intro X; inversion_clear X.
Omega_exprb.
split; try Omega_exprb.
apply elim_var_constraint_correct.
Omega_exprb.
apply IHl.
Omega_exprb.
Qed.


Fixpoint elim_var_andlist (l l': andlist) (v: nat) {struct l} : andlist :=
  match l with
     nil => l'
     | hd::tl => if (inb beq_nat (expr_var (simpl_constraint_var_list' hd (v::nil))) v) then
                          (elim_var_andlist tl (l' ++ (elim_var_andlist' hd tl nil v)) v)
                      else
                          (elim_var_andlist tl (hd::l') v)
  end.

Lemma elim_var_andlist_correct: forall l l' v,
  (forall s, (s |b=  (andlist_semantic (l ++ l'))) -> 
                s |b=  (andlist_semantic (elim_var_andlist l l' v))).
induction l.
simpl andlist_semantic.
intuition.
simpl andlist_semantic.
intros.
destruct inb.
apply IHl.
rewrite (andlist_semantic_app).
cut(
(s |b= andlist_semantic l) /\
(s |b= andlist_semantic (l' ++ elim_var_andlist' a l nil v))
).
intros.
inversion_clear H0.
Omega_exprb.
assert(
(s |b= constraint_semantic a) /\
(s |b= andlist_semantic (l ++ l'))
).
split; try Omega_exprb.
split; try Omega_exprb.
inversion_clear H0.
rewrite (andlist_semantic_app) in H2.
Omega_exprb.
inversion_clear H0.
rewrite (andlist_semantic_app).
rewrite (andlist_semantic_app) in H2.
cut (
(s |b= andlist_semantic l') /\
(s |b= andlist_semantic (elim_var_andlist' a l nil v))
).
intro X; inversion_clear X.
Omega_exprb.
split; try Omega_exprb.
apply elim_var_andlist'_correct.
simpl andlist_semantic.
rewrite <- app_nil_end.
Omega_exprb.
apply IHl.
rewrite (andlist_semantic_app).
simpl andlist_semantic.
assert (
(s |b= constraint_semantic a) /\
(s |b=  andlist_semantic (l ++ l'))
).
split; try Omega_exprb.
inversion_clear H0.
rewrite (andlist_semantic_app) in H2.
Omega_exprb.
Qed.


Fixpoint elim_var_orlist (l: orlist) (v: nat) {struct l} : orlist :=
   match l with
      nil => nil
      | hd::tl => (elim_var_andlist hd nil v)::(elim_var_orlist tl v)
   end.

Lemma elim_var_orlist_correct: forall l v,
  (forall s, eval_b (orlist_semantic l) s = true -> 
               eval_b (orlist_semantic (elim_var_orlist l v)) s = true ).
induction l.
simpl.
intuition.
simpl orlist_semantic.
intros.
assert (
(s |b= andlist_semantic a) \/
(s |b= orlist_semantic l)
).
Eval_b_hyp_clean.
inversion_clear H0.
left; Omega_exprb.
right; Omega_exprb.
cut(
(s |b= andlist_semantic (elim_var_andlist a nil v)) \/
(s |b= orlist_semantic (elim_var_orlist l v))
).
intros.
inversion_clear H1; Omega_exprb.
inversion_clear H0.
left.
apply elim_var_andlist_correct.
rewrite <- app_nil_end.
auto.
right.
apply IHl.
auto.
Qed.


Fixpoint elim_varlist_orlist (l: orlist) (v: list nat) {struct v} : orlist :=
   match v with
      nil => l
      | hd::tl => (elim_varlist_orlist (elim_var_orlist l hd) tl)
   end.

Lemma elim_varlist_orlist_correct: forall v l,
 (forall s, eval_b (orlist_semantic l) s = true ->
               eval_b (orlist_semantic (elim_varlist_orlist l v)) s = true).
induction v.
auto.
simpl elim_varlist_orlist.
intros.
apply IHv.
apply elim_var_orlist_correct.
auto.
Qed.


(***********************************)


Definition eval_constraint (c : constraint) : option bool :=
   match expr_compute c with
     | Some z => Some (Zge_bool 0 z)
     | _ => None
   end.

Lemma eval_constraint2constraint_semantic: forall c b,
  eval_constraint c = Some b ->
  (forall s, eval_b (constraint_semantic c) s = b).
intros.
generalize (expr_compute_correct c); intros.
unfold eval_constraint in H.
destruct (expr_compute c); try discriminate.
simpl.
injection H; intros; subst b.
rewrite (H0 z); auto.
Qed.

Definition andb_option (a b: option bool) :=
  match a with
    None => None
    | Some a' => match b with
                           None => None
                           | Some b' => Some (andb a' b')
                         end
  end.

Definition orb_option (a b: option bool) :=
  match a with
    None => None
    | Some a' => match b with
                           None => None
                           | Some b' => Some (orb a' b')
                         end
  end.

Fixpoint eval_andlist' (a: andlist) : option bool :=
   match a with
     nil => Some true
     | hd::tl => match (eval_constraint hd) with
                         None => None
                         | Some b => andb_option (Some b) (eval_andlist' tl)
                      end
   end.

Lemma eval_andlist'2andlist_semantic: forall a b,
  eval_andlist' a = Some b ->
  (forall s, eval_b (andlist_semantic a) s = b).
induction a.
simpl.
intros.
injection H; auto.
simpl eval_andlist'.
intros.
generalize (eval_constraint2constraint_semantic a); intros.
destruct (eval_constraint a).
simpl in H0.
simpl.
rewrite (H0 b0); auto.
destruct (eval_andlist' a0).
lapply  (IHa b1); intros; auto.
rewrite H1.
injection H; auto.
inversion H.
inversion H.
Qed.

Definition eval_andlist (a: andlist) : option bool :=
  if (beq_nat (length a) 0) then
      None 
  else     
      eval_andlist' a.

Lemma eval_andlist2andlist_semantic: forall a b,
  eval_andlist a = Some b ->
  (forall s, eval_b (andlist_semantic a) s = b).
intros.
unfold eval_andlist in H.
generalize (beq_nat_classic (length a) 0); intro X; inversion_clear X.
rewrite H0 in H; discriminate.
rewrite H0 in H.
apply eval_andlist'2andlist_semantic; auto.
Qed.

Fixpoint eval_orlist' (o: orlist) : option bool :=
   match o with
     nil => Some false
     | hd::tl => orb_option (eval_andlist hd) (eval_orlist' tl)
   end.

Lemma eval_orlist'2orlist_semantic: forall a b,
  eval_orlist' a = Some b ->
  (forall s, eval_b (orlist_semantic a) s = b).
induction a; simpl; intros.
injection H; auto.
generalize ( eval_andlist2andlist_semantic a); intros.
destruct (eval_andlist a); simpl in H; try discriminate.
rewrite (H0 b0); auto.
destruct (eval_orlist' a0); simpl in H; try discriminate.
simpl in H.
lapply (IHa b1); intros.
rewrite H1.
injection H; auto.
auto.
Qed.

Definition eval_orlist (a: orlist) : option bool :=
  if (beq_nat (length a) 0) then
      None 
  else     
      eval_orlist' a.

Lemma eval_orlist2orlist_semantic: forall a b,
  eval_orlist a = Some b ->
  (forall s, eval_b (orlist_semantic a) s = b).
intros.
unfold eval_orlist in H.
generalize (beq_nat_classic (length a) 0); intro X; inversion_clear X.
rewrite H0 in H; discriminate.
rewrite H0 in H.
apply eval_orlist'2orlist_semantic; auto.
Qed.

(***********************************)


Definition omega_test (b: expr_b) : bool :=
   match (expr_b2constraints (! b)) with
      None => false
      | Some ol => match (eval_orlist (simpl_orlist (elim_varlist_orlist ol (expr_b_var b)))) with
                               None => false
                               | Some res => negb res
                            end
  end.

Lemma omega_test_correct: forall b,
   omega_test b = true ->
   (forall s, s |b= b).
intros.
unfold omega_test in H.
assert (
(s |b= b) \/
(s |b!= b)
).
destruct eval_b.
left; auto.
right; auto.
inversion_clear H0; auto.
generalize (expr_b2constraints_correct (!b)); intros.
destruct (expr_b2constraints (!b)).
assert (
s |b= !b
).
Omega_exprb.
clear H1.
rewrite (H0 o) in H2; auto.
clear H0.
assert (
eval_orlist (simpl_orlist (elim_varlist_orlist o (expr_b_var b))) = None \/
exists v, eval_orlist (simpl_orlist (elim_varlist_orlist o (expr_b_var b))) = Some v
).
destruct (eval_orlist (simpl_orlist (elim_varlist_orlist o (expr_b_var b)))).
right; exists b0; auto.
left; auto.
inversion_clear H0.
rewrite H1 in H; inversion H.
inversion_clear H1.
rewrite H0 in H.
destruct x.
simpl in H; discriminate.
generalize (eval_orlist2orlist_semantic _ _ H0 s); intros.
generalize (elim_varlist_orlist_correct (expr_b_var b) o s H2); intros.
rewrite  (simpl_orlist_correct) in H3.
Omega_exprb.
inversion H.
Qed.


(*
Definition t15 := ((var_e 1 >> var_e 2) =b> ((var_e 2 >> var_e 0) =b> (var_e 1 >> var_e 0))).
Eval compute in (omega_test t15).

Lemma t12l: forall s,
 s |b= ((var_e 1 >> var_e 2) =b> ((var_e 2 >> var_e 0) =b> (var_e 1 >> var_e 0))).
intros.
apply omega_test_correct.
unfold omega_test.

Eval compute in (expr_b2constraints
       (!(var_e 1 >> var_e 2 =b> var_e 2 >> var_e 0 =b> var_e 1 >> var_e 0))).


Eval compute in (expr_b_var (var_e 1 >> var_e 2 =b> var_e 2 >> var_e 0
=b> var_e 1 >> var_e 0)).

Eval compute in (elim_varlist_orlist ((((var_e 2 +e int_e 1%Z) -e var_e 1)
           :: ((var_e 0 +e int_e 1%Z) -e var_e 2)
              :: (var_e 1 -e var_e 0) :: nil) :: nil)
                 (expr_b_var
                    (var_e 1 >> var_e 2 =b>
                     var_e 2 >> var_e 0 =b> var_e 1 >> var_e 0))).



(* true *)
Definition test_term1 : expr_b :=
         ((((var_e 3) << (var_e 4)) ||| ((var_e 3) == (var_e 4))) &&& (((var_e 1) << (var_e 2)) ||| ((var_e 1) == (var_e 2)))) =b>
         ((((var_e 3) +e (var_e 1)) <<= ((var_e 4) +e (var_e 2)))).
Eval compute in (omega_test test_term1).


(* true *)
Definition test_term2 : expr_b :=
 (((int_e 0%Z) << (var_e 0)) &&& ((var_e 1) << (var_e 0))) =b> (((var_e 1) +e (int_e 1%Z)) << ((int_e 2%Z) *e (var_e 0))).
Eval compute in (omega_test test_term2).

(* fale *)
Definition test_term3: expr_b :=
 (((var_e 0) <<= (int_e 5%Z)) &&& ((var_e 0) >> (int_e 5%Z))).
Eval compute in (omega_test test_term3).

(* true *)
Definition test_term4: expr_b :=
 (((int_e 0%Z) <<= (int_e 5%Z))).
Eval compute in (omega_test test_term4).

(* true *)
Definition test_term5: expr_b :=
 ((var_e 0) <<= (var_e 0)).
Eval compute in (omega_test test_term5).

(* false *)
Definition test_term6: expr_b :=
 ((var_e 0) << (var_e 0)).
Eval compute in (omega_test test_term6).

(* false *)
Definition test_term7: expr_b :=
 (((var_e 1) +e (int_e 2%Z) +e (var_e 2)) <<= (var_e 3)) =b> ((var_e 1) <<= (var_e 3)).
Eval compute in (omega_test test_term7).

(* true *)
Definition test_term8: expr_b :=
 ((((var_e 1) +e (int_e 2%Z) +e (var_e 2)) <<= (var_e 3)) &&& ((var_e 2) >>= (int_e 0%Z))) =b> ((var_e 1) <<= (var_e 3)) .
Eval compute in (omega_test test_term8).

(* false *)
Definition test_term9: expr_b :=
  ((int_e 0%Z) << (var_e 0)) &&& ((int_e 9%Z) << (var_e 0)).
Eval compute in (omega_test test_term9).


(* true *)
Definition A:= (((var_e 0) +e (var_e 1)) *e ((var_e 0) +e (var_e 1))).
Definition B:= (((var_e 0) *e (var_e 0)) +e ((var_e 1) *e (var_e 1)) +e ((nat_e 2) *e (var_e 0) *e (var_e 1))).

Definition test_term13 : expr_b :=
  (A == B).
Eval compute in (omega_test test_term13).

Lemma implyb: forall s a b,
  (s |b= (a =b> b)) ->
  ((s |b= a) -> (s |b= b)).
  intros.
  Omega_exprb.
Qed.

Lemma dodo: forall a b,
  (a + b) * (a + b) = a*a + b*b + 2*a*b.
intros.
ring.
Show Proof.
Qed.

Lemma dodo2: forall a b,
  a < b -> a - b = 0.
intros.
omega.
Show Proof.
Qed.

Lemma imply_to_or: forall A B,
  (~A \/ B) -> (A -> B).
  intros.
  firstorder.
  Show Proof.
Qed.

*)