(*
 *  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 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
 *)

Require Import List.
Require Import ZArith.
Require Import List.
Require Import EqNat.
Require Import Classical.

Require Import util.
Require Import heap.

Import valandloc.

Module Type VAR.
  Parameter v : Set.
  Parameter eqdec : forall (x y : v), {x=y} + {x <> y}.
  Parameter fresh : v -> (list v) -> Prop.
  Parameter set : (list v) -> Prop.
End VAR.

Module var <: VAR with Definition v := nat.
  Definition v := nat.
  Definition eqdec := eq_nat_dec.
  Fixpoint fresh (x:v) (he:(list v)) {struct he} : Prop :=
    match he with
      | nil => True
      | hd::tl => (x <> hd) /\ (fresh x tl)
    end.
  
  Fixpoint set (he:(list v)) : Prop :=
    match he with
      nil => True
      | hd::tl => (fresh hd tl) /\ (set tl)
    end.
End var.

(* this tactic proves that two variables are different using a (var.set (...::nil)) hypothesis *)
Ltac Resolve_var_neq :=
   match goal with 
      | id: ?v <> ?v' |- ?v <> ?v' => auto
      | id: ?v' <> ?v |- ?v <> ?v' => auto
      | id: var.fresh ?v ?l |- ?v <> ?v' =>  let x := fresh in
                    (inversion_clear id as [x X]; decompose [and] X; clear X); Resolve_var_neq

      | id: var.fresh ?v' ?l |- ?v <> ?v' => let x := fresh in
                    (inversion_clear id as [x X]; decompose [and] X; clear X); Resolve_var_neq
      | id: var.set ?l |- ?v <> ?v' => 
             let x := fresh in
                    (inversion_clear id as [x X]; decompose [and] X; clear X); Resolve_var_neq
      | _ => fail
   end.


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

(* Store *)

Module Type STORE.
  Parameter s : Set.
  Parameter emp : s.
  Parameter lookup : var.v -> s -> Z.
  Parameter update : var.v -> Z -> s -> s.
  Parameter lookup_update : forall x y z st,
    x <> y -> lookup x st = lookup x (update y z st).
  Parameter lookup_update' : forall x z st,
    lookup x (update x z st) = z.
End STORE.

