Library contLib

Require Import Coqlib.
Require Import memory.
Require Import Integers.
Require Import List.
Require Import ZArith.
Require Import language.
Require Import opsem.
Require Import LibTactics.
Require Import assertion.


Lemma addstmts_eq_addcont : forall s ks ,
      AddStmtToKs s ks = AddKsToTail (kseq s kstop) ks.

Lemma addstmts_same_remove : forall s ks ks´, AddStmtToKs s ks = AddStmtToKs s ks´ -> ks =ks´.

Open Local Scope nat_scope.
Lemma length_addcont : forall ks ks´, len_stmtcont (ks##ks´) = (len_stmtcont ks) + (len_stmtcont ks´).

Lemma addcont_same_remove : forall ks ks´ ks0, ks##ks0 = ks´##ks0 -> ks = ks´.

Lemma callcont_some_addstmts : forall ks s k ,
      callcont ks = Some k -> callcont (AddStmtToKs s ks)
= Some (AddStmtToKs s k) .

Lemma callcont_some_addstmts_rev : forall s ks ks´, callcont (AddStmtToKs s ks) = Some (AddStmtToKs s ks´) ->
 callcont ks = Some ks´.

Lemma callcont_some_addcont : forall ks ks1 k ,
      callcont ks = Some k -> callcont (AddKsToTail ks1 ks)
= Some (AddKsToTail ks1 k) .

Lemma callcont_none_addstmts : forall s ks , callcont (AddStmtToKs s ks) = None -> callcont ks = None.

Lemma callcont_none_addstmts_rev : forall ks s, callcont ks = None -> callcont (AddStmtToKs s ks) = None.

Lemma callcont_none :
  forall ks f s E ks´,
    callcont (ks ## kcall f s E kstop) = None ->
      callcont (ks ## kcall f s E ks´) = None.

Lemma callcont_stmts_exist : forall s ks f s0 le ks´,
           callcont (AddStmtToKs s ks) = Some (kcall f s0 le ks´)->
                    exists ks´´, kcall f s0 le ks´ = AddStmtToKs s (kcall f s0 le ks´´).

Lemma callcont_addkcall_imply_callcont_addkcall_exist :
  forall ks f s E ks´ f´ s´ E´ ks´´ ks1,
    callcont (ks ## kcall f s E ks´) = Some (kcall f´ s´ E´ ks´´) ->
      exists ks1´ , callcont (ks ## kcall f s E ks1 ) = Some (kcall f´ s´ E´ ks1´).

Lemma callcont_addkcall_imply_addcont_exist :
  forall ks f s E ks´ f´ s´ E´ ks´´,
    callcont ks <> None ->
      callcont (ks ## kcall f s E ks´) = Some (kcall f´ s´ E´ ks´´) ->
        exists ks´´´, ks´´ = ks´´´ ## kcall f s E ks´.

Lemma callcont_addkcall_imply_callcont_addkcall :
  forall ks f1 s1 E1 ks1 f2 s2 E2 ks2 f s E ks´,
    callcont (ks ## kcall f1 s1 E1 ks1 ) = Some (kcall f s E (ks´ ## kcall f1 s1 E1 ks1)) ->
      callcont (ks ## kcall f2 s2 E2 ks2 ) = Some (kcall f s E (ks´ ## kcall f2 s2 E2 ks2)).

Lemma stmtcont_eq_length :
  forall (s1 s2 : stmtcont),
    s1 = s2 -> len_stmtcont s1 = len_stmtcont s2.

Lemma callcont_ks_kstop :
  forall ks f s E ks´,
    callcont (ks ## kcall f s E ks´) = Some (kcall f s E ks´) ->
    callcont (ks ## kcall f s E kstop) = Some (kcall f s E kstop).

 Lemma call_int_cont_none : forall ks f s E ks1 ,callcont (ks ## kcall f s E ks1) <> None -> callcont ks = None -> callcont (ks ## kcall f s E ks1) = Some (kcall f s E ks1).

Lemma callcont_kseq_kstop : forall ks e s f s0 le´ ks´0,
  callcont (ks ## kseq (swhile e s) kstop) = Some (kcall f s0 le´ ks´0) ->
    exists ks´,callcont ks = Some (kcall f s0 le´ ks´).

Lemma callcont_addcont_none : forall ks ks´, callcont (ks ## ks´) = None ->
                                  callcont ks = None.

Lemma callcont_nont_addkseq_kstop : forall ks s, callcont ks = None -> callcont (ks ## kseq s kstop) = None.

Lemma intcont_some_addcont : forall ks ks1 k ,
      intcont ks = Some k -> intcont (AddKsToTail ks1 ks)
= Some (AddKsToTail ks1 k) .

Lemma intcont_some_addstmts : forall ks s k ,
      intcont ks = Some k -> intcont (AddStmtToKs s ks)
= Some (AddStmtToKs s k) .

Lemma intcont_none_addstmts : forall s ks , intcont (AddStmtToKs s ks) = None -> intcont ks = None.

Lemma intcont_none_addstmsts_rev : forall s ks , intcont ks = None -> intcont (AddStmtToKs s ks) = None.

Lemma intcont_none_addcont : forall s ks , intcont (ks##s) = None -> intcont ks = None.

Lemma intcont_nont_addstmt_prev : forall ks s, intcont ks = None -> intcont (ks ## kseq s kstop) = None.

Lemma intcont_none : forall ks f s E ks´,
           intcont (ks ## kcall f s E kstop) = None ->
            intcont (ks ## kcall f s E ks´) = None.

Lemma intcont_some_kcall_none : forall ks f s E ks1,
                  intcont (ks ## kcall f s E ks1) <> None ->
                                     intcont ks <> None.

Lemma intcont_intcont_none: forall ks f s E ks´,
              intcont ks = None -> intcont (ks ## kcall f s E ks´) = None.

Lemma intcont_addkcall_exist : forall ks f s E ks´ c0 ke0 le0 ks´0 ,
  intcont (ks ## kcall f s E ks´) = Some (kint c0 ke0 le0 ks´0) ->
      exists ks´´, ks´0 = ks´´ ## kcall f s E ks´.

Lemma intcont_addkcall_imply_intcont : forall ks f s E ks´ c0 ke0 le0 ks1 ,
  intcont (ks ## kcall f s E ks1) = Some (kint c0 ke0 le0 (ks´ ## kcall f s E ks1)) ->
    intcont ks = Some (kint c0 ke0 le0 ks´).

Lemma intcont_addkcall_imply_intcont_addkcall_exist :
  forall ks f1 s1 E1 ks1 f2 s2 E2 ks2 c ke E ks´,
    intcont (ks ## kcall f1 s1 E1 ks1 ) = Some (kint c ke E ks´) ->
      exists ks´´,intcont (ks ## kcall f2 s2 E2 ks2 ) = Some (kint c ke E ks´´).

Lemma callcont_none_intcont_some_imply_callcont_addcont_none : forall ks ks´ , callcont ks = None -> intcont ks <> None -> callcont (ks ## ks´) = None.

Lemma callcont_some : forall ks0 f s E´, callcont ks0 = None -> intcont ks0 = None -> callcont (ks0 ## kcall f s E´ kstop) = Some
  (kcall f s E´ kstop).

Lemma callcont_kcall_neqnone : forall ks f s E , ~(callcont (ks ## kcall f s E kstop) = None /\ intcont (ks ## kcall f s E kstop) = None).

Lemma callcont_not_none : forall ks f s E ks´, intcont (ks ## kcall f s E ks´) = None-> callcont (ks ## kcall f s E ks´) <> None.

Lemma callcont_not_none´ : forall ks f s E ks´ ks0 , ks ## kcall f s E ks´ = kret ks0 -> intcont ks0 = None -> callcont ks0 <> None.

Lemma call_int_none_call: forall ks f s E ks´,
                             callcont ks =None -> intcont ks = None ->
                             callcont (ks ## kcall f s E ks´) = Some (kcall f s E ks´).

Lemma callcont_some_eq : forall ks1 f s E ks ,
                  callcont ks1 = None ->
                  intcont ks1 = None ->
               callcont (ks1 ## kcall f s E ks) = Some (kcall f s E ks) .

 Lemma callcont_intcont_kcall_none : forall ks f s E ,
              callcont ks = None -> intcont (ks ## kcall f s E kstop) = None -> intcont ks = None.

Lemma intcont_calcont_not_none: forall ks f s E ks´,
              intcont ks = None -> callcont (ks ## kcall f s E ks´) <> None.

Lemma ks_puls_kcall_neq : forall ks ks´ f s E, ks ## kcall f s E ks´ <> kstop.

Lemma add_stmt_not_kstop : forall s ks, AddStmtToKs s ks <> kstop.

Lemma addstmt_kret_exist : forall s ks ks´ , AddStmtToKs s ks = kret ks´ ->
                   exists ks´´, ks = kret ks´´.

Lemma kseq_not_kstop : forall ks e s, ks ## kseq (swhile e s) kstop <> kstop.

Lemma kseq_eq_addstmt: forall ks s , ks ## kseq s kstop = AddStmtToKs s ks.

Lemma kseq_addcont : forall ks ks´ ks´´,
  kseq ks (ks´ ## ks´´) = (kseq ks ks´) ## ks´´.

Lemma kcall_addcont : forall f s E ks ks´,
  kcall f s E (ks ## ks´) = (kcall f s E ks) ## ks´.

Lemma kint_addcont : forall c ke le ks ks´,
  kint c ke le (ks ## ks´) = (kint c ke le ks) ## ks´.

Lemma kassignr_addcont : forall e t ks ks´,
  kassignr e t (ks ## ks´) = (kassignr e t ks )## ks´.

Lemma kassignl_addcont : forall v t ks ks´,
  kassignl v t (ks ## ks´) = (kassignl v t ks )## ks´.

Lemma kfuneval_addcont : forall f vl tl el ks ks´,
  kfuneval f vl tl el (ks ## ks´) = (kfuneval f vl tl el ks) ## ks´.

Lemma kif_addcont : forall s1 s2 ks ks´,
  kif s1 s2 (ks ## ks´) = (kif s1 s2 ks) ## ks´.

Lemma kwhile_addcont : forall e s ks ks´,
  kwhile e s (ks ## ks´) = (kwhile e s ks) ## ks´.

Lemma kret_addcont : forall ks ks´,
  kret (ks ## ks´) = (kret ks) ## ks´.

Ltac rewrite_addcont :=
  try rewrite kseq_addcont;
  try rewrite kcall_addcont;
  try rewrite kint_addcont;
  try rewrite kassignr_addcont;
  try rewrite kassignl_addcont;
  try rewrite kfuneval_addcont;
  try rewrite kif_addcont;
  try rewrite kwhile_addcont;
  try rewrite kret_addcont.