(*Require Import ZArith.
Require Import util.
Require Import List.
Require Import heap.

Open Local Scope heap_scope.
*)
(*
 * heap-related tactics 
   *)

Lemma disjoint_up: forall x x1 x2 x3,
   x = (heap.union x1 x3) -> heap.disjoint x1 x3 -> heap.disjoint x x2 -> 
   heap.disjoint x1 x2.
  intros.
  apply heap.equal_union_disjoint with x3.
  rewrite <-H.
  auto.
Qed.

Lemma disjoint_up': forall x x1 x2 x3,
   x = (heap.union x1 x3) -> heap.disjoint x1 x3 -> heap.disjoint x x2 -> 
   heap.disjoint x3 x2.
  intros.
  apply heap.equal_union_disjoint with x1.
  assert ((x1 +++ x3) = (x3 +++ x1)).
  apply heap.union_com.
  auto.
  rewrite <-H2.
  rewrite <-H.
  auto.
Qed.

Ltac Disjoint_heap :=
 match goal with
    | id: (?x1 +++ ?x2) # ?x |- _ => generalize (heap.disjoint_union'
x1 x2 x (heap.disjoint_com (x1 +++ x2) x id)); intro Disjoint_heapA;
inversion_clear Disjoint_heapA; clear id; Disjoint_heap
    | id: ?x # (?x1 +++ ?x2) |- _ => generalize (heap.disjoint_union'
x1 x2 x id); intro Disjoint_heapA; inversion_clear Disjoint_heapA; clear
id; Disjoint_heap
    |  |- (?x1 +++ ?x2) # ?x3 => eapply heap.disjoint_com; eapply
heap.disjoint_union; split; [ (Disjoint_simpl || Disjoint_heap) |
(Disjoint_simpl || Disjoint_heap)]
    |  |- ?x3 # (?x1 +++ ?x2) => eapply heap.disjoint_union; split; [
(Disjoint_simpl || Disjoint_heap) | (Disjoint_simpl || Disjoint_heap)]
    |  |- ?x1 # ?x2 => Disjoint_up
  end
  with
 Disjoint_up :=
  (
     Disjoint_simpl ||  (Disjoint_up_left) || (Disjoint_up_right)
  )
  with
 Disjoint_up_left :=
  match goal with
     | id1:  ?X1 = (?x1 +++ ?x1')  |- ?x1 # ?x2 => apply (disjoint_up
X1 x1 x2 x1' id1); [(Disjoint_simpl || Disjoint_heap)|(Disjoint_simpl ||
Disjoint_heap)]
     | id1:  ?X1 = (?x1 +++ ?x1')  |- ?x1' # ?x2 => apply (disjoint_up'
X1 x1 x2 x1' id1) ; [(Disjoint_simpl || Disjoint_heap)|(Disjoint_simpl
|| Disjoint_heap)]
     |  |- ?x1 # ?x2 => (Disjoint_simpl)
  end