Module store : STORE.
  Definition s := list (var.v * Z).

  Definition emp : s := nil.
  
  (* Extract the value of a var from a store, default value is Z0 *)
  Fixpoint lookup (w:var.v) (st:s) {struct st} : Z :=
    match st with
      nil => Z0
      | (var', val')::tl =>
	match (var.eqdec w var') with
	  left _ => val'
	  | right _ => (lookup w tl)
	end
    end.

  (* update of the value of a variable in a store *)
  Fixpoint update (i:var.v) (w:Z) (st:s) {struct st} : s :=
    match st with
      nil => (i,w)::nil
      | (add', val')::tl =>
	match (var.eqdec i add') with
	  left _ => (add', w)::tl 
	  | right _ => (add', val')::(update i w tl)
	end
    end.

  Lemma lookup_update : forall x y z st,
    x <> y -> lookup x st = lookup x (update y z st).
    induction st.
    simpl.
    case (var.eqdec x y).
    tauto.
    auto.
    simpl.
    induction a.
    case (var.eqdec x a).
    intro; subst a.
    case (var.eqdec y x).
    intro; subst y; tauto.
    simpl.
    case (var.eqdec x x).
    auto.
    tauto.
    case (var.eqdec y a).
    intro.
    subst a.
    simpl.
    case (var.eqdec x y).
    tauto.
    auto.
    simpl.
    case (var.eqdec x a).
    tauto.
    auto.
  Qed.
    
  Lemma lookup_update' : forall w z st,
    lookup w (update w z st) = z.
    induction st.
    simpl.
    case (var.eqdec w w).
    auto.
    tauto.
    simpl.
    induction a.
    case (var.eqdec w a).
    intros.
    subst w.
    simpl.
    case (var.eqdec a a).
    auto.
    tauto.
    simpl.
    intros.
    case (var.eqdec w a).
    tauto.
    auto.
  Qed.
  
End store.

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

(* Expressions definition *)

Inductive expr : Set :=
  var_e : var.v -> expr
| int_e : Z -> expr
| add_e : expr -> expr -> expr
| min_e : expr -> expr -> expr
| mul_e : expr -> expr -> expr
| div_e : expr -> expr -> expr.

Definition nat_e (x:nat) := int_e (Z_of_nat x).

Definition null : expr := int_e 0%Z.

Notation "e1 '+e' e2" := (add_e e1 e2) (at level 79) : sep_scope.
Notation "e1 '-e' e2" := (min_e e1 e2) (at level 79) : sep_scope.
Notation "e1 '*e' e2" := (mul_e e1 e2) (at level 79) : sep_scope.
Notation "e1 '/e' e2" := (div_e e1 e2) (at level 79) : sep_scope.

Open Local Scope sep_scope.

Fixpoint expr_var (e:expr) {struct e}: list var.v :=
  match e with
    var_e x => x::nil
    | int_e z => nil
    | add_e e1 e2 => (expr_var e1) ++ (expr_var e2)
    | min_e e1 e2 => (expr_var e1) ++ (expr_var e2)
    | mul_e e1 e2 => (expr_var e1) ++ (expr_var e2)
    | div_e e1 e2 => (expr_var e1) ++ (expr_var e2)
  end.


Fixpoint expr_eq (e1: expr) (e2: expr) {struct e1} : bool :=
    match e1 with
       var_e w1 => match e2 with
                               var_e w2 => beq_nat w1 w2
                               | _ => false
                             end
       | int_e i1 => match e2 with
                               int_e i2 => Zeq_bool i1 i2
                               | _ => false
                             end
       | add_e e11 e12 => match e2 with
                               add_e e21 e22 =>  andb (expr_eq e11 e21) (expr_eq e12 e22)
                               | _ => false
                             end
       | min_e e11 e12 => match e2 with
                               min_e e21 e22 => andb (expr_eq e11 e21) (expr_eq e12 e22)
                               | _ => false
                             end
       | mul_e e11 e12 => match e2 with
                               mul_e e21 e22 => andb (expr_eq e11 e21) (expr_eq e12 e22)
                               | _ => false
                             end
       | div_e e11 e12 => match e2 with
                               div_e e21 e22 => andb (expr_eq e11 e21) (expr_eq e12 e22)
                               | _ => false
                             end
end.

Fixpoint expr_rewrite (e: expr) (patern: expr) (rep: expr) {struct e}: expr :=
    match e with
       var_e w => match (expr_eq e patern) with
                               true => rep
                               | false => e
                             end
       | int_e i => match (expr_eq e patern) with
                               true => rep
                               | false => e
                             end
       | add_e e1 e2 => match (expr_eq e patern) with
                               true => rep
                               | false => add_e (expr_rewrite e1 patern rep) (expr_rewrite e2 patern rep)
                             end
       | min_e e1 e2 => match (expr_eq e patern) with
                               true => rep
                               | false => min_e (expr_rewrite e1 patern rep) (expr_rewrite e2 patern rep)
                             end
       | mul_e e1 e2 => match (expr_eq e patern) with
                               true => rep
                               | false => mul_e (expr_rewrite e1 patern rep) (expr_rewrite e2 patern rep)
                             end
       | div_e e1 e2 => match (expr_eq e patern) with
                               true => rep
                               | false => div_e (expr_rewrite e1 patern rep) (expr_rewrite e2 patern rep)
                             end

end.

(* Compute the value of an expression on a store *)
Fixpoint eval (e:expr) (s:store.s) {struct e} : Z :=
match e with
  var_e w => (store.lookup w s)
| int_e i => i
| add_e e1 e2 => (Zplus (eval e1 s) (eval e2 s))
| min_e e1 e2 => (Zminus (eval e1 s) (eval e2 s))
| mul_e e1 e2 => (Zmult (eval e1 s) (eval e2 s))
| div_e e1 e2 => (Zdiv (eval e1 s) (eval e2 s))
end.

Lemma inde_expr : forall e l,
  inter (expr_var e) l nil ->
  forall x, In x l ->
    forall s z,
      eval e s = eval e (store.update x z s).
induction e.
simpl.
intros.
apply store.lookup_update.
red in H.
generalize (H x); intro.
inversion_clear H1.
intro.
subst x.
apply H2.
simpl; auto.
simpl.
auto.
intros.
cut ((inter (expr_var e1) l nil)/\(inter (expr_var e2) l nil)).
intro.
simpl.
inversion_clear H1.
rewrite (IHe1 _ H2 _ H0 s z).
rewrite (IHe2 _ H3 _ H0 s z).
auto.
simpl in H.
apply inter_app.
auto.
intros.
cut ((inter (expr_var e1) l nil)/\(inter (expr_var e2) l nil)).
intro.
simpl.
inversion_clear H1.
rewrite (IHe1 _ H2 _ H0 s z).
rewrite (IHe2 _ H3 _ H0 s z).
auto.
simpl in H.
apply inter_app.
auto.
intros.
cut ((inter (expr_var e1) l nil)/\(inter (expr_var e2) l nil)).
intro.
simpl.
inversion_clear H1.
rewrite (IHe1 _ H2 _ H0 s z).
rewrite (IHe2 _ H3 _ H0 s z).
auto.
simpl in H.
apply inter_app.
auto.
intros.
simpl.
cut ((inter (expr_var e1) l nil)/\(inter (expr_var e2) l nil)).
intro.
inversion_clear H1.
rewrite (IHe1 _ H2 _ H0 s z).
rewrite (IHe2 _ H3 _ H0 s z).
auto.
simpl in H.
apply inter_app.
auto.
Qed.

(* tactics for applying presburger *)
Ltac Z_to_nat x:= assert (Z_to_natA1: Zpos x = Z_of_nat (nat_of_P x)); [auto | rewrite Z_to_natA1; clear Z_to_natA1; unfold nat_of_P; simpl (Pmult_nat x 1);idtac ].

(*
Ltac Injection :=
          match goal with
             | |- _ => rewrite <- inj_plus; Injection
             | |- _ => rewrite <- inj_minus1; [ Injection | omega]
             | |- _ => rewrite <- inj_mult; Injection
             | |- _ => idtac
          end.
*)

Lemma Z0_mech: Z0 = Z_of_nat 0.
intuition.
Qed.

Ltac Supr_Z t :=
            match t with 
               | Z0 => rewrite Z0_mech
               | Zpos ?x => Z_to_nat x
               | Zplus ?x1 ?x2 => (Supr_Z x1 || idtac) ; (Supr_Z x2 || idtac); rewrite <- inj_plus
               | Zminus ? x1 ?x2 => (Supr_Z x1|| idtac) ; (Supr_Z x2 || idtac); rewrite <- inj_minus1; [ idtac | omega]
               | _ => idtac
             end.

Ltac Supr_Z_eq :=
             match goal with
                | |- ?x1 = ?x2 => Supr_Z x1; Supr_Z x2; (Supr_Z || idtac); apply Z_of_nat_inj'
                | |- ?x1 < ?x2 => Supr_Z x1; Supr_Z x2; (Supr_Z || idtac)
                | |- ?x1 > ?x2 => Supr_Z x1; Supr_Z x2; (Supr_Z || idtac)
                | |- ?x1 <= ?x2 => Supr_Z x1; Supr_Z x2; (Supr_Z || idtac)
                | |- ?x1 >= ?x2 => Supr_Z x1; Supr_Z x2; (Supr_Z || idtac)
             end.


Ltac Z_to_nat_Hyp x id:= assert (Z_to_natA1: Zpos x = Z_of_nat (nat_of_P x)); [auto | rewrite Z_to_natA1 in id; clear Z_to_natA1; unfold nat_of_P in id; simpl (Pmult_nat x 1) in id;idtac ].

Ltac Supr_Z_Hyp t id:=
            match t with 
               | Z0 => rewrite Z0_mech in id
               | Zpos ?x => Z_to_nat_Hyp x id
               | Zplus ?x1 ?x2 => (Supr_Z_Hyp x1 id || idtac) ; (Supr_Z_Hyp x2 id || idtac); rewrite <- inj_plus in id
               | Zminus ? x1 ?x2 => (Supr_Z_Hyp x1 id || idtac) ; (Supr_Z_Hyp x2 id || idtac); rewrite <- inj_minus1 in id; [  idtac | omega]
               | _ => idtac
             end.


Ltac Supr_Z_eq_Hyp := 
             match goal with
                | id: ?x1 = ?x2 |- _ => Supr_Z_Hyp x1 id; Supr_Z_Hyp x2 id; (Supr_Z_Hyp || idtac); (generalize ( Z_of_nat_inj _ _ id); intro || auto)
                | id: ?x1 > ?x2 |- _ => Supr_Z_Hyp x1 id; Supr_Z_Hyp x2 id; (Supr_Z_Hyp || idtac)
                | id: ?x1 < ?x2 |- _ => Supr_Z_Hyp x1 id; Supr_Z_Hyp x2 id; (Supr_Z_Hyp || idtac)
                | id: ?x1 >= ?x2 |- _ => Supr_Z_Hyp x1 id; Supr_Z_Hyp x2 id; (Supr_Z_Hyp || idtac)
                | id: ?x1 <= ?x2 |- _ => Supr_Z_Hyp x1 id; Supr_Z_Hyp x2 id; (Supr_Z_Hyp || idtac)
                | |- _ => idtac
             end.
           

Ltac Presb_Z := Supr_Z_eq; Supr_Z_eq_Hyp; (omega || idtac).

(*
Lemma test_Presb_Z: forall x y,
            ((Z_of_nat x) + 4%Z - 2%Z = (Z_of_nat (y +4)))%Z ->
            ((Z_of_nat (x+ 2)) + 2%Z = (Z_of_nat y) + 6%Z)%Z.
intros.
Presb_Z.
Qed.
*)


(* notation for structures *)
Notation "x '-.>' y " := ((var_e x) +e (int_e y)) (at level 79) : sep_scope.

(* boolean expression *)

Inductive expr_b : Set :=
  true_b: expr_b
  | eq_b : expr -> expr -> expr_b
  | neq_b : expr -> expr -> expr_b
  | ge_b : expr -> expr -> expr_b
  | gt_b : expr -> expr -> expr_b
  | neg_b : expr_b -> expr_b
  | and_b : expr_b -> expr_b -> expr_b
  | or_b : expr_b -> expr_b -> expr_b.

Notation "e == e'" := (eq_b e e') (at level 80) : sep_scope.
Notation "e =/= e'" := (neq_b e e') (at level 80) : sep_scope.
Notation "e &&& e'" := (and_b e e') (at level 80) : sep_scope.
Notation "e ||| e'" := (or_b e e') (at level 80) : sep_scope.
Notation "e >>= e'" := (ge_b e e') (at level 80) : sep_scope.
Notation "e >> e'" := (gt_b e e') (at level 80) : sep_scope.

Fixpoint expr_b_var (e:expr_b) : list var.v :=
  match e with 
    true_b => nil
    | eq_b e1 e2 => (expr_var e1) ++ (expr_var e2)
    | neq_b e1 e2 => (expr_var e1) ++ (expr_var e2)
    | ge_b e1 e2 => (expr_var e1) ++ (expr_var e2)
    | gt_b e1 e2 => (expr_var e1) ++ (expr_var e2)
    | and_b e1 e2 => (expr_b_var e1) ++ (expr_b_var e2)
    | or_b e1 e2 => (expr_b_var e1) ++ (expr_b_var e2)
    | neg_b e => (expr_b_var e)
  end.

Fixpoint expr_b_eq (e1: expr_b) (e2: expr_b) {struct e1} : bool :=
match e1 with
  true_b => match e2 with
                       true_b => true
                       | _ => false
                    end
  | f == g => match e2 with
                       f' == g' => andb (expr_eq f f') (expr_eq g g')
                       | _ => false
                    end   
  | f =/= g => match e2 with
                       f' =/= g' => andb (expr_eq f f') (expr_eq g g')
                       | _ => false
                    end   
  | f >>= g => match e2 with
                       f' >>= g' => andb (expr_eq f f') (expr_eq g g')
                       | _ => false
                    end   
  | f >> g => match e2 with
                       f' >> g' => andb (expr_eq f f') (expr_eq g g')
                       | _ => false
                    end   
  | f &&& g => match e2 with
                       f' &&& g' => andb (expr_b_eq f f') (expr_b_eq g g')
                       | _ => false
                    end   
  | f ||| g => match e2 with
                       f' ||| g' => andb (expr_b_eq f f') (expr_b_eq g g')
                       | _ => false
                    end   
  | neg_b e =>  match e2 with
                       neg_b e' => (expr_b_eq e e')
                       | _ => false
                    end   
end.   

Fixpoint expr_b_rewrite (e: expr_b) (patern: expr) (rep: expr) {struct e}: expr_b :=
match e with
  true_b => true_b
  | f == g => (expr_rewrite f patern rep) == (expr_rewrite g patern rep)
  | f =/= g => (expr_rewrite f patern rep) =/= (expr_rewrite g patern rep)
  | f >>= g => (expr_rewrite f patern rep) >>= (expr_rewrite g patern rep)
  | f >> g => (expr_rewrite f patern rep) >> (expr_rewrite g patern rep)
  | f &&& g => (expr_b_rewrite f patern rep) &&& (expr_b_rewrite g patern rep)
  | f ||| g => (expr_b_rewrite f patern rep) ||| (expr_b_rewrite g patern rep)
  | neg_b e => neg_b (expr_b_rewrite e patern rep)
end.  

(* Compute the value of an boolean expression *)
Fixpoint eval_b (e:expr_b) (s:store.s) {struct e} : bool :=
match e with
  true_b => true
  | f == g => (Zeq_bool (eval f s) (eval g s))
  | f =/= g => (negb (Zeq_bool (eval f s) (eval g s)))
  | f >>= g => (Zge_bool (eval f s) (eval g s))
  | f >> g => (Zgt_bool (eval f s) (eval g s))
  | f &&& g => (andb (eval_b f s) (eval_b g s))
  | f ||| g => (orb (eval_b f s) (eval_b g s))
  | neg_b e => negb (eval_b e s)
end.


Fixpoint expr_b_sem (e: expr_b) (s: store.s) {struct e}: Prop :=
match e with
  true_b => True
  | f == g => ((eval f s) = (eval g s))%Z
  | f =/= g => ((eval f s) <> (eval g s))%Z
  | f >>= g => ((eval f s) >= (eval g s))%Z
  | f >> g => ((eval f s) > (eval g s))%Z
  | f &&& g => (expr_b_sem f s) /\ (expr_b_sem g s)
  | f ||| g => (expr_b_sem f s) \/ (expr_b_sem g s)
  | neg_b e => ~ (expr_b_sem e s)
end. 

Lemma expr_b_semantic_good: forall e s,
                (eval_b e s = true) <-> (expr_b_sem e s).
induction e.

simpl.
split.
auto.
auto.

simpl.
split.
intros.
eapply Zeq_bool_true.
auto.
intros.
unfold eqb.
generalize (Zeq_bool_classic (eval e s) (eval e0 s)); intro X; inversion_clear X.
rewrite (Zeq_bool_true (eval e s) (eval e0 s)) in H.
tauto.
auto.
rewrite H.
apply Zeq_bool_refl.

simpl.
split.
intros.
generalize (Zeq_bool_false (eval e s) (eval e0 s)); intro X; inversion_clear X.
generalize (negb_true_is_false _ H).
intros.
tauto.
intros.
unfold eqb.
generalize (Zeq_bool_classic (eval e s) (eval e0 s)); intro X; inversion_clear X.
rewrite (Zeq_bool_true (eval e s) (eval e0 s)) in H.
tauto.
auto.
rewrite H0; auto.

simpl.
split.
intros.
generalize (Zge_cases (eval e s) (eval e0 s)).
intros.
rewrite H in H0.
auto.
simpl; intros.
generalize (Zge_cases (eval e s) (eval e0 s)).
intros.
assert (Zge_bool (eval e s) (eval e0 s)= true \/ Zge_bool (eval e s) (eval e0 s)= false).
elim Zge_bool.
left; auto.
right; auto.
inversion_clear H1.
auto.
rewrite H2 in H0.
auto.

simpl.
split.
intros.
generalize (Zgt_cases (eval e s) (eval e0 s)).
intros.
rewrite H in H0.
auto.
simpl; intros.
generalize (Zgt_cases (eval e s) (eval e0 s)).
intros.
assert (Zgt_bool (eval e s) (eval e0 s)= true \/ Zgt_bool (eval e s) (eval e0 s)= false).
elim Zgt_bool.
left; auto.
right; auto.
inversion_clear H1.
auto.
rewrite H2 in H0.
auto.

simpl; split.
intros.
assert (eval_b e s = true \/ eval_b e s = false).
elim eval_b.
left; auto.
right; auto.
inversion_clear H0.
rewrite H1 in H.
simpl in H; inversion_clear H.
elim (classic (expr_b_sem e s)).
intros.
generalize (IHe s); intro X; inversion_clear X.
intuition.
rewrite H1 in H5; inversion H5.
auto.
intros.
assert (eval_b e s = true \/ eval_b e s = false).
elim eval_b.
left; auto.
right; auto.
inversion_clear H0.
generalize (IHe s); intro X; inversion_clear X.
intuition.
rewrite H1; auto.

simpl; split.
intros.
generalize (IHe1 s); intro X; inversion_clear X.
generalize (IHe2 s); intro X; inversion_clear X.
generalize (andb_prop _ _ H); intro X; inversion_clear X.
intuition.
intros.
apply andb_true_intro.
generalize (IHe1 s); intro X; inversion_clear X.
generalize (IHe2 s); intro X; inversion_clear X.
intuition.

simpl; split.
intros.
generalize (IHe1 s); intro X; inversion_clear X.
generalize (IHe2 s); intro X; inversion_clear X.
generalize (orb_prop _ _ H); intro.
intuition.
intros.
apply orb_true_intro.
generalize (IHe1 s); intro X; inversion_clear X.
generalize (IHe2 s); intro X; inversion_clear X.
intuition.
Qed.

Lemma expr_b_false_negb_true: forall b s,
    eval_b b s = false -> eval_b (neg_b b) s = true.
intros.
simpl.
apply (negb_false_is_true).
rewrite negb_elim.
auto.
Qed.

Lemma expr_b_true_negb_false: forall b s,
    eval_b (neg_b b) s = true -> eval_b b s = false.
intros.
simpl.
apply (negb_true_is_false).
simpl in H.
auto.
Qed.


Ltac Eval_b_hyp h :=
            match goal with
               | h: eval_b ?e ?s = true |- _ => 
                     generalize (expr_b_semantic_good e s); intro eval_b_HypX; inversion_clear eval_b_HypX as [eval_b_HypX1 eval_b_HypX2]; 
                     generalize (eval_b_HypX1 h); clear eval_b_HypX1 eval_b_HypX2;
                     intro eval_b_HypX; simpl in eval_b_HypX; generalize eval_b_HypX; let x := fresh in intro x; clear eval_b_HypX; clear h
            end.

Ltac Eval_b_goal :=
            match goal with
                |  |-  eval_b ?e ?s = true => 
                     generalize (expr_b_semantic_good e s); intro eval_b_HypX; inversion_clear eval_b_HypX as [eval_b_HypX1 eval_b_HypX2]; 
                     apply (eval_b_HypX2); clear eval_b_HypX1 eval_b_HypX2; simpl
                |  |-  eval_b ?e ?s = false => apply (expr_b_true_negb_false e s); Eval_b_goal
               	| |- _ => idtac
            end.

Ltac Eval_b_hyp_clean :=
            match goal with
               | id: eval_b ?e ?s = true |- _ => Eval_b_hyp id;  Eval_b_hyp_clean
               | id: eval_b ?e ?s = false |- _ => generalize (expr_b_false_negb_true e s id); clear id; intro; Eval_b_hyp_clean
               | |- _ => idtac
            end.

Ltac Resolve_presb :=
            Eval_b_hyp_clean; Eval_b_goal; (tauto || omega || Presb_Z ).

(*
Lemma t1: forall e3 e4 e1 e2 s,
    eval_b ((e3 >> e4) &&& (e1 >>= e2)) s = true -> 
    eval_b (neg_b ((e3 +e e1) >> (e4 +e e2))) s = false.
intros.
Resolve_presb.
Qed.
*)

Open Local Scope heap_scope.

(* assertions *)

Definition assert := store.s -> heap.h -> Prop. 

(* The True/False assertions *)

Definition TT : assert := fun s h => True.

Definition FF : assert := fun s h => False.

Module sep.

(* The separation conjunction *)

Definition con (P Q:assert) : assert := fun s h =>
  exists h1, exists h2, h1 # h2 /\ h === h1 +++ h2 /\ P s h1 /\ Q s h2.

Notation "P ** Q" := (con P Q) (at level 80).

Lemma con_inde_store: forall P Q s s' h,
  ((P ** Q) s h) -> 
  (forall s s' h, P s h -> P s' h) -> 
  (forall s s' h, Q s h -> Q s' h) ->
  ((P ** Q) s' h).
intros.
red in H.
red.
inversion_clear H.
inversion_clear H2.
decompose [and] H; clear H.
exists x; exists x0.
intuition.
eapply H0.
apply H3.
eapply H1.
apply H6.
Qed.

(* The separation implication *)

Definition imp (P Q:assert) : assert := fun s h =>
  forall h', h # h' /\ P s h' ->
    forall h'', h'' === h +++ h' -> Q s h''.

Notation "P -* Q" := (imp P Q) (at level 80).

(** Assertions lemma *)

Definition entails (P Q:assert) : Prop :=
  forall s h, P s h -> Q s h.

Notation "P ==> Q" := (entails P Q) (at level 90, no associativity).

Definition equiv (P Q:assert) : Prop :=
  forall s h, P s h <-> Q s h.

Notation "P <==> Q" := (equiv P Q) (at level 90, no associativity).

Lemma con_TT : forall P, P ==> (P ** TT).
red.
intros.
exists h.
exists heap.emp.
split.
apply heap.disjoint_emp.
split.
apply heap.equal_sym.
apply heap.equal_union_emp.
split; auto.
red; auto.
Qed.

Lemma con_com : forall P Q, P ** Q ==> Q ** P.
red.
intros.
inversion_clear H as [h1].
inversion_clear H0 as [h2].
decompose [and] H; clear H.
exists h2.
exists h1.
split.
apply heap.disjoint_com; auto.
split.
apply heap.equal_trans with (h1 +++ h2); auto.
apply heap.union_com.
auto.
auto.
Qed.

Axiom assert_ext: forall P Q, (P <==> Q) -> P = Q.

Lemma con_com_equiv : forall P Q, (P ** Q) = (Q ** P).
intros.
apply assert_ext.
split; intros.
apply con_com; auto.
apply con_com; auto.
Qed.

Lemma con_assoc: forall P Q R, (P ** Q) ** R ==> P ** (Q ** R).
red.
intros.
inversion_clear H.
inversion_clear H0.
decompose [and] H; clear H.
inversion_clear H1.
inversion_clear H.
decompose [and] H1; clear H1.
exists x1; exists (heap.union x2 x0).
split.
apply heap.disjoint_union.
split; auto.
apply heap.equal_union_disjoint with x2 x.
auto.
split.
apply heap.equal_trans with (heap.union x x0); auto.
apply heap.equal_trans with (heap.union (heap.union x1 x2) x0); auto.
apply heap.equal_union; auto.
apply heap.disjoint_com; auto.
apply heap.equal_sym.
apply heap.union_assoc.
split; auto.
exists x2; exists x0.
split.
apply heap.equal_union_disjoint with x1 x.
split; auto.
apply heap.equal_trans with (heap.union x1 x2); auto.
apply heap.union_com.
auto.
split; auto.
apply heap.equal_refl.
Qed.

Lemma con_assoc_equiv : forall P Q R, ((Q ** P) ** R) = (Q ** (P ** R)).
intros.
apply assert_ext.
split; intros.
apply con_assoc.
auto.
rewrite con_com_equiv.
apply con_assoc.
rewrite con_com_equiv.
apply con_assoc.
rewrite con_com_equiv.
auto.
Qed.

Lemma mp : forall P Q, Q ** (Q -* P) ==> P.
red.
intros.
red in H.
inversion_clear H.
inversion_clear H0.
decompose [and] H; clear H.
red in H4.
assert (heap.disjoint x0 x).
apply heap.disjoint_com; auto.
apply (H4 _ (conj (heap.disjoint_com _ _ H0) H1)).
apply heap.equal_trans with (x +++ x0); auto.
apply heap.union_com.
apply heap.disjoint_com; auto.
Qed.

Lemma monotony : forall (P1 P2 Q1 Q2:assert),
  forall s h,
    ((forall h', P1 s h' -> P2 s h') /\ (forall h'', Q1 s h'' -> Q2 s h'')) -> 
    ((P1 ** Q1) s h -> (P2 ** Q2) s h).
intros.
red.
inversion_clear H0.
inversion_clear H1.
decompose [and] H0; clear H0.
generalize ((proj1 H) _ H2); intro.
generalize ((proj2 H) _ H5); intro.
exists x.
exists x0.
split; auto.
Qed.

Lemma adjunction : forall (P1 P2 P3:assert),
  forall s,
    (forall h, (P1 ** P2) s h -> P3 s h) ->
    (forall h, P1 s h -> (P2 -* P3) s h).
intros.
red.
intros.
apply H.
red.
exists h.
exists h'.
split; auto.
intuition.
intuition.
Qed.

Lemma adjunction' : forall (P1 P2 P3:assert),
  forall s,
    (forall h, P1 s h -> (P2 -* P3) s h) ->
       (forall h, (P1 ** P2) s h -> P3 s h).
intros.
inversion_clear H0.
inversion_clear H1.
decompose [and] H0; clear H0.
generalize (H x H2); intros.
red in H0.
eapply H0.
intuition.
apply H1; apply H3.
auto.
auto.
Qed.

Lemma imp_reg : forall P Q, P ==> Q -* (P ** Q).
red.
intros.
red.
intros.
red.
exists h.
exists h'.
split; auto.
intuition.
intuition.
Qed.

Definition emp : assert := fun s h => h === heap.emp.

Lemma con_emp : forall p,
  forall s h,
  (p ** emp) s h -> exists h', h === h' /\ p s h'.
  intros.
  inversion_clear H.
  inversion_clear H0.
  decompose [and] H; clear H.
  exists x; split; auto.
  red in H4.
  generalize (heap.equal_emp _ H4); intros.
  subst x0.
  apply heap.equal_trans with (x +++ heap.emp); auto.
  apply heap.equal_union_emp.
Qed.

Lemma con_emp' : forall P, P ==> (P ** emp).
  red.
  intros.
  exists h.
  exists heap.emp.
  split.
  apply heap.disjoint_emp.
  split.
  apply heap.equal_sym.
  apply heap.equal_union_emp.
  split.
  auto.
  red.
  apply heap.equal_refl.
Qed.

(* The mapping assertion *)
Definition mapsto e e' s h := 
  exists p, 
    val2loc (eval e s) = Some p /\ h === heap.singleton p (eval e' s).

Notation "e1 '|->' e2" := (mapsto e1 e2) (at level 79, no associativity).

Lemma mapsto_extensional: forall e1 e2 s h1 h2,
    h1 === h2 -> ((e1 |-> e2) s h1 <-> (e1 |-> e2) s h2).
intros.
split.
intros.
red.
red in H0.
inversion_clear H0.
inversion_clear H1.
exists x.
split.
auto.
eapply heap.equal_trans with h1.
apply heap.equal_sym.
auto.
auto.
intros.
red.
red in H0.
inversion_clear H0.
inversion_clear H1.
exists x.
split.
auto.
eapply heap.equal_trans with h2.
auto.
auto.
Qed.

Lemma mapsto_con_inversion : forall l e P s h,
  ((l |-> e) ** P) s h ->
  exists n,
    val2loc (eval l s) = Some n /\ 
    exists h',
      h === (heap.singleton n (eval e s)) +++ h' /\
      P s h'.
intros.
inversion_clear H as [h''].
inversion_clear H0 as [h'].
decompose [and] H; clear H.
inversion_clear H1 as [n].
inversion_clear H.
exists n.
split; auto.
exists h'.
split; auto.
apply heap.equal_trans with (h'' +++ h'); auto.
apply heap.equal_union; auto.
apply heap.disjoint_com; auto.
Qed.

Fixpoint mapstos (e:expr) (l:list expr) {struct l} : assert :=
  match l with
    nil => sep.emp
    | e1::tl => (e |-> e1) ** (mapstos (e +e (int_e 1%Z)) tl)
  end.

Notation "x '|-->' l" := (mapstos x l) (at level 80).

End sep.

Notation "P ** Q" := (sep.con P Q) (at level 80) : sep_scope.
Notation "P -* Q" := (sep.imp P Q) (at level 80) : sep_scope.
Notation "P ==> Q" := (sep.entails P Q) (at level 90, no associativity) : sep_scope.
Notation "P <==> Q" := (sep.equiv P Q) (at level 90, no associativity) : sep_scope.
Notation "e1 '|->' e2" := (sep.mapsto e1 e2) (at level 79, no associativity) : sep_scope.
Notation "x '|-->' l" := (sep.mapstos x l) (at level 80) : sep_scope.

(* Tactic for decision on disjointness equality over heap *)

Lemma disjoint_up: forall x x1 x2 x3,
    heap.equal x (heap.union x1 x3) -> heap.disjoint x1 x3 -> heap.disjoint x x2 -> heap.disjoint x1 x2.
intros.
eapply heap.equal_union_disjoint.
split.
apply H.
auto.
Qed.

Lemma union_in_equal_com: forall x x1 x2,
    heap.equal x (heap.union x1 x2) -> heap.disjoint x1 x2 -> heap.equal x (heap.union x2 x1).
intros.
apply (heap.equal_trans x (heap.union x1 x2) (heap.union x2 x1)).
auto.
apply heap.union_com.
auto.
Qed.

Ltac Disjoint_simpl :=
  match goal with
     | id : heap.disjoint ?x1 ?x2 |- heap.disjoint ?x1 ?x2 => apply id
     | id : heap.disjoint ?x2 ?x1 |- heap.disjoint ?x1 ?x2 => apply heap.disjoint_com; apply id
     | |- heap.disjoint ?x1 heap.emp => apply heap.disjoint_emp
     | |- heap.disjoint heap.emp ?x1 => apply heap.disjoint_com; apply heap.disjoint_emp
  end.


Ltac Disjoint_up :=
        (Disjoint_simpl ||  (Disjoint_up_left1) || (Disjoint_up_right1)) 
   with
  Disjoint_up_left1 :=
   match goal with
      | id1:  heap.equal ?X1 (heap.union ?x1 ?x1') , id2: heap.disjoint ?x1 ?x1'  |- heap.disjoint ?x1 ?x2 =>  
                apply (disjoint_up X1 x1 x2 x1' id1 id2); Disjoint_up
      | id1:  heap.equal ?X1 (heap.union ?x1' ?x1) , id2: heap.disjoint ?x1' ?x1   |- heap.disjoint ?x1 ?x2 => 
                apply (disjoint_up X1 x1 x2 x1' (union_in_equal_com X1 x1' x1 id1 id2) (heap.disjoint_com x1' x1 id2)) ; Disjoint_up
      |  |- heap.disjoint ?x1 ?x2 => (Disjoint_simpl)
   end
with
  Disjoint_up_right1 :=
   match goal with
      | id1:  heap.equal ?X1 (heap.union ?x2 ?x2') , id2: heap.disjoint ?x2 ?x2'  |- heap.disjoint ?x1 ?x2 =>  
                apply heap.disjoint_com; apply (disjoint_up X1 x2 x1 x2' id1 id2); Disjoint_up
      | id1:  heap.equal ?X1 (heap.union ?x2' ?x2) , id2: heap.disjoint ?x2' ?x2   |- heap.disjoint ?x1 ?x2 => 
                apply heap.disjoint_com; apply (disjoint_up X1 x2 x1 x2' (union_in_equal_com X1 x2' x2 id1 id2) (heap.disjoint_com x2' x2 id2)) ; Disjoint_up
      |  |- heap.disjoint ?x1 ?x2 => (Disjoint_simpl)
   end.

Ltac Disjoint_heap :=
  match goal with

     | id1: heap.disjoint (heap.union ?h1 ?h2)  ?h3 |- _ => 
               generalize (heap.disjoint_union' h1 h2 h3 (heap.disjoint_com (heap.union h1 h2) h3 id1)); intro X; inversion_clear X; clear id1; (Disjoint_simpl || Disjoint_heap)

     | id1: heap.disjoint ?h3 (heap.union  ?h1 ?h2) |- _ => 
               generalize (heap.disjoint_union' h1 h2 h3 id1); intro X; inversion_clear X; clear id1; (Disjoint_simpl || Disjoint_heap)

     |  |- heap.disjoint (heap.union ?x1 ?x2) ?x3 => 
               apply heap.disjoint_com; apply heap.disjoint_union; split; [ (Disjoint_simpl || Disjoint_heap) | (Disjoint_simpl || Disjoint_heap)]

     |  |- heap.disjoint ?x3 (heap.union ?x1 ?x2) => 
               apply heap.disjoint_union; split;[ (Disjoint_simpl || Disjoint_heap) | (Disjoint_simpl || Disjoint_heap)]

     |  |- heap.disjoint ?x1 ?x2 => (Disjoint_up)

   end.

(* Test for the tatcic *)

Lemma tactic_test_disjoint: forall h h1 h2 h11 h12 h21 h22 h111 h112 h121 h122 h211 h212 h221 h222,
     heap.disjoint h1 h2 ->
     heap.disjoint h11 h12 ->
     heap.disjoint h21 h22 ->
     heap.disjoint h111 h112 ->
     heap.disjoint h121 h122 ->
     heap.disjoint h211 h212 ->
     heap.disjoint h221 h222 ->
     heap.equal h (heap.union h1 h2) ->
     heap.equal h1 (heap.union h11 h12) ->
     heap.equal h2 (heap.union h21 h22) ->
     heap.equal h11 (heap.union h111 h112) ->
     heap.equal h12 (heap.union h121 h122) ->
     heap.equal h21 (heap.union h211 h212) ->
     heap.equal h22 (heap.union h221 h222) ->
     heap.disjoint (heap.union h112 h221) h222 .
intros.
Disjoint_heap.
Qed.

Lemma tactic_test_disjoint2: forall h h1 h2,
     heap.disjoint h (heap.union h1 h2) ->
     heap.disjoint h h2 .
intros.
Disjoint_heap.
Qed.


(* Lemmas for the Equality tactic *)

Lemma equal_tactic_l1: forall h1 h2 h3 h4,
    heap.disjoint h1 h2 ->
        heap.equal (heap.union h2 h1) (heap.union h3 h4) ->
             heap.equal (heap.union h1 h2) (heap.union h3 h4).
intros.
apply (heap.equal_trans (heap.union h1 h2) (heap.union h2 h1) (heap.union h3 h4)).
apply (heap.union_com).
auto.
auto.
Qed.

Lemma equal_tactic_l1': forall h1 h2 h3 h4,
      heap.disjoint h3 h4 ->
        heap.equal (heap.union h1 h2) (heap.union h4 h3) ->
             heap.equal (heap.union h1 h2) (heap.union h3 h4).
intros.
apply (heap.equal_trans (heap.union h1 h2) (heap.union h4 h3) (heap.union h3 h4)).
auto.
apply (heap.union_com).
Disjoint_heap.
Qed.


Lemma equal_tactic_l2: forall h1 h2 h3 H,
        heap.equal  H (heap.union (heap.union h1 h2) h3) ->
              heap.equal  H (heap.union h1 (heap.union h2 h3)).
intros.
apply (heap.equal_trans H (heap.union (heap.union h1 h2) h3) (heap.union h1 (heap.union h2 h3))).
auto.
apply heap.equal_sym.
apply heap.union_assoc.
Qed.

Lemma equal_tactic_l3: forall h1 h2 h3 H,
        heap.equal (heap.union (heap.union h1 h2) h3) H  ->
              heap.equal (heap.union h1 (heap.union h2 h3)) H.
intros.
apply heap.equal_sym.
generalize (heap.equal_sym _ _ H0); intro.
apply equal_tactic_l2.
auto.
Qed.

Lemma equal_tactic_l4: forall x1 x2 h1 h2 H,
        heap.equal H (heap.union x1 x2) ->
              heap.equal (heap.union x1 x2) (heap.union h1 h2) ->
                  heap.equal (heap.union h1 h2) H.
intros.
apply (heap.equal_trans (heap.union h1 h2) (heap.union x1 x2) H).
apply heap.equal_sym.
auto.
apply heap.equal_sym.
auto.
Qed.

Lemma equal_tactic_l4': forall x1 h1 h2 H,
        heap.equal H x1 ->
              heap.equal x1 (heap.union h1 h2) ->
                  heap.equal (heap.union h1 h2) H.
intros.
apply (heap.equal_trans (heap.union h1 h2) x1 H).
apply heap.equal_sym.
auto.
apply heap.equal_sym.
auto.
Qed.

Lemma equal_tactic_l5: forall x1 x2 h1 h2 H,
        heap.equal H (heap.union x1 x2) ->
              heap.equal (heap.union x1 x2) (heap.union h1 h2) ->
                  heap.equal H (heap.union h1 h2).
intros.
apply (heap.equal_trans H (heap.union x1 x2) (heap.union h1 h2)).
auto.
auto.
Qed.


Lemma equal_tactic_l5': forall x1 h1 h2 H,
        heap.equal H x1 ->
              heap.equal x1 (heap.union h1 h2) ->
                  heap.equal H (heap.union h1 h2).
intros.
apply (heap.equal_trans H x1 (heap.union h1 h2)).
auto.
auto.
Qed.


Lemma equal_tactic_l6: forall X Y,
     heap.equal X Y ->
         heap.equal (heap.union X heap.emp) Y.
intros.
apply (heap.equal_trans (heap.union X heap.emp) X Y).
apply heap.equal_union_emp.
auto.
Qed.

Lemma equal_tactic_l7: forall X Y,
     heap.equal Y X ->
         heap.equal (heap.union heap.emp X ) Y.
intros.
apply (heap.equal_trans (heap.union heap.emp X) (heap.union X heap.emp) Y).
apply heap.union_com.
apply heap.disjoint_com.
apply heap.disjoint_emp.
apply equal_tactic_l6.
apply heap.equal_sym.
auto.
Qed.

Lemma equal_tactic_l8: forall x1 x2 h1 X Y,
              heap.equal X (heap.union x1 x2) ->
                heap.disjoint h1 X ->
                  heap.disjoint x1 x2 ->
                    heap.equal (heap.union h1 (heap.union x1 x2) ) Y ->
                       heap.equal (heap.union h1 X) Y.
intros.
apply (heap.equal_trans (heap.union h1 X) (heap.union h1 (heap.union x1 x2)) Y).
generalize (heap.equal_union X (heap.union x1 x2) H h1 H0); intros.
apply (heap.equal_trans (heap.union h1 X) (heap.union X h1) (heap.union h1 (heap.union x1 x2))).
apply heap.union_com.
auto.
apply (heap.equal_trans (heap.union X h1) (heap.union (heap.union x1 x2) h1) (heap.union h1 (heap.union x1 x2))).
auto.
apply heap.union_com.
assert (heap.disjoint x1 h1).
eapply (heap.equal_union_disjoint).
split.
apply H.
apply heap.disjoint_com.
auto.
assert (heap.disjoint x2 h1).
eapply (heap.equal_union_disjoint).
split.
assert (heap.equal X (heap.union x2 x1)).
apply (heap.equal_trans X  (heap.union x1 x2)).
auto.
apply heap.union_com.
auto.
apply H5.
apply heap.disjoint_com.
auto.
apply heap.disjoint_com.
apply heap.disjoint_union.
split.
apply heap.disjoint_com.
auto.
apply heap.disjoint_com.
auto.
auto.
Qed.


Lemma equal_tactic_l8': forall x1 h1 X Y,
              heap.equal X x1 ->
                heap.disjoint h1 X ->
                    heap.equal (heap.union h1 x1 ) Y ->
                       heap.equal (heap.union h1 X) Y.
intros.
apply (heap.equal_trans (heap.union h1 X) (heap.union h1 x1) Y).
generalize (heap.equal_union X x1 H h1 H0); intros.
apply (heap.equal_trans (heap.union h1 X) (heap.union X h1) (heap.union h1 x1)).
apply heap.union_com.
auto.
apply (heap.equal_trans) with (heap.union x1 h1).
auto.
apply heap.union_com.
apply heap.disjoint_com.
eapply heap.disjoint_equal.
apply H0.
auto.
auto.
Qed.

Lemma equal_tactic_l9: forall X Y h1,
            heap.disjoint h1 X ->
               heap.equal X Y ->
                  heap.equal (heap.union X h1) (heap.union Y h1).
intros.
apply heap.equal_union.
auto.
auto.
Qed.

Lemma equal_tactic_l9': forall X Y x1 x2,
      heap.equal x1 x2 ->
            heap.disjoint x1 X ->
            heap.disjoint x2 X ->
               heap.equal X Y ->
                  heap.equal (heap.union X x1) (heap.union Y x2).
intros.
eapply heap.equal_trans with (heap.union X x2).
eapply heap.equal_trans with (heap.union x1 X).
eapply heap.union_com.
apply heap.disjoint_com.
auto.
eapply heap.equal_trans with (heap.union  x2 X).
apply equal_tactic_l9.
apply heap.disjoint_com.
auto.
auto.
eapply heap.union_com.
auto.
apply equal_tactic_l9.
auto.
auto.
Qed.

(* a cleaning tactic *)
Ltac emp_red := 
	   match goal with
	          | id: sep.emp ?s ?h |- _ => red in id; emp_red
		  | |-_ => idtac
	   end.
	

(* The equality tactic (obsolete) *)

Ltac Equal_heap' := emp_red; 
     match goal with

	 | id1: heap.equal ?h heap.emp |- _ => generalize (heap.equal_emp h id1); intro; subst h; [Equal_heap']

	 | id1: heap.equal heap.emp ?h |- _ => generalize (heap.equal_emp h (heap.equal_sym _ _ id1)); intro; subst h; [Equal_heap']

         | |- heap.equal (heap.union ?X ?h1) (heap.union ?Y ?h1) => apply (equal_tactic_l9 X Y h1); [Disjoint_heap | Equal_heap']

         | |- heap.equal ?h ?h => apply heap.equal_refl
(*
         | id1: heap.equal ?x1 ?x2 |- heap.equal ?x1 ?x2 => auto

         | id1: heap.equal ?x1 ?x2 |- heap.equal ?x2 ?x1 => apply heap.equal_sym; auto
*)

(*
         | id1: heap.equal ?x2 ?x1 |- heap.equal (heap.union ?X ?x1) (heap.union ?Y ?x2) => 
                           apply (equal_tactic_l9' X Y x1 x2 (heap.equal_sym x2 x1 id1)); [Disjoint_heap | Disjoint_heap | Equal_heap]

         | id1: heap.equal ?x1 ?x2 |- heap.equal (heap.union ?X ?x1) (heap.union ?Y ?x2) => 
                           apply (equal_tactic_l9' X Y x1 x2 id1); [Disjoint_heap | Disjoint_heap | Equal_heap]
*)
         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal (heap.union ?h1 ?X) ?Y => apply (equal_tactic_l8 x1 x2 h1 X Y id1); [Disjoint_heap | Disjoint_heap | Equal_heap' ]

         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal ?Y (heap.union ?h1 ?X) => apply heap.equal_sym; apply (equal_tactic_l8 x1 x2 h1 X Y id1); [Disjoint_heap | Disjoint_heap | apply heap.equal_sym;  Equal_heap' ]

         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal ?X (heap.union ?h1 ?h2) => apply (equal_tactic_l5 x1 x2 h1 h2 X id1); [Equal_heap']

         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal (heap.union ?h1 ?h2) ?X  => apply (equal_tactic_l4 x1 x2 h1 h2 X id1); [Equal_heap']
(*
         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal ?X ?h => apply (heap.equal_trans X (heap.union x1 x2) h id1); [Equal_heap]

         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal ?h ?X  => apply heap.equal_sym; apply (heap.equal_trans X (heap.union x1 x2) h id1); apply heap.equal_sym; [Equal_heap]
*)
         | |- heap.equal (heap.union ?h1 (heap.union ?h2 ?h3)) ?X=> apply equal_tactic_l3; [Equal_heap']

         | |- heap.equal  ?X (heap.union ?h1 (heap.union ?h2 ?h3))=> apply equal_tactic_l2; [Equal_heap']

         | |- heap.equal (heap.union ?X heap.emp) ?Y => apply equal_tactic_l6; [Equal_heap']

         | |- heap.equal ?Y (heap.union ?X heap.emp) => apply heap.equal_sym; apply equal_tactic_l6; [Equal_heap']

         | |- heap.equal (heap.union heap.emp ?X ) ?Y => apply equal_tactic_l7; [Equal_heap']

         | |- heap.equal ?Y (heap.union heap.emp ?X ) => apply heap.equal_sym; apply equal_tactic_l7; [Equal_heap']

         | |- heap.equal (heap.union ?h1 ?h2) ?X => apply equal_tactic_l1; [Disjoint_heap | Equal_heap']
         
         | |- heap.equal ?X (heap.union ?h1 ?h2) => apply equal_tactic_l1'; [Disjoint_heap | Equal_heap']
         
(*         | |- _ => idtac*)
                
      end.


(* An updated version suitable in case of destructive update *)

Ltac Equal_heap := emp_red;
     match goal with

	 | id1: heap.equal ?h heap.emp |- _ => generalize (heap.equal_emp h id1); intro; subst h; [Equal_heap]

	 | id1: heap.equal heap.emp ?h |- _ => generalize (heap.equal_emp h (heap.equal_sym _ _ id1)); intro; subst h; [Equal_heap]

         | |- heap.equal (heap.union ?X ?h1) (heap.union ?Y ?h1) => apply (equal_tactic_l9 X Y h1); [Disjoint_heap | Equal_heap]

         | |- heap.equal ?h ?h => apply heap.equal_refl

         | id1: heap.equal ?x1 ?x2 |- heap.equal ?x1 ?x2 => auto

         | id1: heap.equal ?x1 ?x2 |- heap.equal ?x2 ?x1 => apply heap.equal_sym; auto

         | id1: heap.equal ?x2 ?x1 |- heap.equal (heap.union ?X ?x1) (heap.union ?Y ?x2) => 
                           apply (equal_tactic_l9' X Y x1 x2 (heap.equal_sym x2 x1 id1)); [Disjoint_heap | Disjoint_heap | Equal_heap]

         | id1: heap.equal ?x1 ?x2 |- heap.equal (heap.union ?X ?x1) (heap.union ?Y ?x2) => 
                           apply (equal_tactic_l9' X Y x1 x2 id1); [Disjoint_heap | Disjoint_heap | Equal_heap]

         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal (heap.union ?h1 ?X) ?Y => apply (equal_tactic_l8 x1 x2 h1 X Y id1); [Disjoint_heap | Disjoint_heap | Equal_heap]

         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal ?Y (heap.union ?h1 ?X) => apply heap.equal_sym; apply (equal_tactic_l8 x1 x2 h1 X Y id1); [Disjoint_heap | Disjoint_heap | apply heap.equal_sym;  Equal_heap ]

         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal ?X (heap.union ?h1 ?h2) => apply (equal_tactic_l5 x1 x2 h1 h2 X id1); [Equal_heap]

         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal (heap.union ?h1 ?h2) ?X  => apply (equal_tactic_l4 x1 x2 h1 h2 X id1); [Equal_heap]

         | id1:  heap.equal ?X ?x1 |- heap.equal (heap.union ?h1 ?X) ?Y => apply (equal_tactic_l8' x1 h1 X Y id1); [Disjoint_heap | Disjoint_heap | Equal_heap ]

         | id1:  heap.equal ?X ?x1 |- heap.equal ?Y (heap.union ?h1 ?X) => apply heap.equal_sym; apply (equal_tactic_l8' x1 h1 X Y id1); [Disjoint_heap | Disjoint_heap | apply heap.equal_sym;  Equal_heap]

         | id1:  heap.equal ?X ?x1 |- heap.equal ?X (heap.union ?h1 ?h2) => apply (equal_tactic_l5' x1 h1 h2 X id1); [Equal_heap]

         | id1:  heap.equal ?X ?x1 |- heap.equal (heap.union ?h1 ?h2) ?X  => apply (equal_tactic_l4' x1 h1 h2 X id1); [Equal_heap]

         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal ?X ?h => apply (heap.equal_trans X (heap.union x1 x2) h id1); [Equal_heap]

         | id1:  heap.equal ?X (heap.union ?x1 ?x2) |- heap.equal ?h ?X  => apply heap.equal_sym; apply (heap.equal_trans X (heap.union x1 x2) h id1); apply heap.equal_sym; [Equal_heap]

         | |- heap.equal (heap.union ?h1 (heap.union ?h2 ?h3)) ?X=> apply equal_tactic_l3; [Equal_heap]

         | |- heap.equal  ?X (heap.union ?h1 (heap.union ?h2 ?h3))=> apply equal_tactic_l2; [Equal_heap]

         | |- heap.equal (heap.union ?X heap.emp) ?Y => apply equal_tactic_l6; [Equal_heap]

         | |- heap.equal ?Y (heap.union ?X heap.emp) => apply heap.equal_sym; apply equal_tactic_l6; [Equal_heap]

         | |- heap.equal (heap.union heap.emp ?X ) ?Y => apply equal_tactic_l7; [Equal_heap]

         | |- heap.equal ?Y (heap.union heap.emp ?X ) => apply heap.equal_sym; apply equal_tactic_l7; [Equal_heap]

         | |- heap.equal (heap.union ?h1 ?h2) ?X => apply equal_tactic_l1; [Disjoint_heap | Equal_heap]
         
         | |- heap.equal ?X (heap.union ?h1 ?h2) => apply equal_tactic_l1'; [Disjoint_heap | Equal_heap]
         
      end.

(*

Lemma tactic_test_equal: forall h h1 h2 h11 h12 h21 h22 h111 h112 h121 h122 h211 h212 h221 h222 (h3 h4:heap.h),
     heap.disjoint h1 h2 ->
     heap.disjoint h11 h12 ->
     heap.disjoint h21 h22 ->
     heap.disjoint h111 h112 ->
     heap.disjoint h121 h122 ->
     heap.disjoint h211 h212 ->
     heap.disjoint h221 h222 ->
     heap.equal h (heap.union h1 h2) ->
     heap.equal h1 (heap.union h11 h12) ->
     heap.equal h2 (heap.union h21 h22) ->
     heap.equal h11 (heap.union h111 h112) ->
     heap.equal h12 (heap.union h121 h122) ->
     heap.equal h21 (heap.union h211 h212) ->
     heap.equal h22 (heap.union h221 h222) ->
     heap.equal (heap.union h1 h2) (heap.union (heap.union h21 h12) (heap.union h22 (heap.union h111 h112))).


intros.
Equal_heap.
Qed.

Lemma tactic_test_equal2: forall h x0 x2 x4 x5 h1 h2 h3 h4 x x6 x7 x8 x9 h' h'' x11 x10,
	heap.disjoint x0 x2 ->
	heap.equal h (heap.union x0 x2) ->
	heap.disjoint x4 x5 ->
	heap.equal x2 (heap.union x4 x5) ->
	heap.disjoint h1 h2 ->
	heap.equal x4 (heap.union h1 h2) ->
	heap.disjoint x x6 ->
	heap.equal h1 (heap.union x x6) ->
	heap.disjoint x7 x8 ->
	heap.equal x (heap.union x7 x8) ->
	heap.disjoint x9 heap.emp ->
	heap.equal x8 (heap.union x9 heap.emp) ->
	heap.disjoint h3 h4 ->
	heap.equal h2 (heap.union h3 h4) ->
	heap.disjoint x10 x11 ->
	heap.equal h3 (heap.union x10 x11) ->
	heap.equal h4 heap.emp ->
	heap.equal h'' 
	(heap.union (heap.union x7 (heap.union x6 (heap.union h2 (heap.union x5 x0)))) h') ->
	heap.disjoint  (heap.union x7 (heap.union x6 (heap.union h2 (heap.union x5 x0)))) h' ->
	heap.equal h2 (heap.union x10 x11).
intros.
Equal_heap.
Qed.	
*)

(* Tactic to decompose / compose heap related to separating conjonction *)

Ltac Decompose_sepcon id h1 h2:=
  inversion_clear id as [h1 X]; inversion_clear X as [h2 Y]; decompose [and] Y; clear Y.
        
Ltac Compose_sepcon id1 id2:=
    exists id1; exists id2; split; [Disjoint_heap | (split;[ (Equal_heap) | split; idtac])].

Ltac Compose_sepcon' id1 id2:=
    exists id1; exists id2; split; [Disjoint_heap | (split;[ (Equal_heap') | split; idtac])].

Ltac Intro_sepimp id1 id2 := red; intro id1; intro X; inversion_clear X; intro id2; intro.

Definition inde (l:list var.v) (P:assert) :=
  forall s h,
    (forall x v, In x l -> (P s h <-> P (store.update x v s) h)).

Lemma inde_update_store : forall (P:assert) x z s h,
  inde (x::nil) P ->
  P s h ->
  P (store.update x z s) h.
intros.
red in H.
generalize (H s h x z); intro.
assert (In x (x::nil)).
red; simpl; auto.
tauto.
Qed.

Lemma inde_update_store' : forall (P:assert) x z s h,
  inde (x::nil) P ->
  P (store.update x z s) h ->
  P s h.
intros.
red in H.
generalize (H s h x z); intro.
assert (In x (x::nil)).
red; simpl; auto.
tauto.
Qed.

Lemma inde_sep_con : forall l (P Q:assert),
  inde l P -> inde l Q ->
  inde l (P ** Q).
unfold inde.
split; intros.
inversion_clear H2.
inversion_clear H3.
decompose [and] H2; clear H2.
exists x0; exists x1.
split; auto.
generalize (H s x0 x v H1); intro.
generalize (H0 s x1 x v H1); intro.
tauto.
inversion_clear H2.
inversion_clear H3.
decompose [and] H2; clear H2.
exists x0; exists x1.
split; auto.
generalize (H s x0 x v H1); intro.
generalize (H0 s x1 x v H1); intro.
tauto.
Qed.

Lemma inde_sep_imp : forall l (P Q:assert),
  inde l P -> inde l Q ->
  inde l (P -* Q).
intros.
red.
intros.
split; intros.
red in H2.
red.
intros.
assert (P s h').
red in H.
generalize (H s h' _ v H1); intro.
tauto.
generalize (H2 _ (conj (proj1 H3) H5)); intro.
red in H0.
generalize (H0 s h'' _ v H1); intro.
inversion_clear H7.
apply H8; clear H9.
apply H6.
auto.
red.
intros.
assert (P (store.update x v s) h').
red in H.
generalize (H s h' _ v H1); intro.
tauto.
generalize (H2 _ (conj (proj1 H3) H5)); intro.
red in H0.
generalize (H0 s h'' _ v H1); intro.
inversion_clear H7.
apply H9; clear H8.
apply H6.
auto.
Qed.

Lemma inde_mapsto : forall l p v,
  inter (expr_var p) l nil ->
  inter (expr_var v) l nil ->
  inde l (p |-> v).
intros.
red.
split; intros.
inversion_clear H2.
inversion_clear H3.
exists x0.
rewrite <-(inde_expr _ _ H _ H1 s v0).
rewrite <-(inde_expr _ _ H0 _ H1 s v0).
split; auto.
inversion_clear H2.
inversion_clear H3.
exists x0.
rewrite (inde_expr _ _ H _ H1 s v0).
rewrite (inde_expr _ _ H0 _ H1 s v0).
auto.
Qed.

Lemma inde_mapsto' : forall e x,
   inde x (fun s h => exists z, ((int_e e) |-> (int_e z)) s h).
split; intros.
inversion_clear H0.
exists x1.
intuition.
inversion_clear H0.
exists x1.
intuition.
Qed.

Lemma inde_mapsto'' : forall e1 e2 x,
   inde x ((int_e e1) |-> (int_e e2)).
split; intros; auto.
Qed.