Library CompOptCert.MemoryReorder

Require Import sflib.
From Paco Require Import paco.

Require Import Axioms.
Require Import Basic.
Require Import DataStructure.
Require Import DenseOrder.
Require Import Loc.

Require Import Event.
Require Import Time.
Require Import View.
Require Import Cell.
Require Import Memory.
Require Import MemoryFacts.

Require Import Cover.

Set Implicit Arguments.

Module MemoryReorder.
  Lemma add_add
        mem0 loc1 from1 to1 msg1
        mem1 loc2 from2 to2 msg2
        mem2
        (ADD1: Memory.add mem0 loc1 from1 to1 msg1 mem1)
        (ADD2: Memory.add mem1 loc2 from2 to2 msg2 mem2):
     mem1',
      <<ADD1: Memory.add mem0 loc2 from2 to2 msg2 mem1'>>
      <<ADD2: Memory.add mem1' loc1 from1 to1 msg1 mem2>>
      <<LOCTS: (loc1, to1) (loc2, to2)>>.
  Proof.
    exploit (@Memory.add_exists mem0 loc2 from2 to2).
    { i. inv ADD2. inv ADD. eapply DISJOINT.
      etrans; [eapply Memory.add_o; eauto|]. condtac; ss; eauto.
      des. subst. exploit Memory.add_get0; eauto. i. des. congr.
    }
    { inv ADD2. inv ADD. auto. }
    { inv ADD2. inv ADD. eauto. }
    i. des.
    exploit (@Memory.add_exists mem3 loc1 from1 to1).
    { i. revert GET2. erewrite Memory.add_o; eauto. condtac; ss.
      - des. subst. i. inv GET2.
        exploit Memory.add_get0; try exact ADD2; eauto.
        inv ADD2. inv ADD. symmetry. eapply DISJOINT.
        etrans; [eapply Memory.add_o; eauto|]. condtac; ss. des; congr.
      - guardH o. i. inv ADD1. inv ADD. eapply DISJOINT; eauto.
    }
    { inv ADD1. inv ADD. auto. }
    { inv ADD1. inv ADD. eauto. }
    i. des.
    esplits; eauto; cycle 1.
    { ii. inv H.
      exploit Memory.add_get0; try exact ADD2; eauto.
      erewrite Memory.add_o; eauto. condtac; s; i; des; congr.
    }
    cut (mem4 = mem2); [by i; subst; eauto|].
    apply Memory.ext. i.
    setoid_rewrite Memory.add_o; cycle 1; eauto.
    erewrite (@Memory.add_o mem3); eauto. erewrite (@Memory.add_o mem1); eauto.
    repeat (condtac; ss). des. subst.
    exploit Memory.add_get0; try exact ADD1; eauto. i. des.
    exploit Memory.add_get0; try exact ADD2; eauto. i. des.
    congr.
  Qed.

  Lemma add_split_same
        mem0 loc ts1 ts2 ts3 msg2 msg3 mem1 mem2
        (ADD1: Memory.add mem0 loc ts1 ts3 msg3 mem1)
        (SPLIT2: Memory.split mem1 loc ts1 ts2 ts3 msg2 msg3 mem2):
     mem1',
      <<ADD1: Memory.add mem0 loc ts1 ts2 msg2 mem1'>>
      <<ADD2: Memory.add mem1' loc ts2 ts3 msg3 mem2>>.
  Proof.
    exploit (@Memory.add_exists mem0 loc ts1 ts2 msg2); eauto.
    { i. inv ADD1. inv ADD. hexploit DISJOINT; eauto. i.
      eapply Interval.le_disjoint; eauto. econs; [refl|].
      inv SPLIT2. inv SPLIT. left. auto.
    }
    { inv SPLIT2. inv SPLIT. auto. }
    { inv SPLIT2. inv SPLIT. auto. }
    i. des.
    exploit (@Memory.add_exists mem3 loc ts2 ts3 msg3); eauto.
    { i. revert GET2. erewrite Memory.add_o; eauto. condtac; ss.
      - des. subst. i. inv GET2.
        symmetry. apply Interval.disjoint_imm.
      - i. inv ADD1. inv ADD. hexploit DISJOINT; eauto. i.
        eapply Interval.le_disjoint; eauto. econs; [|refl].
        inv SPLIT2. inv SPLIT. left. auto.
    }
    { inv SPLIT2. inv SPLIT. auto. }
    { inv ADD1. inv ADD. auto. }
    i. des.
    cut (mem4 = mem2); [by i; subst; eauto|].
    apply Memory.ext. i.
    erewrite Memory.add_o; eauto. erewrite Memory.add_o; eauto.
    erewrite (@Memory.split_o mem2); eauto. erewrite (@Memory.add_o mem1); eauto.
    repeat (condtac; ss). des. repeat subst.
    inv SPLIT2. inv SPLIT. exfalso. eapply Time.lt_strorder. eauto.
  Qed.

  Lemma add_split
        mem0 loc1 from1 to1 msg1
        mem1 loc2 ts21 ts22 ts23 msg22 msg23
        mem2
        (ADD1: Memory.add mem0 loc1 from1 to1 msg1 mem1)
        (SPLIT2: Memory.split mem1 loc2 ts21 ts22 ts23 msg22 msg23 mem2):
    (loc1 = loc2 from1 = ts21 to1 = ts23 msg1 = msg23
      mem1',
       <<ADD1: Memory.add mem0 loc2 ts21 ts22 msg22 mem1'>>
       <<ADD2: Memory.add mem1' loc2 ts22 ts23 msg23 mem2>>)
    (<<LOCTS1: (loc1, to1) (loc2, ts23)>>
      mem1',
       <<SPLIT1: Memory.split mem0 loc2 ts21 ts22 ts23 msg22 msg23 mem1'>>
       <<ADD2: Memory.add mem1' loc1 from1 to1 msg1 mem2>>).
  Proof.
    exploit Memory.split_get0; eauto. i. des.
    revert GET0. erewrite Memory.add_o; eauto. condtac; ss.
    { des. i. inv GET0. left. splits; eauto.
      eapply add_split_same; eauto.
    }
    guardH o. i. right. splits.
    { ii. inv H. unguardH o. des; congr. }
    exploit (@Memory.split_exists mem0 loc2 ts21 ts22 ts23);
      try by inv SPLIT2; inv SPLIT; eauto.
    i. des.
    exploit (@Memory.add_exists mem3 loc1 from1 to1);
      try by inv ADD1; inv ADD; eauto.
    { i. revert GET3. erewrite Memory.split_o; eauto. repeat condtac; ss.
      - des. subst. i. inv GET3.
        inv ADD1. inv ADD. hexploit DISJOINT; eauto. i. symmetry in H.
        symmetry. eapply Interval.le_disjoint; eauto. econs; [refl|].
        inv SPLIT2. inv SPLIT. left. auto.
      - guardH o0. i. des. inv GET3.
        inv ADD1. inv ADD. hexploit DISJOINT; eauto. i. symmetry in H.
        symmetry. eapply Interval.le_disjoint; eauto. econs; [|refl].
        inv SPLIT2. inv SPLIT. left. auto.
      - guardH o0. i. inv ADD1. inv ADD. eapply DISJOINT; eauto.
    }
    i. des.
    esplits; eauto.
    cut (mem4 = mem2); [by i; subst; eauto|].
    apply Memory.ext. i.
    erewrite Memory.add_o; eauto. erewrite Memory.split_o; eauto.
    setoid_rewrite Memory.split_o; cycle 1; eauto.
    erewrite (@Memory.add_o mem1); eauto.
    repeat (condtac; ss).
    - des. repeat subst.
      exploit Memory.add_get0; try exact ADD1; eauto. i. des.
      exploit Memory.split_get0; try exact SPLIT2; eauto. i. des.
      congr.
    - guardH o0. des. repeat subst. unguardH o. des; congr.
  Qed.

  Lemma add_lower
        mem0 loc1 from1 to1 msg1
        mem1 loc2 from2 to2 msg2 msg2'
        mem2
        (ADD1: Memory.add mem0 loc1 from1 to1 msg1 mem1)
        (LOWER2: Memory.lower mem1 loc2 from2 to2 msg2 msg2' mem2):
    (loc1 = loc2 from1 = from2 to1 = to2 msg1 = msg2
     Memory.add mem0 loc1 from1 to1 msg2' mem2)
    (<<LOCTS1: (loc1, to1) (loc2, to2)>>
      mem1',
       <<LOWER1: Memory.lower mem0 loc2 from2 to2 msg2 msg2' mem1'>>
       <<ADD2: Memory.add mem1' loc1 from1 to1 msg1 mem2>>).
  Proof.
    exploit Memory.lower_get0; eauto.
    erewrite Memory.add_o; eauto. condtac; ss.
    - des. subst. i. des. inv GET. left. splits; eauto.
      inv ADD1. inv ADD. inv LOWER2. inv LOWER.
      rewrite LocFun.add_add_eq. econs; auto.
      unfold Cell.add in ×.
      destruct r, r0. ss. subst.
      unfold LocFun.add. condtac; [|congr]. s.
      rewrite DOMap.add_add_eq. econs; auto.
    - guardH o. i. des. right. splits.
      { ii. inv H. unguardH o. des; congr. }
      exploit (@Memory.lower_exists mem0 loc2 from2 to2);
        try by inv LOWER2; inv LOWER; eauto.
      i. des.
      exploit (@Memory.add_exists mem3 loc1 from1 to1).
      { i. revert GET2. erewrite Memory.lower_o; eauto. condtac; ss.
        - des. subst. i. inv GET2.
          exploit Memory.lower_get0; eauto. i. des.
          inv ADD1. inv ADD. eapply DISJOINT. eauto.
        - guardH o0. i. inv ADD1. inv ADD. eapply DISJOINT; eauto.
      }
      { inv ADD1. inv ADD. auto. }
      { inv ADD1. inv ADD. eauto. }
      i. des.
      esplits; eauto.
      cut (mem4 = mem2); [by i; subst; eauto|].
      apply Memory.ext. i.
      erewrite Memory.add_o; eauto. erewrite Memory.lower_o; eauto.
      setoid_rewrite Memory.lower_o; cycle 1; eauto.
      erewrite (@Memory.add_o mem1); eauto.
      repeat (condtac; ss). des. repeat subst.
      unguardH o. des; congr.
  Qed.

  Lemma add_remove
        mem0 loc1 from1 to1 msg1
        mem1 loc2 from2 to2 msg2
        mem2
        (LOCTS1: (loc1, to1) (loc2, to2))
        (ADD1: Memory.add mem0 loc1 from1 to1 msg1 mem1)
        (REMOVE2: Memory.remove mem1 loc2 from2 to2 msg2 mem2):
     mem1',
      <<REMOVE1: Memory.remove mem0 loc2 from2 to2 msg2 mem1'>>
      <<ADD2: Memory.add mem1' loc1 from1 to1 msg1 mem2>>.
  Proof.
    exploit (@Memory.remove_exists mem0 loc2 from2 to2).
    { hexploit Memory.remove_get0; eauto.
      erewrite Memory.add_o; eauto. condtac; ss; i; des; subst; eauto. congr.
    }
    i. des.
    exploit (@Memory.add_exists mem3 loc1 from1 to1);
      try by inv ADD1; inv ADD; eauto.
    { i. revert GET2. erewrite Memory.remove_o; eauto. condtac; ss.
      inv ADD1. inv ADD. eauto.
    }
    i. des.
    cut (mem4 = mem2); [by i; subst; eauto|].
    apply Memory.ext. i.
    erewrite Memory.add_o; eauto. erewrite Memory.remove_o; eauto.
    erewrite (@Memory.remove_o mem2); eauto. erewrite (@Memory.add_o mem1); eauto.
    repeat (condtac; ss). des. repeat subst. congr.
  Qed.

  Lemma add_remove_same
        mem0 loc1 from1 to1 msg1
        mem1 from2 msg2
        mem2
        (ADD1: Memory.add mem0 loc1 from1 to1 msg1 mem1)
        (REMOVE2: Memory.remove mem1 loc1 from2 to1 msg2 mem2):
    from1 = from2 msg1 = msg2 mem0 = mem2.
  Proof.
    exploit Memory.add_get0; eauto. i. des.
    exploit Memory.remove_get0; eauto. i. des.
    rewrite GET0 in ×. inv GET1. splits; auto.
    apply Memory.ext. i.
    erewrite (@Memory.remove_o mem2); eauto. condtac; ss.
    - des. subst. ss.
    - erewrite (@Memory.add_o mem1); eauto. condtac; ss.
  Qed.

  Lemma split_add
        mem0 loc1 ts11 ts12 ts13 msg12 msg13
        mem1 loc2 from2 to2 msg2
        mem2
        (SPLIT1: Memory.split mem0 loc1 ts11 ts12 ts13 msg12 msg13 mem1)
        (ADD2: Memory.add mem1 loc2 from2 to2 msg2 mem2):
    <<LOCTS1: (loc1, ts12) (loc2, to2)>>
    <<LOCTS2: (loc1, ts13) (loc2, to2)>>
     mem1',
      <<ADD1: Memory.add mem0 loc2 from2 to2 msg2 mem1'>>
      <<SPLIT2: Memory.split mem1' loc1 ts11 ts12 ts13 msg12 msg13 mem2>>.
  Proof.
    exploit (@Memory.add_exists mem0 loc2 from2 to2);
      try by inv ADD2; inv ADD; eauto.
    { apply covered_disjoint_get_disjoint. i. rewrite <- split_covered in H; eauto.
      eapply get_disjoint_covered_disjoint; eauto. inv ADD2. inv ADD. auto.
    }
    i. des.
    exploit (@Memory.split_exists mem3 loc1 ts11 ts12 ts13);
      try by inv SPLIT1; inv SPLIT; eauto.
    { erewrite Memory.add_o; eauto. condtac; ss.
      - des. subst.
        hexploit Memory.add_get0; try exact ADD2; eauto. i. des.
        revert GET. erewrite Memory.split_o; eauto. repeat condtac; ss.
      - guardH o. hexploit Memory.split_get0; eauto. i. des. eauto.
    }
    i. des.
    splits.
    { ii. inv H.
      hexploit Memory.add_get0; try exact ADD2; eauto. i. des.
      revert GET. erewrite Memory.split_o; eauto. repeat condtac; ss.
      guardH o0. des; congr.
    }
    { ii. inv H.
      hexploit Memory.add_get0; try exact ADD2; eauto. i. des.
      revert GET. erewrite Memory.split_o; eauto. repeat condtac; ss.
      guardH o. des; congr.
    }
    cut (mem4 = mem2); [by i; subst; eauto|].
    apply Memory.ext. i.
    erewrite Memory.split_o; eauto. erewrite Memory.add_o; eauto.
    erewrite (@Memory.add_o mem2); eauto. erewrite (@Memory.split_o mem1); eauto.
    repeat (condtac; ss).
    - des. repeat subst.
      hexploit Memory.add_get0; try exact ADD2; eauto. i. des.
      revert GET. erewrite Memory.split_o; eauto. repeat condtac; ss.
    - guardH o. des. repeat subst.
      hexploit Memory.add_get0; try exact ADD2; eauto. i. des.
      revert GET. erewrite Memory.split_o; eauto. repeat condtac; ss.
  Qed.

  Lemma split_split
        mem0 loc1 ts11 ts12 ts13 msg12 msg13
        mem1 loc2 ts21 ts22 ts23 msg22 msg23
        mem2
        (LOCTS1: (loc1, ts13) (loc2, ts23))
        (SPLIT1: Memory.split mem0 loc1 ts11 ts12 ts13 msg12 msg13 mem1)
        (SPLIT2: Memory.split mem1 loc2 ts21 ts22 ts23 msg22 msg23 mem2):
    (loc1 = loc2 ts21 = ts11 ts23 = ts12
      mem1',
       <<SPLIT1: Memory.split mem0 loc2 ts21 ts22 ts13 msg22 msg13 mem1'>>
       <<SPLIT2: Memory.split mem1' loc1 ts22 ts12 ts13 msg12 msg13 mem2>>)
    ((loc2, ts21, ts23) (loc1, ts11, ts12)
      mem1',
       <<SPLIT1: Memory.split mem0 loc2 ts21 ts22 ts23 msg22 msg23 mem1'>>
       <<SPLIT2: Memory.split mem1' loc1 ts11 ts12 ts13 msg12 msg13 mem2>>).
  Proof.
    exploit Memory.split_get0; try exact SPLIT2; eauto. i. des.
    revert GET0. erewrite Memory.split_o; eauto. repeat condtac; ss.
    - i. des. inv GET0. left. splits; auto.
      exploit Memory.split_get0; try exact SPLIT1; eauto. i. des.
      exploit Memory.split_get0; try exact SPLIT2; eauto. i. des.
      revert GET4. erewrite Memory.split_o; eauto. condtac; ss.
      exploit (@Memory.split_exists mem0 loc1 ts21 ts22 ts13);
        try by inv SPLIT2; inv SPLIT; eauto.
      { etrans.
        - inv SPLIT2. inv SPLIT. eauto.
        - inv SPLIT1. inv SPLIT. eauto.
      }
      i. des.
      exploit (@Memory.split_exists mem3 loc1 ts22 ts12 ts13);
        (try by inv SPLIT1; inv SPLIT; eauto);
        (try by inv SPLIT2; inv SPLIT; eauto).
      { erewrite Memory.split_o; eauto. repeat condtac; ss.
        - des. subst. inv x0. inv SPLIT.
          exfalso. eapply Time.lt_strorder. eauto.
        - guardH o. des; congr.
      }
      i. des.
      cut (mem4 = mem2); [by i; subst; eauto|].
      apply Memory.ext. i.
      erewrite Memory.split_o; eauto. erewrite Memory.split_o; eauto.
      erewrite (@Memory.split_o mem2); eauto. erewrite (@Memory.split_o mem1); eauto.
      repeat (condtac; ss).
      + des. repeat subst. inv x1. inv SPLIT.
        exfalso. eapply Time.lt_strorder. eauto.
      + guardH o. des. repeat subst. inv x0. inv SPLIT.
        exfalso. eapply Time.lt_strorder. eauto.
    - guardH o. i. des. inv GET0. congr.
    - guardH o. guardH o0. i. right.
      exploit (@Memory.split_exists mem0 loc2 ts21 ts22 ts23);
        try by inv SPLIT2; inv SPLIT; eauto. i. des.
      exploit (@Memory.split_exists mem3 loc1 ts11 ts12 ts13);
        try by inv SPLIT1; inv SPLIT; eauto.
      { erewrite Memory.split_o; eauto. repeat condtac; ss.
        - des. subst. hexploit Memory.split_get0; try exact SPLIT2; eauto. i. des.
          revert GET3. erewrite Memory.split_o; eauto. repeat condtac; ss.
        - guardH o1. des. subst. unguardH o0. des; congr.
        - guardH o1. guardH o2. hexploit Memory.split_get0; try exact SPLIT1; eauto. i. des. eauto.
      }
      i. des. splits.
      { ii. inv H. unguardH o. des; congr. }
      cut (mem4 = mem2); [by i; subst; eauto|].
      apply Memory.ext. i.
      erewrite Memory.split_o; eauto. erewrite Memory.split_o; eauto.
      erewrite (@Memory.split_o mem2); eauto. erewrite (@Memory.split_o mem1); eauto.
      repeat (condtac; ss).
      + des. repeat subst.
        exploit Memory.split_get0; try exact SPLIT2; eauto. i. des.
        revert GET3. erewrite Memory.split_o; eauto. repeat condtac; ss.
      + guardH o1. des. repeat subst. unguardH o. des; congr.
      + guardH o1. des. repeat subst.
        exploit Memory.split_get0; try exact SPLIT2; eauto. i. des.
        revert GET3. erewrite Memory.split_o; eauto. repeat condtac; ss.
      + guardH o1. guardH o2. des. repeat subst. unguardH o0. des; congr.
  Qed.

  Lemma split_lower_diff
        mem0 loc1 ts11 ts12 ts13 msg12 msg13
        mem1 loc2 from2 to2 msg2 msg2'
        mem2
        (LOCTS1: (loc1, ts13) (loc2, to2))
        (SPLIT1: Memory.split mem0 loc1 ts11 ts12 ts13 msg12 msg13 mem1)
        (LOWER2: Memory.lower mem1 loc2 from2 to2 msg2 msg2' mem2):
    (loc1 = loc2 ts11 = from2 ts12 = to2 msg12 = msg2
     Memory.split mem0 loc1 ts11 ts12 ts13 msg2' msg13 mem2)
    ((loc1, ts12) (loc2, to2)
      mem1',
        <<LOWER1: Memory.lower mem0 loc2 from2 to2 msg2 msg2' mem1'>>
        <<SPLIT2: Memory.split mem1' loc1 ts11 ts12 ts13 msg12 msg13 mem2>>).
  Proof.
    exploit Memory.lower_get0; eauto. i. des.
    revert GET. erewrite Memory.split_o; eauto. repeat condtac; ss.
    - des. subst. i. inv GET. left. splits; auto.
      inv SPLIT1. inv SPLIT. inv LOWER2. inv LOWER.
      rewrite LocFun.add_add_eq. econs; auto.
      unfold Cell.split in ×.
      destruct r, r0. ss. subst.
      unfold LocFun.add. condtac; [|congr]. s.
      rewrite DOMap.add_add_eq. econs; auto.
    - guardH o. des. subst. congr.
    - guardH o. guardH o0. i. right.
      exploit (@Memory.lower_exists mem0 loc2 from2 to2);
        try by inv LOWER2; inv LOWER; eauto. i. des.
      exploit (@Memory.split_exists mem3 loc1 ts11 ts12 ts13);
        try by inv SPLIT1; inv SPLIT; eauto.
      { erewrite Memory.lower_o; eauto. condtac; ss.
        - des. subst. congr.
        - guardH o1. hexploit Memory.split_get0; try exact SPLIT1; eauto. i. des. eauto.
      }
      i. des.
      splits.
      { ii. inv H. exploit Memory.split_get0; try exact SPLIT1; eauto. i. des.
        exploit Memory.lower_get0; eauto. i. des. congr.
      }
      cut (mem4 = mem2); [by i; subst; eauto|].
      apply Memory.ext. i.
      erewrite Memory.split_o; eauto. erewrite Memory.lower_o; eauto.
      erewrite (@Memory.lower_o mem2); eauto. erewrite (@Memory.split_o mem1); eauto.
      repeat (condtac; ss).
      + des. repeat subst. congr.
      + guardH o1. des. repeat subst. congr.
  Qed.

  Lemma split_lower_same
        loc
        mem0 ts11 ts12 ts13 msg12 msg13
        mem1 from2 msg2 msg2'
        mem2
        (SPLIT1: Memory.split mem0 loc ts11 ts12 ts13 msg12 msg13 mem1)
        (LOWER2: Memory.lower mem1 loc from2 ts13 msg2 msg2' mem2):
    from2 = ts12 msg13 = msg2
     mem1',
      <<LOWER1: Memory.lower mem0 loc ts11 ts13 msg2 msg2' mem1'>>
      <<SPLIT2: Memory.split mem1' loc ts11 ts12 ts13 msg12 msg2' mem2>>.
  Proof.
    exploit Memory.lower_get0; eauto. erewrite Memory.split_o; eauto. repeat condtac; ss; cycle 2.
    { clear -o0. des; congr. }
    { des. subst. inv SPLIT1. inv SPLIT. exfalso. eapply Time.lt_strorder. eauto. }
    clear o a COND COND0. i. des. inv GET. splits; ss.
    exploit Memory.split_get0; eauto. i. des.
    exploit (@Memory.lower_exists mem0 loc ts11 ts13);
      try by inv LOWER2; inv LOWER; eauto.
    { inv SPLIT1. inv SPLIT. etrans; eauto. }
    i. des.
    exploit (@Memory.split_exists mem3 loc ts11 from2 ts13);
      try by inv SPLIT1; inv SPLIT; eauto.
    { erewrite Memory.lower_o; eauto. condtac; ss. des; congr. }
    i. des.
    cut (mem4 = mem2); [by i; subst; esplits; eauto|].
    apply Memory.ext. i.
    erewrite Memory.split_o; eauto. erewrite Memory.lower_o; eauto.
    erewrite (@Memory.lower_o mem2); eauto. erewrite (@Memory.split_o mem1); eauto.
    repeat (condtac; ss).
    des. repeat subst. congr.
  Qed.

  Lemma split_remove
        mem0 loc1 ts11 ts12 ts13 msg12 msg13
        mem1 loc2 from2 to2 msg2
        mem2
        (LOCTS1: (loc1, ts12) (loc2, to2))
        (LOCTS2: (loc1, ts13) (loc2, to2))
        (SPLIT1: Memory.split mem0 loc1 ts11 ts12 ts13 msg12 msg13 mem1)
        (REMOVE2: Memory.remove mem1 loc2 from2 to2 msg2 mem2):
     mem1',
      <<REMOVE1: Memory.remove mem0 loc2 from2 to2 msg2 mem1'>>
      <<SPLIT2: Memory.split mem1' loc1 ts11 ts12 ts13 msg12 msg13 mem2>>.
  Proof.
    exploit (@Memory.remove_exists mem0 loc2 from2 to2).
    { hexploit Memory.remove_get0; eauto.
      erewrite Memory.split_o; eauto. repeat condtac; ss.
      { des. subst. congr. }
      { guardH o. des. subst. congr. }
      guardH o. guardH o0. i. des. eauto.
    }
    i. des.
    exploit (@Memory.split_exists mem3 loc1 ts11 ts12 ts13);
      try by inv SPLIT1; inv SPLIT; eauto.
    { erewrite Memory.remove_o; eauto. condtac; ss.
      { des. subst. congr. }
      guardH o. hexploit Memory.split_get0; eauto. i. des. eauto.
    }
    i. des.
    cut (mem4 = mem2); [by i; subst; eauto|].
    apply Memory.ext. i.
    erewrite Memory.split_o; eauto. erewrite Memory.remove_o; eauto.
    erewrite (@Memory.remove_o mem2); eauto. erewrite (@Memory.split_o mem1); eauto.
    repeat (condtac; ss).
    - des. repeat subst. congr.
    - guardH o. des. repeat subst. congr.
  Qed.

  Lemma split_remove_same
        mem0 loc1 ts11 ts12 ts13 msg12 msg13
        mem1 from2 msg2
        mem2
        (SPLIT1: Memory.split mem0 loc1 ts11 ts12 ts13 msg12 msg13 mem1)
        (REMOVE2: Memory.remove mem1 loc1 from2 ts13 msg2 mem2):
    from2 = ts12 msg13 = msg2
     mem1',
      <<REMOVE1: Memory.remove mem0 loc1 ts11 ts13 msg13 mem1'>>
      <<ADD2: Memory.add mem1' loc1 ts11 ts12 msg12 mem2>>.
  Proof.
    exploit Memory.split_get0; eauto. i. des.
    exploit Memory.remove_get0; eauto. i. des.
    rewrite GET3 in ×. inv GET2. splits; auto.
    exploit (@Memory.remove_exists mem0 loc1 ts11 ts13 msg13); eauto. i. des.
    exploit (@Memory.add_exists mem3 loc1 ts11 ts12 msg12); eauto.
    { ii. revert GET2.
      erewrite Memory.remove_o; eauto. condtac; ss. i. des; ss.
      exploit Memory.get_disjoint; [exact GET0|exact GET2|..]. i. des.
      { subst. ss. }
      inv LHS. inv RHS. ss.
      apply (x2 x); econs; ss.
      inv SPLIT1. inv SPLIT.
      etrans; try exact TO. econs; ss. }
    { inv SPLIT1. inv SPLIT. ss. }
    { inv SPLIT1. inv SPLIT. ss. }
    i. des. esplits; eauto.
    cut (mem4 = mem2); [i; subst; eauto|].
    apply Memory.ext. i.
    erewrite Memory.add_o; eauto. erewrite Memory.remove_o; eauto.
    erewrite (@Memory.remove_o mem2); eauto. erewrite (@Memory.split_o mem1); eauto.
    repeat (condtac; ss).
    des. subst. congr.
  Qed.

  Lemma lower_add
        mem0 loc1 from1 to1 msg1 msg1'
        mem1 loc2 from2 to2 msg2
        mem2
        (LOWER1: Memory.lower mem0 loc1 from1 to1 msg1 msg1' mem1)
        (ADD2: Memory.add mem1 loc2 from2 to2 msg2 mem2):
     mem1',
      <<ADD1: Memory.add mem0 loc2 from2 to2 msg2 mem1'>>
      <<LOWER2: Memory.lower mem1' loc1 from1 to1 msg1 msg1' mem2>>
      <<LOCTS: (loc1, to1) (loc2, to2)>>.
  Proof.
    exploit (@Memory.add_exists mem0 loc2 from2 to2);
      try by inv ADD2; inv ADD; eauto.
    { apply covered_disjoint_get_disjoint. i. rewrite <- lower_covered in H; eauto.
      eapply get_disjoint_covered_disjoint; eauto. inv ADD2. inv ADD. auto.
    }
    i. des.
    exploit (@Memory.lower_exists mem3 loc1 from1 to1);
      try by inv LOWER1; inv LOWER; eauto.
    { erewrite Memory.add_o; eauto. condtac; ss.
      - des. subst. hexploit Memory.lower_get0; eauto. i. des.
        hexploit Memory.add_get0; eauto. i. des. congr.
      - guardH o. hexploit Memory.lower_get0; eauto. i. des. eauto.
    }
    i. des.
    esplits; eauto; cycle 1.
    { ii. inv H.
      exploit Memory.lower_get0; try exact LOWER1; eauto. i. des.
      exploit Memory.add_get0; eauto. i. des. congr.
    }
    cut (mem4 = mem2); [by i; subst; eauto|].
    apply Memory.ext. i.
    erewrite Memory.lower_o; eauto. erewrite Memory.add_o; eauto.
    erewrite (@Memory.add_o mem2); eauto. erewrite (@Memory.lower_o mem1); eauto.
    repeat (condtac; ss). des. repeat subst.
    exploit Memory.add_get0; try exact ADD2; eauto. i. des.
    revert GET. erewrite Memory.lower_o; eauto. condtac; ss.
  Qed.

  Lemma lower_split
        mem0 loc1 from1 to1 msg1 msg1'
        mem1 loc2 ts21 ts22 ts23 msg22 msg23
        mem2
        (LOWER1: Memory.lower mem0 loc1 from1 to1 msg1 msg1' mem1)
        (SPLIT2: Memory.split mem1 loc2 ts21 ts22 ts23 msg22 msg23 mem2):
     from1' msg23' mem1',
      <<SPLIT1: Memory.split mem0 loc2 ts21 ts22 ts23 msg22 msg23' mem1'>>
      <<LOWER2: Memory.lower mem1' loc1 from1' to1 msg1 msg1' mem2>>
      <<FROM1: __guard__ ((loc1, to1, from1', msg1', msg23') = (loc2, ts23, ts22, msg23, msg1)
                          ((loc1, to1) (loc2, ts23) (from1', msg23') = (from1, msg23)))>>.
  Proof.
    destruct (loc_ts_eq_dec (loc1, to1) (loc2, ts23)); ss.
    - des. subst.
      exploit Memory.split_get0; eauto. i. des.
      revert GET0. erewrite Memory.lower_o; eauto. condtac; ss; cycle 1.
      { des; congr. }
      i. inv GET0.
      exploit (@Memory.split_exists mem0 loc2 ts21 ts22 ts23);
        try by inv SPLIT2; inv SPLIT; eauto.
      { hexploit Memory.lower_get0; eauto. i. des. eauto. }
      i. des.
      exploit (@Memory.lower_exists mem3 loc2 ts22 ts23);
        try by inv LOWER1; inv LOWER; eauto.
      { erewrite Memory.split_o; eauto. repeat condtac; ss.
        ss. des. subst. inv SPLIT2. inv SPLIT.
        exfalso. eapply Time.lt_strorder. eauto.
      }
      { inv SPLIT2. inv SPLIT. auto. }
      i. des.
      esplits; eauto; cycle 1.
      { left. eauto. }
      cut (mem4 = mem2); [by i; subst; eauto|].
      apply Memory.ext. i.
      erewrite Memory.lower_o; eauto. erewrite Memory.split_o; eauto.
      erewrite (@Memory.split_o mem2); eauto. erewrite (@Memory.lower_o mem1); eauto.
      repeat (condtac; ss).
      des. repeat subst.
      revert GET. erewrite Memory.lower_o; eauto. condtac; ss.
    - guardH o.
      exploit Memory.split_get0; eauto. i. des.
      exploit (@Memory.split_exists mem0 loc2 ts21 ts22 ts23);
        try by inv SPLIT2; inv SPLIT; eauto.
      { revert GET0. erewrite Memory.lower_o; eauto. condtac; eauto.
        ss. i. des. inv GET0. unguardH o. des; congr.
      }
      i. des.
      exploit (@Memory.lower_exists mem3 loc1 from1 to1);
        try by inv LOWER1; inv LOWER; eauto.
      { erewrite Memory.split_o; eauto. repeat condtac; ss.
        - des. subst. hexploit Memory.split_get0; eauto.
          hexploit Memory.lower_get0; eauto. i. des. congr.
        - guardH o0. des. subst.
          unguardH o. des; congr.
        - guardH o0. guardH o1. hexploit Memory.lower_get0; eauto. i. des. eauto.
      }
      i. des.
      esplits; eauto; cycle 1.
      { right. splits; eauto. ii. inv H. unguardH o. des; congr. }
      cut (mem4 = mem2); [by i; subst; eauto|].
      apply Memory.ext. i.
      erewrite Memory.lower_o; eauto. erewrite Memory.split_o; eauto.
      erewrite (@Memory.split_o mem2); eauto. erewrite (@Memory.lower_o mem1); eauto.
      repeat (condtac; ss).
      + des. repeat subst.
        revert GET. erewrite Memory.lower_o; eauto. condtac; ss.
      + guardH o0. des. repeat subst. unguardH o. des; congr.
  Qed.

  Lemma lower_lower
        mem0 loc1 from1 to1 msg1 msg1'
        mem1 loc2 from2 to2 msg2 msg2'
        mem2
        (LOWER1: Memory.lower mem0 loc1 from1 to1 msg1 msg1' mem1)
        (LOWER2: Memory.lower mem1 loc2 from2 to2 msg2 msg2' mem2):
    (loc1 = loc2 from1 = from2 to1 = to2 msg1' = msg2
     Memory.lower mem0 loc1 from1 to1 msg1 msg2' mem2)
    (<<LOCTS1: (loc1, to1) (loc2, to2)>>
      mem1',
       <<LOWER1: Memory.lower mem0 loc2 from2 to2 msg2 msg2' mem1'>>
       <<LOWER2: Memory.lower mem1' loc1 from1 to1 msg1 msg1' mem2>>).
  Proof.
    exploit Memory.lower_get0; eauto. i. des.
    revert GET. erewrite Memory.lower_o; eauto. condtac; ss.
    - des. subst. i. inv GET. left. splits; eauto.
      inv LOWER1. inv LOWER. inv LOWER2. inv LOWER.
      rewrite LocFun.add_add_eq. econs; auto.
      unfold Cell.lower in ×.
      destruct r, r0. ss. subst.
      unfold LocFun.add. condtac; [|congr]. s.
      rewrite DOMap.add_add_eq. econs; auto.
      etrans; eauto.
    - guardH o. i. right. splits.
      { ii. inv H. unguardH o. des; congr. }
      exploit (@Memory.lower_exists mem0 loc2 from2 to2);
        try by inv LOWER2; inv LOWER; eauto.
      i. des.
      exploit (@Memory.lower_exists mem3 loc1 from1 to1);
        try by inv LOWER1; inv LOWER; eauto.
      { erewrite Memory.lower_o; eauto. condtac; ss.
        - des. subst. unguardH o. des; congr.
        - guardH o0. hexploit Memory.lower_get0; try exact LOWER1; eauto. i. des. eauto.
      }
      i. des.
      esplits; eauto.
      cut (mem4 = mem2); [by i; subst; eauto|].
      apply Memory.ext. i.
      erewrite Memory.lower_o; eauto. erewrite Memory.lower_o; eauto.
      erewrite (@Memory.lower_o mem2); eauto. erewrite (@Memory.lower_o mem1); eauto.
      repeat (condtac; ss). des. repeat subst.
      unguardH o. des; congr.
  Qed.

  Lemma lower_remove
        mem0 loc1 from1 to1 msg1 msg1'
        mem1 loc2 from2 to2 msg2
        mem2
        (LOCTS1: (loc1, to1) (loc2, to2))
        (LOWER1: Memory.lower mem0 loc1 from1 to1 msg1 msg1' mem1)
        (REMOVE2: Memory.remove mem1 loc2 from2 to2 msg2 mem2):
     mem1',
      <<REMOVE1: Memory.remove mem0 loc2 from2 to2 msg2 mem1'>>
      <<LOWER2: Memory.lower mem1' loc1 from1 to1 msg1 msg1' mem2>>.
  Proof.
    exploit (@Memory.remove_exists mem0 loc2 from2 to2).
    { hexploit Memory.remove_get0; eauto. i. des.
      revert GET. erewrite Memory.lower_o; eauto. condtac; ss.
      { des. subst. congr. }
      eauto.
    }
    i. des.
    exploit (@Memory.lower_exists mem3 loc1 from1 to1);
      try by inv LOWER1; inv LOWER; eauto.
    { erewrite Memory.remove_o; eauto. condtac; ss.
      { des. subst. congr. }
      inv LOWER1. inv LOWER. eauto.
    }
    i. des.
    cut (mem4 = mem2); [by i; subst; eauto|].
    apply Memory.ext. i.
    erewrite Memory.lower_o; eauto. erewrite Memory.remove_o; eauto.
    erewrite (@Memory.remove_o mem2); eauto. erewrite (@Memory.lower_o mem1); eauto.
    repeat (condtac; ss). des. repeat subst. congr.
  Qed.

  Lemma lower_remove_same
        mem0 loc1 from1 to1 msg1 msg1'
        mem1 from2 msg2
        mem2
        (LOWER1: Memory.lower mem0 loc1 from1 to1 msg1 msg1' mem1)
        (REMOVE2: Memory.remove mem1 loc1 from2 to1 msg2 mem2):
    from1 = from2 msg1' = msg2
    <<REMOVE1: Memory.remove mem0 loc1 from1 to1 msg1 mem2>>.
  Proof.
    exploit Memory.lower_get0; eauto. i. des.
    exploit Memory.remove_get0; eauto. i. des.
    rewrite GET1 in ×. inv GET0. splits; auto.
    exploit (@Memory.remove_exists mem0 loc1 from1 to1 msg1); eauto. i. des.
    cut (mem3 = mem2); [i; subst; eauto|].
    apply Memory.ext. i.
    erewrite Memory.remove_o; eauto.
    erewrite (@Memory.remove_o mem2); try exact REMOVE2.
    erewrite (@Memory.lower_o mem1); eauto.
    repeat (condtac; ss).
  Qed.

  Lemma remove_add
        mem0 loc1 from1 to1 msg1
        mem1 loc2 from2 to2 msg2
        mem2
        mem1'
        (REMOVE1: Memory.remove mem0 loc1 from1 to1 msg1 mem1)
        (ADD2: Memory.add mem1 loc2 from2 to2 msg2 mem2)
        (ADD1: Memory.add mem0 loc2 from2 to2 msg2 mem1'):
    Memory.remove mem1' loc1 from1 to1 msg1 mem2.
  Proof.
    exploit Memory.remove_get0; try eexact REMOVE1; eauto. i. des.
    exploit (@Memory.remove_exists mem1' loc1 from1 to1 msg1); eauto.
    { erewrite Memory.add_o; eauto. condtac; ss; eauto.
      des. subst. exploit Memory.add_get0; eauto. i. des. congr.
    }
    i. des.
    cut (mem3 = mem2); [by i; subst|].
    apply Memory.ext. i.
    erewrite Memory.remove_o; eauto. erewrite Memory.add_o; eauto.
    erewrite (@Memory.add_o mem2); eauto. erewrite (@Memory.remove_o mem1); eauto.
    repeat (condtac; ss). des. subst. subst.
    exploit Memory.add_get0; try eexact ADD1; eauto. i. des. congr.
  Qed.

  Lemma remove_add_disjloc
        mem0 loc1 from1 to1 msg1
        mem1 loc2 from2 to2 msg2
        mem2
        (REMOVE1: Memory.remove mem0 loc1 from1 to1 msg1 mem1)
        (ADD2: Memory.add mem1 loc2 from2 to2 msg2 mem2)
        (DISJ: loc1 loc2):
     mem1',
      Memory.add mem0 loc2 from2 to2 msg2 mem1'
      Memory.remove mem1' loc1 from1 to1 msg1 mem2.
  Proof.
    assert(Time.lt from2 to2 Message.wf msg2).
    {
      clear - ADD2.
      inv ADD2.
      inv ADD; eauto.
    }
    des.
    assert( mem1', Memory.add mem0 loc2 from2 to2 msg2 mem1').
    {
      eapply Memory.add_exists; eauto.
      i. cut(Memory.get loc2 to0 mem1 = Some (from0, msg0)).
      Focus 2.
      erewrite Memory.remove_o; eauto.
      des_ifs.
      ss; des; subst; ss.
      i.
      inv ADD2. inv ADD.
      unfold Memory.get in H1. unfold Cell.get in H1.
      eapply DISJOINT in H1; eauto.
    }
    des.
    eexists.
    split; eauto.
    eapply remove_add; eauto.
  Qed.

  Lemma remove_add_disjts
        mem0 loc from1 to1 msg1
        mem1 from2 to2 msg2
        mem2
        (REMOVE: Memory.remove mem0 loc from1 to1 msg1 mem1)
        (ADD: Memory.add mem1 loc from2 to2 msg2 mem2)
        (DISJ: Time.le to2 from1 Time.le to1 from2):
     mem1',
      Memory.add mem0 loc from2 to2 msg2 mem1'
      Memory.remove mem1' loc from1 to1 msg1 mem2.
  Proof.
    assert(Time.lt from2 to2 Message.wf msg2).
    {
      clear - ADD.
      inv ADD.
      inv ADD0; ss.
    }
    assert(Time.lt from1 to1 (from1 = Time.bot to1 = Time.bot)).
    {
      clear - REMOVE.
      inv REMOVE.
      inv REMOVE0.
      destruct r; ss.
      destruct mem0; ss.
      inv WF0.
      eapply VOLUME in GET; eauto.
      des; eauto.
      inv GET; ss.
      right; eauto.
    }
    destruct DISJ; destruct H.
    {
      assert( mem1', Memory.add mem0 loc from2 to2 msg2 mem1').
      {
        eapply Memory.add_exists; eauto.
        i.
        exploit Memory.remove_o; [eapply REMOVE | eauto..].
        instantiate(2 := loc); instantiate (1 := to0); i.
        des_ifH x0; ss.
        {
          destruct a; subst.
          eapply Memory.remove_get0 in REMOVE.
          destruct REMOVE.
          rewrite GET2 in H4; inv H4.
          ii. inv LHS; ss. inv RHS; ss.
          assert(Time.lt from1 to2).
          {
            clear - TO FROM0.
            eapply TimeFacts.lt_le_lt; eauto.
          }
          clear - H1 H4.
          eapply Time_le_gt_false; eauto.
        }
        {
          destruct o; ss.
          rewrite <- x0 in GET2.
          clear - ADD GET2.
          inv ADD.
          inv ADD0.
          unfold Memory.get in GET2.
          unfold Cell.get in GET2.
          eapply DISJOINT in GET2; eauto.
        }
      }
      destruct H3 as (mem1' & ADD').
      eexists.
      split; [eapply ADD' | idtac].
      eapply remove_add; eauto.
    }
    {
      assert( mem1', Memory.add mem0 loc from2 to2 msg2 mem1').
      {
        eapply Memory.add_exists; eauto.
        i.
        exploit Memory.remove_o; [eapply REMOVE | eauto..].
        instantiate(2 := loc); instantiate (1 := to0); i.
        des_ifH x0; ss.
        {
          destruct a; subst.
          eapply Memory.remove_get0 in REMOVE.
          destruct REMOVE.
          rewrite GET2 in H4; inv H4.
          ii. inv LHS; ss. inv RHS; ss.
          assert(Time.lt from2 to1).
          {
            clear - FROM TO0.
            eapply TimeFacts.lt_le_lt; eauto.
          }
          clear - H1 H4.
          eapply Time_lt_ge_false; eauto.
        }
        {
          destruct o; ss.
          rewrite <- x0 in GET2.
          clear - ADD GET2.
          inv ADD.
          inv ADD0.
          unfold Memory.get in GET2.
          unfold Cell.get in GET2.
          eapply DISJOINT in GET2; eauto.
        }
      }
      destruct H3 as (mem1' & ADD').
      eexists.
      split; [eapply ADD' | idtac].
      eapply remove_add; eauto.
    }
  Qed.

  Lemma remove_add_disj
        mem0 loc1 from1 to1 msg1
        mem1 loc2 from2 to2 msg2
        mem2
        (REMOVE: Memory.remove mem0 loc1 from1 to1 msg1 mem1)
        (ADD: Memory.add mem1 loc2 from2 to2 msg2 mem2)
        (DISJ: (loc1 loc2)
                 (loc1 = loc2 (Time.le to2 from1 Time.le to1 from2))):
     mem1',
      Memory.add mem0 loc2 from2 to2 msg2 mem1'
      Memory.remove mem1' loc1 from1 to1 msg1 mem2.
  Proof.
    des.
    eapply remove_add_disjloc; eauto.
    subst. eapply remove_add_disjts; eauto.
    subst. eapply remove_add_disjts; eauto.
  Qed.

  Lemma remove_split
        mem0 loc1 from1 to1 msg1
        mem1 loc2 ts21 ts22 ts23 msg22 msg23
        mem2
        mem1'
        (REMOVE1: Memory.remove mem0 loc1 from1 to1 msg1 mem1)
        (SPLIT2: Memory.split mem1 loc2 ts21 ts22 ts23 msg22 msg23 mem2)
        (SPLIT1: Memory.split mem0 loc2 ts21 ts22 ts23 msg22 msg23 mem1'):
    Memory.remove mem1' loc1 from1 to1 msg1 mem2.
  Proof.
    exploit Memory.remove_get0; try eexact REMOVE1; eauto. i. des.
    exploit Memory.split_get0; try exact SPLIT1; eauto. i. des.
    exploit (@Memory.remove_exists mem1' loc1 from1 to1 msg1); eauto.
    { erewrite Memory.split_o; eauto. repeat condtac; ss.
      - des. subst. congr.
      - guardH o. des. subst. rewrite GET0 in GET0. inv GET0.
        exploit Memory.split_get0; try exact SPLIT2; eauto. i. des.
        revert GET5. erewrite Memory.remove_o; eauto. condtac; ss.
    }
    i. des.
    cut (mem3 = mem2); [by i; subst|].
    apply Memory.ext. i.
    erewrite Memory.remove_o; eauto. erewrite Memory.split_o; eauto.
    erewrite (@Memory.split_o mem2); eauto. erewrite (@Memory.remove_o mem1); eauto.
    repeat (condtac; ss).
    - des; congr.
    - guardH o. des. subst. rewrite GET in GET2. inv GET2.
      exploit Memory.remove_get0; try exact GET1; eauto. i. des.
      revert GET2. erewrite Memory.split_o; eauto. repeat condtac; ss. i. inv GET2.
      inv SPLIT1. inv SPLIT. exfalso. eapply Time.lt_strorder. eauto.
  Qed.

  Lemma remove_split_aux
        mem0 loc1 from1 to1 msg1
        mem1 loc2 ts21 ts22 ts23 msg22 msg23
        mem2
        (REMOVE: Memory.remove mem0 loc1 from1 to1 msg1 mem1)
        (SPLIT: Memory.split mem1 loc2 ts21 ts22 ts23 msg22 msg23 mem2):
     mem1',
      Memory.split mem0 loc2 ts21 ts22 ts23 msg22 msg23 mem1'
      Memory.remove mem1' loc1 from1 to1 msg1 mem2.
  Proof.
    assert (WF_MSG: Message.wf msg22).
    {
      inv SPLIT. inv SPLIT0. eauto.
    }
    assert (LT: Time.lt ts21 ts22 Time.lt ts22 ts23).
    {
      inv SPLIT. inv SPLIT0; eauto.
    }
    des.
    exploit Memory.split_get0; eauto. ii; des.
    erewrite Memory.remove_o in GET0; eauto.
    des_ifH GET0; ss.
    exploit Memory.split_exists;
      [eapply GET0 | eapply LT | eapply LT0 | eapply WF_MSG | eauto..].
    ii. destruct x0.
    exploit remove_split; eauto.
  Qed.

  Lemma remove_lower
        mem0 loc1 from1 to1 msg1
        mem1 loc2 from2 to2 msg2' msg2
        mem2
        mem1'
        (REMOVE1: Memory.remove mem0 loc1 from1 to1 msg1 mem1)
        (LOWER2: Memory.lower mem1 loc2 from2 to2 msg2' msg2 mem2)
        (LOWER1: Memory.lower mem0 loc2 from2 to2 msg2' msg2 mem1'):
    Memory.remove mem1' loc1 from1 to1 msg1 mem2.
  Proof.
    exploit Memory.remove_get0; try eexact REMOVE1; eauto. i. des.
    exploit (@Memory.remove_exists mem1' loc1 from1 to1 msg1); eauto.
    { erewrite Memory.lower_o; eauto. condtac; ss.
      des. subst.
      exploit Memory.lower_get0; try exact LOWER2; eauto. i. des.
      revert GET1. erewrite Memory.remove_o; eauto. condtac; ss.
    }
    i. des.
    cut (mem3 = mem2); [by i; subst|].
    apply Memory.ext. i.
    erewrite Memory.remove_o; eauto. erewrite Memory.lower_o; eauto.
    erewrite (@Memory.lower_o mem2); eauto. erewrite (@Memory.remove_o mem1); eauto.
    repeat (condtac; ss). des. repeat subst.
    exploit Memory.lower_get0; try exact LOWER2; eauto. i. des.
    revert GET1. erewrite Memory.remove_o; eauto. condtac; ss.
  Qed.

  Lemma remove_lower_aux
        mem0 loc1 from1 to1 msg1
        mem1 loc2 from2 to2 msg2' msg2
        mem2
        (REMOVE: Memory.remove mem0 loc1 from1 to1 msg1 mem1)
        (LOWER: Memory.lower mem1 loc2 from2 to2 msg2' msg2 mem2):
     mem1',
      Memory.lower mem0 loc2 from2 to2 msg2' msg2 mem1'
      Memory.remove mem1' loc1 from1 to1 msg1 mem2.
  Proof.
    assert (WF_MSG: Message.wf msg2).
    {
      inv LOWER. inv LOWER0; eauto.
    }
    assert (LT: Time.lt from2 to2).
    {
      inv LOWER. inv LOWER0; eauto.
    }
    assert (MSG_LE: Message.le msg2 msg2').
    {
      inv LOWER. inv LOWER0. eauto.
    }
    exploit Memory.lower_get0; eauto. ii; des.
    erewrite Memory.remove_o in GET; eauto.
    des_ifH GET; ss.
    exploit Memory.lower_exists; eauto.
    intro LOWER'. destruct LOWER'.
    exploit Memory.lower_exists;
      [eapply GET | eapply LT | eapply WF_MSG | eauto..].
    clear o. ii; des.
    exploit remove_lower; eauto.
  Qed.

  Lemma remove_remove
        promises0 loc1 from1 to1 msg1
        promises1 loc2 from2 to2 msg2
        promises2
        (REMOVE1: Memory.remove promises0 loc1 from1 to1 msg1 promises1)
        (REMOVE2: Memory.remove promises1 loc2 from2 to2 msg2 promises2):
     promises1',
      <<REMOVE1: Memory.remove promises0 loc2 from2 to2 msg2 promises1'>>
      <<REMOVE2: Memory.remove promises1' loc1 from1 to1 msg1 promises2>>.
  Proof.
    exploit Memory.remove_get0; try apply REMOVE2; eauto. i. des.
    revert GET. erewrite Memory.remove_o; eauto. condtac; ss. guardH o. i.
    exploit Memory.remove_exists; eauto. i. des.
    hexploit Memory.remove_get0; try apply REMOVE1; eauto. i. des.
    exploit (@Memory.remove_exists mem2 loc1 from1 to1 msg1); eauto.
    { erewrite Memory.remove_o; eauto. condtac; ss. des. subst. congr. }
    i. des.
    esplits; eauto.
    cut (mem0 = promises2); [by i; subst|].
    apply Memory.ext. i.
    erewrite Memory.remove_o; eauto. erewrite Memory.remove_o; eauto.
    erewrite (@Memory.remove_o promises2); eauto. erewrite (@Memory.remove_o promises1); eauto.
    repeat (condtac; ss).
  Qed.


  Lemma promise_add_remove
        loc1 from1 to1 msg1
        loc2 from2 to2 msg2
        promises0 mem0
        promises1 mem1
        promises2
        (LOCTS1: (loc1, to1) (loc2, to2))
        (PROMISE1: Memory.promise promises0 mem0 loc1 from1 to1 msg1 promises1 mem1 Memory.op_kind_add)
        (REMOVE2: Memory.remove promises1 loc2 from2 to2 msg2 promises2):
     promises1',
      <<REMOVE1: Memory.remove promises0 loc2 from2 to2 msg2 promises1'>>
      <<PROMISE2: Memory.promise promises1' mem0 loc1 from1 to1 msg1 promises2 mem1 Memory.op_kind_add>>.
  Proof.
    inv PROMISE1.
    exploit add_remove; try exact PROMISES; eauto. i. des.
    esplits; eauto.
  Qed.

  Lemma promise_split_remove
        loc1 from1 to1 msg1
        loc2 from2 to2 msg2
        to3 msg3
        promises0 mem0
        promises1 mem1
        promises2
        (LOCTS1: (loc1, to1) (loc2, to2))
        (LOCTS2: (loc1, to3) (loc2, to2))
        (PROMISE1: Memory.promise promises0 mem0 loc1 from1 to1 msg1 promises1 mem1 (Memory.op_kind_split to3 msg3))
        (REMOVE2: Memory.remove promises1 loc2 from2 to2 msg2 promises2):
     promises1',
      <<REMOVE1: Memory.remove promises0 loc2 from2 to2 msg2 promises1'>>
      <<PROMISE2: Memory.promise promises1' mem0 loc1 from1 to1 msg1 promises2 mem1 (Memory.op_kind_split to3 msg3)>>.
  Proof.
    inv PROMISE1.
    exploit split_remove; try exact PROMISES; eauto. i. des.
    esplits; eauto. econs; eauto.
  Qed.

  Lemma promise_lower_remove
        loc1 from1 to1 msg0 msg1
        loc2 from2 to2 msg2
        promises0 mem0
        promises1 mem1
        promises2
        (LOCTS1: (loc1, to1) (loc2, to2))
        (PROMISE1: Memory.promise promises0 mem0 loc1 from1 to1 msg1 promises1 mem1 (Memory.op_kind_lower msg0))
        (REMOVE2: Memory.remove promises1 loc2 from2 to2 msg2 promises2):
     promises1',
      <<REMOVE1: Memory.remove promises0 loc2 from2 to2 msg2 promises1'>>
      <<PROMISE2: Memory.promise promises1' mem0 loc1 from1 to1 msg1 promises2 mem1 (Memory.op_kind_lower msg0)>>.
  Proof.
    inv PROMISE1.
    exploit lower_remove; try exact PROMISES; eauto. i. des.
    esplits; eauto.
  Qed.

  Lemma remove_promise
        promises1 loc1 from1 to1 msg1
        promises2 loc2 from2 to2 msg2
        promises3
        mem1 mem3
        kind
        (LE: Memory.le promises1 mem1)
        (REMOVE: Memory.remove promises1 loc1 from1 to1 msg1 promises2)
        (PROMISE: Memory.promise promises2 mem1 loc2 from2 to2 msg2 promises3 mem3 kind):
     promises2',
      Memory.promise promises1 mem1 loc2 from2 to2 msg2 promises2' mem3 kind
      Memory.remove promises2' loc1 from1 to1 msg1 promises3.
  Proof.
    inv PROMISE.
    - exploit Memory.add_exists_le; eauto. i. des.
      exploit remove_add; eauto.
    - exploit Memory.split_get0; try eexact PROMISES; eauto. i. des.
      revert GET0. erewrite Memory.remove_o; eauto. condtac; ss. i. guardH o.
      exploit Memory.split_exists; try exact GET0; try by inv PROMISES; inv SPLIT; eauto. i. des.
      exploit remove_split; eauto. i.
      esplits; eauto. econs; eauto.
    - exploit Memory.lower_get0; try eexact PROMISES; eauto. i. des.
      revert GET. erewrite Memory.remove_o; eauto. condtac; ss. i. guardH o.
      exploit Memory.lower_exists; try exact GET; try by inv PROMISES; inv LOWER; eauto. i. des.
      exploit remove_lower; eauto. i.
      esplits; eauto.
    - exploit remove_remove; try exact REMOVE; eauto. i. des. eauto.
  Qed.

  Lemma promise_add_promise_split_same
        promises0 mem0 loc ts1 ts2 ts3 msg2 msg3
        promises1 mem1
        promises2 mem2
        (ADD1: Memory.promise promises0 mem0 loc ts1 ts3 msg3 promises1 mem1 Memory.op_kind_add)
        (SPLIT2: Memory.promise promises1 mem1 loc ts1 ts2 msg2 promises2 mem2 (Memory.op_kind_split ts3 msg3)):
     promises1' mem1',
      <<ADD1: Memory.promise promises0 mem0 loc ts1 ts2 msg2 promises1' mem1' Memory.op_kind_add>>
      <<ADD2: Memory.promise promises1' mem1' loc ts2 ts3 msg3 promises2 mem2 Memory.op_kind_add>>.
  Proof.
    inv ADD1. inv SPLIT2.
    exploit add_split; try exact PROMISES; eauto. i. des; [|congr].
    exploit add_split; try exact MEM; eauto. i. des; [|congr].
    esplits.
    - econs; eauto.
      i. exploit Memory.add_get0; try exact MEM. i. des.
      exploit Memory.add_get1; try exact GET; try exact MEM. i.
      exploit Memory.get_ts; try exact GET1. i. des.
      { subst. inv ADD3. inv ADD. inv TO. }
      exploit Memory.get_ts; try exact x8. i. des.
      { subst. inv ADD0. inv ADD. inv TO. }
      exploit Memory.get_disjoint; [exact GET1|exact x8|..]. i. des.
      { subst. inv ADD0. inv ADD. timetac. }
      destruct (TimeFacts.le_lt_dec ts3 to').
      + apply (x11 ts3); econs; ss; try refl.
        inv ADD3. inv ADD. ss.
      + apply (x11 to'); econs; ss; try refl.
        { etrans; try exact x10. inv ADD0. inv ADD. ss. }
        { econs. ss. }
    - econs; eauto.
      i. revert GET.
      erewrite Memory.add_o; eauto. condtac; ss; eauto.
      i. des. subst. inv GET. inv MEM. inv ADD. timetac.
  Qed.

  Lemma promise_split_promise_split_same
        promises0 mem0 loc ts1 ts2 ts3 ts4 val2 released2 msg3 msg4
        promises1 mem1
        promises2 mem2
        (SPLIT1: Memory.promise promises0 mem0 loc ts1 ts3 msg3 promises1 mem1 (Memory.op_kind_split ts4 msg4))
        (SPLIT2: Memory.promise promises1 mem1 loc ts1 ts2 (Message.concrete val2 released2) promises2 mem2 (Memory.op_kind_split ts3 msg3)):
     promises1' mem1',
      <<SPLIT1: Memory.promise promises0 mem0 loc ts1 ts2 (Message.concrete val2 released2) promises1' mem1' (Memory.op_kind_split ts4 msg4)>>
      <<SPLIT2: Memory.promise promises1' mem1' loc ts2 ts3 msg3 promises2 mem2 (Memory.op_kind_split ts4 msg4)>>.
  Proof.
    assert (LOCTS: (loc, ts4) (loc, ts3)).
    { intro X. inv X. inv SPLIT1. inv MEM. inv SPLIT. timetac. }
    inv SPLIT1. inv SPLIT2.
    exploit split_split; try exact PROMISES; eauto. i. des; [|congr].
    exploit split_split; try exact MEM; eauto. i. des; [|congr].
    esplits.
    - econs; eauto; congr.
    - econs; eauto.
  Qed.

  Lemma promise_lower_promise_split_same
        promises0 mem0 loc ts1 ts2 ts3 msg0 val2 released2 msg3
        promises1 mem1
        promises2 mem2
        (LOWER1: Memory.promise promises0 mem0 loc ts1 ts3 msg3 promises1 mem1 (Memory.op_kind_lower msg0))
        (SPLIT2: Memory.promise promises1 mem1 loc ts1 ts2 (Message.concrete val2 released2) promises2 mem2 (Memory.op_kind_split ts3 msg3)):
     promises1' mem1',
      <<SPLIT1: Memory.promise promises0 mem0 loc ts1 ts2 (Message.concrete val2 released2) promises1' mem1' (Memory.op_kind_split ts3 msg0)>>
      <<LOWER2: Memory.promise promises1' mem1' loc ts2 ts3 msg3 promises2 mem2 (Memory.op_kind_lower msg0)>>.
  Proof.
    inv LOWER1. inv SPLIT2.
    exploit lower_split; try exact PROMISES; eauto. i. des.
    unguard. des; [|congr]. inv FROM1.
    exploit lower_split; try exact MEM; eauto. i. des.
    unguard. des; [|congr]. inv FROM1.
    esplits.
    - econs; eauto; congr.
    - econs; eauto.
  Qed.

  Lemma split_remove_the_split_msg_stable
        mem1 loc from to ts msg1 msg2 mem2 msg3 mem3 loc0 to0 from0 msg0
        (SPLIT: Memory.split mem1 loc from to ts msg1 msg2 mem2)
        (REMOVE: Memory.remove mem2 loc from to msg3 mem3)
        (GET: Memory.get loc0 to0 mem1 = Some (from0, msg0)):
     from0', Memory.get loc0 to0 mem3 = Some (from0', msg0).
  Proof.
    exploit Memory.split_get1; eauto. ii; des.
    exploit Memory.remove_get1; eauto. ii; des; subst.
    {
      exploit Memory.split_get0; eauto. ii; des.
      rewrite GET in GET0. ss.
    }
    {
      eauto.
    }
  Qed.

  Lemma split_remove_the_split_msg_stable_rvs
        mem1 loc from to ts msg1 msg2 mem2 msg3 mem3 loc0 to0 from0 msg0
        (SPLIT: Memory.split mem1 loc from to ts msg1 msg2 mem2)
        (REMOVE: Memory.remove mem2 loc from to msg3 mem3)
        (GET: Memory.get loc0 to0 mem3 = Some (from0, msg0)):
    (loc0 = loc to0 = ts from0 = to msg0 = msg2)
    (Memory.get loc0 to0 mem1 = Some (from0, msg0)).
  Proof.
    erewrite Memory.remove_o in GET; eauto.
    des_ifH GET; ss; des; subst; ss; eauto.
    erewrite Memory.split_o in GET; eauto.
    des_ifH GET; ss; des; subst; ss; eauto.
    des_ifH GET; ss; des; subst; ss; eauto.
    des_ifH GET; ss; des; subst; ss; eauto.
    erewrite Memory.split_o in GET; eauto.
    des_ifH GET; ss; des; subst; ss; eauto.
    des_ifH GET; ss; des; subst; ss; eauto.
    des_ifH GET; ss; des; subst; ss; eauto.
    inv GET. eauto.
  Qed.

End MemoryReorder.