with
 Disjoint_up_right :=
  match goal with
     | id1: ?X1 = (?x2 +++ ?x2')  |- ?x1 # ?x2 => apply
heap.disjoint_com; apply (disjoint_up X1 x2 x1 x2' id1);
[(Disjoint_simpl || Disjoint_heap)|(Disjoint_simpl || Disjoint_heap)]
     | id1: ?X1 = (?x2 +++ ?x2')  |- ?x1 # ?x2' => apply
heap.disjoint_com; apply (disjoint_up' X1 x2 x1 x2' id1) ;
[(Disjoint_simpl || Disjoint_heap)|(Disjoint_simpl || Disjoint_heap)]
     |  |- ?x1 # ?x2 => (Disjoint_simpl)
  end
 with
 Disjoint_simpl :=
 match goal with
    | id : ?x1 # ?x2 |- ?x1 # ?x2 => auto
    | id : ?x2 # ?x1 |- ?x1 # ?x2 => apply heap.disjoint_com; auto
    | |- ?x1 # heap.emp => apply (heap.disjoint_emp x1)
    | |- heap.emp # ?x1 => apply heap.disjoint_com; apply
(heap.disjoint_emp x1)
 end.

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

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

Lemma equal_tactic_l2: forall h1 h2 h3 H,
  H = (heap.union (heap.union h1 h2) h3) ->
  H = (heap.union h1 (heap.union h2 h3)).
  intros.
  rewrite H0.
  apply sym_eq.
  apply heap.union_assoc.
Qed.

Lemma equal_tactic_l2': forall h1 h2 h3,
  (heap.union (heap.union h1 h2) h3) = (heap.union h1 (heap.union h2 h3)).
  intros.
  apply sym_eq.
  apply heap.union_assoc.
Qed.

Lemma equal_tactic_l3: forall h1 h2 h3 H,
  (heap.union (heap.union h1 h2) h3) = H  ->
  (heap.union h1 (heap.union h2 h3)) = H.
  intros.
  rewrite <- H0.
  apply heap.union_assoc.
Qed.

Lemma equal_tactic_l4: forall x1 x2 h1 h2 H,
  H = (heap.union x1 x2) ->
  (heap.union x1 x2) = (heap.union h1 h2) ->
  (heap.union h1 h2) = H.
  intros.
  rewrite H0.
  rewrite H1.
  auto.
Qed.

Lemma equal_tactic_l4': forall x1 h1 h2 H,
  H = x1 ->
  x1 = (heap.union h1 h2) ->
  (heap.union h1 h2) = H.
  intros.
  rewrite H0.
  rewrite H1.
  auto.
Qed.

Lemma equal_tactic_l5: forall x1 x2 h1 h2 H,
  H = (heap.union x1 x2) ->
  (heap.union x1 x2) = (heap.union h1 h2) ->
  H = (heap.union h1 h2).
  intros.
  rewrite H0.
  rewrite H1.
  auto.
Qed.

Lemma equal_tactic_l5': forall x1 h1 h2 H,
  H = x1 ->
  x1 = (heap.union h1 h2) ->
  H = (heap.union h1 h2).
  intros.
  rewrite H0.
  rewrite H1.
  auto.
Qed.

Lemma equal_tactic_l6: forall X Y,
  X = Y ->
  (heap.union X heap.emp) = Y.
  intros.
  rewrite H.
  apply heap.equal_union_emp.
Qed.

Lemma equal_tactic_l7: forall X Y,
  Y = X ->
        (heap.union heap.emp X ) = Y.
  intros.
  subst X.
  apply trans_eq with (heap.union Y heap.emp).
  apply heap.union_com.
  apply heap.disjoint_com.
  apply heap.disjoint_emp.
  apply heap.equal_union_emp.
Qed.

Lemma equal_tactic_l8: forall x1 x2 h1 X Y,
  X = (heap.union x1 x2) ->
  heap.disjoint h1 X ->
  heap.disjoint x1 x2 ->
  (heap.union h1 (heap.union x1 x2) ) =  Y ->
  (heap.union h1 X) = Y.
  intros.
  subst X Y.
  auto.
Qed.

Lemma equal_tactic_l8': forall x1 h1 X Y,
  X = x1 ->
  heap.disjoint h1 X ->
  (heap.union h1 x1) = Y ->
  (heap.union h1 X) = Y.
  intros.
  subst X Y.
  auto.
Qed.

Lemma equal_tactic_l9: forall X Y h1,
  h1 = X ->
  X = Y ->
  (heap.union X h1) = (heap.union Y h1).
  intros.
  subst X Y.
  auto.
Qed.

Lemma equal_tactic_l9': forall X Y x1 x2,
  x1 = x2 ->
  heap.disjoint x1 X ->
  heap.disjoint x2 X ->
  X = Y ->
  (heap.union X x1) = (heap.union Y x2).
  intros.
  subst Y x1.
  auto.
Qed.

Lemma equal_tactic_l10: forall X h1 h2,
  h1 = h2 ->
  (heap.union X h1) = (heap.union X h2).
  intros.
  subst h1.
  auto.
Qed.


Ltac Equal_heap :=
  (Equal_heap_clean || Equal_heap_main)
  with
  Equal_heap_clean :=
  match goal with
    | id: ?h = heap.emp |- _ => subst h; Equal_heap
    | id: heap.emp = ?h |- _ => subst h; Equal_heap
  end
  with
  Equal_heap_main :=
  match goal with
    | |-  (?h1 +++ ?h2) = (?h1 +++ ?h3) => apply (equal_tactic_l10 h1 h2 h3); Equal_heap
    | |- ?h1 = ?h1 => auto
    | |- (heap.emp +++ ?h1) = ?h2 => apply (equal_tactic_l7 h1 h2);
      [Equal_heap]
    | |- (?h1 +++ heap.emp) = ?h2 => apply (equal_tactic_l6 h1 h2);
      [Equal_heap]
    | |- ?h2 = (heap.emp +++ ?h1)  => symmetry; apply (equal_tactic_l7 h1 h2); [Equal_heap]
    | |- ?h2 = (?h1 +++ heap.emp) => symmetry;apply (equal_tactic_l6 h1 h2); [Equal_heap]
    |  id: ?X = (?x1 +++ ?x2) |- (?X +++ ?x1') = (?Y +++ ?x2') =>
      rewrite id ;  Equal_heap
    |  id: ?Y = (?y1 +++ ?y2) |- (?X +++ ?x1') = (?Y +++ ?x2') =>
      rewrite id ;  Equal_heap
    |  id: ?X = (?x1 +++ ?x2) |- ?X = (?Y +++ ?x2') => rewrite id ;
      Equal_heap
    |  id: ?Y = (?y1 +++ ?y2) |- (?X +++ ?x1') = ?Y => rewrite id ;
      Equal_heap
    | |- ((?h1 +++ ?h2) +++ ?h3) = ?X => rewrite (equal_tactic_l2' h1 h2 h3); [Equal_heap]
    | |- ?X = ((?h1 +++ ?h2) +++ ?h3)  => rewrite (equal_tactic_l2' h1 h2 h3); [Equal_heap]
    | |- (?h1 +++ ?h2) = (?h3 +++ ?h4) => apply  (equal_tactic_l1 h1 h2 h3 h4); [Disjoint_heap | Equal_heap]
    | id1: ?h1 = ?h2 |- ?h1 = ?h3 => rewrite id1; Equal_heap
    | id1: ?h1 = ?h2 |- ?h3 = ?h1 => rewrite id1; Equal_heap
  end.


Close Local Scope heap_scope.