Require Arith.
Require Omega.
Require machine.

Section lemmas.


Lemma apart_extend_right : 
  (e1,sz1,e2,sz2:nat)(sz2':nat)
  (apart e1 sz1 e2 sz2) ->
  (le sz2' sz2) ->
  (apart e1 sz1 e2 sz2').
Proof.
Unfold apart.
Intros.
Omega.
Qed.


Lemma apart_shift_right : 
  (e1,sz1,e2,sz2:nat)(x,sz2':nat)
  (apart e1 sz1 e2 sz2) ->
  (le (plus x sz2') sz2) ->
  (lt (0) sz2') ->
  (apart e1 sz1 (plus e2 x) sz2').
Proof.
Unfold apart.
Intros.
Omega.
Qed.


Lemma apart_move_both : 
  (e1,sz1,e2,sz2:nat)(a:nat)
  (apart e1 sz1 e2 sz2) ->
  (apart (plus a e1) sz1 (plus a e2) sz2).
Proof.
Unfold apart.
Intros.
Omega.
Qed.



Lemma apart_sym : (e1:exp; n1:nat; e2:exp; n2:nat)
  (apart e1 n1 e2 n2) ->
  (apart e2 n2 e1 n1).
Proof.
Unfold apart.
Intros.
Omega.
Qed.

Lemma allocate_addr_apart : (s:state)
  (n:nat)
  (e1:exp; SZ1:nat)  
  (lt (0) n) ->
  (lt (0) SZ1) ->
  (addr SZ1 (mem_of s) e1) ->
  (apart e1 SZ1 (rega_of (allocate n s)) n). 
Proof.
Intros.
Unfold apart.
LetTac a := (rega_of (allocate n s)).
Decompose Sum (lt_eq_lt_dec e1 a).
  Left.
  Split; Auto.  
  LetTac o := (minus a e1).
  Assert (not (le (plus o (1)) SZ1)).
    Intro.    
    Apply allocate_new with n1:=(1) o:=(0) n2:=n
        s:=s; Auto with arith.
      Replace (plus (0) (rega_of (allocate n s)))
          with (plus o e1).
        EApply addr_closed; EAuto.

        Unfold o a.
        Unfold a in a1.
        Omega.

      Unfold o a in H2; Unfold a in a1; Unfold a.
      Omega.

  ElimType False; Apply allocate_new with s:=s 
      n1:=(1) o:=(0) n2:=n;
      EAuto.
    EApply addr_closed.
      Rewrite b in H1; EApply H1.    
  
      Omega.

  Right.
  Split; Auto.  
  LetTac o := (minus e1 a).
  Assert (not (le (plus o (1)) n)).
    Intro.    
    Apply allocate_new with n1:=(1) o:=o n2:=n
        s:=s; Auto with arith.
       Omega.
   
      Replace (plus o (rega_of (allocate n s)))
          with (plus (0) e1).
        EApply addr_closed; EAuto.

        Unfold o a.
        Unfold a in b.
        Omega.

      Unfold o a in H2; Unfold a in b; Unfold a.
      Omega.
Qed.

Lemma allocate_addr_apart_extend : (s:state)
  (n:nat)
  (e1:exp; SZ1:nat; SZ2:nat)  
  (lt (0) n) ->
  (lt (0) SZ1) ->
  (le SZ2 n) ->
  (addr SZ1 (mem_of s) e1) ->
  (apart e1 SZ1 (rega_of (allocate n s)) SZ2). 
Proof.
Intros.
EApply apart_extend_right; EAuto.
EApply allocate_addr_apart; EAuto.
Qed.

End lemmas.

Tactic Definition Discriminate_something :=
  Match Context With [ H: ? = ? |- ? ]
    -> Discriminate H.
Tactic Definition Discriminate_some3 :=
  Match Context With [ H: (? = ?)\/(? = ?)\/(? = ?) |- ? ]
    -> Decompose [or] H; Discriminate_something.