Library seplog_lemmas

This file contains a set of lemmas for defining "sep auto", which is a tactic defined in 'seplog_tactics.v' for proving entailments of relational assertions.

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.
Require Import simulation.
Require Import inferules.
Require Import baseTac.

Set Implicit Arguments.

Ltac destruct_s s := destruct s as [[[[[[]]][[]]]]].

Theorem astar_comm :
  forall P Q,
    P ** Q ==> Q ** P.

Theorem atrue_intro :
  forall s, s |= Atrue.

Theorem astar_mono :
  forall P Q P´ Q´,
    P ==> P´ ->
    Q ==> Q´ ->
    P ** Q ==> P´ ** Q´.

Theorem aconj_mono :
  forall P Q P´ Q´,
    P ==> P´ ->
    Q ==> Q´ ->
    (P //\\ Q ==> P´ //\\ Q´).

Theorem adisj_mono :
  forall P Q P´ Q´,
    P ==> P´ ->
    Q ==> Q´ ->
    (P \\// Q ==> P´ \\// Q´).

Theorem astar_l_aemp_intro :
  forall P, P ==> Aemp ** P.

Theorem astar_r_aemp_intro :
  forall P, P ==> P ** Aemp.

Theorem astar_l_aemp_elim :
  forall P, Aemp ** P ==> P.

Theorem astar_r_aemp_elim :
  forall P, P ** Aemp ==> P.

Theorem astar_assoc_intro :
  forall P Q R, P ** Q ** R ==> (P ** Q ) ** R.

Theorem astar_assoc_elim :
  forall P Q R, (P ** Q ) ** R ==> P ** Q ** R.

Theorem apure_intro :
  forall s (P:Prop),
    s |= Aemp -> P -> s |= [| P |].

Theorem apure_elim :
  forall s P,
    s |= [| P |] -> P /\ s |= Aemp.

Theorem astar_2atrue_intro :
  Atrue ==> Atrue ** Atrue.

Theorem astar_2atrue_elim :
  Atrue ** Atrue ==> Atrue.

Theorem astar_l_afalse_elim :
  forall s P,
    s |= Afalse ** P -> s |= Afalse.

Theorem astar_l_afalse_intro :
  forall s P,
    s |= Afalse -> s |= Afalse ** P.

Theorem astar_l_apure_elim :
  forall s (P:Prop) (Q:asrt),
    s |= [| P |] ** Q -> P /\ s |= Q.

Theorem astar_l_apure_intro :
  forall s (P:Prop) Q,
    s |= Q -> P -> s |= [| P |] ** Q.

Theorem aexists_elim :
  forall s {t:Type} (P:t->asrt),
    (s |= (EX x, P x )) -> (exists x, s |= (P x)).

Theorem aexists_intro :
  forall s {t:Type} (P:t->asrt),
    (exists x, s |= (P x)) -> (s |= (EX x, P x )).

Theorem astar_r_aexists_intro :
  forall {t:Type} P (Q:t->asrt),
    EX x, (P ** Q x ) ==> P ** EX x, Q x.

Theorem astar_l_aexists_intro :
  forall {t:Type} (P:t->asrt) Q,
    EX x, (P x ** Q ) ==> (EX x, P x ) ** Q.

Theorem astar_r_aexists_elim :
  forall {t:Type} P (Q:t->asrt),
    P ** (EX x, Q x ) ==> EX x, (P ** Q x ).

Theorem astar_l_aexists_elim :
  forall {t:Type} (P:t->asrt) Q,
    (EX x, P x ) ** Q ==> EX x, (P x ** Q ).

Theorem aconj_r_aexists_intro :
  forall {t:Type} P (Q:t->asrt),
    EX x, (P //\\ Q x ) ==> P //\\ EX x, Q x.

Theorem aconj_l_aexists_intro :
  forall {t:Type} (P:t->asrt) Q,
    EX x, (P x //\\ Q ) ==> (EX x, P x ) //\\ Q.

Theorem aconj_r_aexists_elim :
  forall {t:Type} P (Q:t->asrt),
    P //\\ (EX x, Q x ) ==> EX x, (P //\\ Q x ).

Theorem aconj_l_aexists_elim :
  forall {t:Type} (P:t->asrt) Q,
    (EX x, P x ) //\\ Q ==> EX x, (P x //\\ Q ).

Theorem adisj_r_aexists_intro :
  forall {t:Type} P (Q:t->asrt),
    EX x, (P \\// Q x ) ==> P \\// EX x, Q x.

Theorem adisj_l_aexists_intro :
  forall {t:Type} (P:t->asrt) Q,
    EX x, (P x \\// Q ) ==> (EX x, P x ) \\// Q.

Theorem adisj_r_aexists_elim :
  forall {t:Type} P (Q:t->asrt),
    (exists (x:t ), x = x) ->
    P \\// (EX x, Q x ) ==> EX x, (P \\// Q x ).

Theorem adisj_l_aexists_elim :
  forall {t:Type} (P:t->asrt) Q,
    (exists (x:t ), x = x) ->
    (EX x, P x ) \\// Q ==> EX x, (P x \\// Q ).

Theorem aexists_prop :
  forall {t:Type} (P Q:t->asrt) s,
    (forall x, s |= P x -> s |= Q x) ->
    (s |= EX y, P y -> s |= EX z, Q z).

Theorem aconj_elim :
  forall P Q s,
    (s |= P //\\ Q) -> s |= P /\ s |= Q.

Theorem aconj_intro :
  forall P Q s,
    s |= P -> s |= Q -> s |= P //\\ Q.

Theorem adisj_elim :
  forall P Q s,
    (s |= P \\// Q) -> s |= P \/ s |= Q.

Theorem adisj_intro :
  forall P Q s,
    s |= P \/ s |= Q -> s |= P \\// Q.

Theorem astar_r_aconj_elim :
  forall P Q Q´,
    P ** (Q //\\ Q´) ==> P ** Q //\\ P ** Q´.

Theorem astar_l_aconj_elim :
  forall P P´ Q,
    (P //\\ P´) ** Q ==> P ** Q //\\ P´ ** Q.

Lemma aconj_l_astar_l_apure_elim :
  forall P Q R,
    ([| P |] ** Q ) //\\ R ==> [| P |] ** (Q //\\ R ).

Lemma aconj_l_apure_elim :
  forall P Q,
    [| P |] //\\ Q ==> [| P |] ** (Aemp //\\ Q ).

Lemma aconj_r_astar_l_apure_elim :
  forall P Q R,
    P //\\ ([| Q |] ** R ) ==> [| Q |] ** (P //\\ R ).

Lemma aconj_r_apure_elim :
  forall P Q,
    P //\\ [| Q |] ==> [| Q |] ** (P //\\ Aemp ).

Lemma aconj_l_astar_l_apure_intro :
  forall P Q R,
    [| P |] ** (Q //\\ R ) ==> ([| P |] ** Q ) //\\ R.

Lemma aconj_l_apure_intro :
  forall P Q,
    [| P |] ** (Aemp //\\ Q ) ==> [| P |] //\\ Q.

Lemma aconj_r_astar_l_apure_intro :
  forall P Q R,
    [| Q |] ** (P //\\ R ) ==> P //\\ ([| Q |] ** R ).

Lemma aconj_r_apure_intro :
  forall P Q,
    [| Q |] ** (P //\\ Aemp ) ==> P //\\ [| Q |].

Theorem aconj_2aemp_elim :
  Aemp //\\ Aemp ==> Aemp.

Theorem aconj_2aemp_intro :
  Aemp ==> Aemp //\\ Aemp.

Theorem astar_prop :
  forall s P Q,
    s |= P ** Q ->
    exists s1 s2, (s1 |= P /\ s2 |= Q ).

Theorem astar_l_aie_intro :
  forall s i Q,
    s |= Q -> getie (gettaskst s) = i -> s |= Aie i ** Q.

Theorem astar_l_aie_elim :
  forall s i Q,
    s |= Aie i ** Q ->
    getie (gettaskst s) = i /\ s |= Q.

Theorem aie_intro :
  forall s i,
    s |= Aemp -> getie (gettaskst s) = i -> s |= Aie i.

Theorem aie_elim :
  forall s i,
    s |= Aie i -> getie (gettaskst s) = i /\ s |= Aemp.

Theorem astar_l_ais_intro :
  forall s i Q,
    s |= Q -> getis (gettaskst s) = i -> s |= Ais i ** Q.

Theorem astar_l_ais_elim :
  forall s i Q,
    s |= Ais i ** Q ->
    getis (gettaskst s) = i /\ s |= Q.

Theorem ais_intro :
  forall s i,
    s |= Aemp -> getis (gettaskst s) = i -> s |= Ais i.

Theorem ais_elim :
  forall s i,
    s |= Ais i -> getis (gettaskst s) = i /\ s |= Aemp.

Theorem astar_l_aisr_intro :
  forall s i Q,
    s |= Q -> getisr (gettaskst s) = i -> s |= Aisr i ** Q.

Theorem astar_l_aisr_elim :
  forall s i Q,
    s |= Aisr i ** Q ->
    getisr (gettaskst s) = i /\ s |= Q.

Theorem aisr_intro :
  forall s i,
    s |= Aemp -> getisr (gettaskst s) = i -> s |= Aisr i.

Theorem aisr_elim :
  forall s i,
    s |= Aisr i -> getisr (gettaskst s) = i /\ s |= Aemp.

Theorem astar_l_acs_intro :
  forall s i Q,
    s |= Q -> getcs (gettaskst s) = i -> s |= Acs i ** Q.

Theorem astar_l_acs_elim :
  forall s i Q,
    s |= Acs i ** Q ->
    getcs (gettaskst s) = i /\ s |= Q.

Theorem acs_intro :
  forall s i,
    s |= Aemp -> getcs (gettaskst s) = i -> s |= Acs i.

Theorem acs_elim :
  forall s i,
    s |= Acs i -> getcs (gettaskst s) = i /\ s |= Aemp.

Theorem astar_l_atopis_intro :
  forall s i Q,
    s |= Q -> gettopis (getis (gettaskst s)) = i -> s |= ATopis i ** Q.

Theorem astar_l_atopis_elim :
  forall s i Q,
    s |= ATopis i ** Q ->
    gettopis (getis (gettaskst s)) = i /\ s |= Q.

Theorem atopis_intro :
  forall s i,
    s |= Aemp -> gettopis (getis (gettaskst s)) = i -> s |= ATopis i.

Theorem atopis_elim :
  forall s i,
    s |= ATopis i -> gettopis (getis (gettaskst s)) = i /\ s |= Aemp.

Theorem astar_l_adomlenv_intro :
  forall s d Q,
    s |= Q -> eq_dom_env (getlenv s) d -> s |= A_dom_lenv d ** Q.

Theorem astar_l_adomlenv_elim :
  forall s d Q,
    s |= A_dom_lenv d ** Q ->
    eq_dom_env (getlenv s) d /\ s |= Q.

Theorem adomlenv_intro :
  forall s d,
    s |= Aemp -> eq_dom_env (getlenv s) d -> s |= A_dom_lenv d.

Theorem adomlenv_elim :
  forall s d,
    s |= A_dom_lenv d -> eq_dom_env (getlenv s) d /\ s |= Aemp.

Theorem astar_l_anotinlenv_intro :
  forall s x Q,
    s |= Q -> ~ EnvMod.indom (getlenv s) x -> s |= A_notin_lenv x ** Q.

Theorem astar_l_anotinlenv_elim :
  forall s x Q,
    s |= A_notin_lenv x ** Q ->
    ~ EnvMod.indom (getlenv s) x /\ s |= Q.

Theorem anotinlenv_intro :
  forall s x,
    s |= Aemp -> ~ EnvMod.indom (getlenv s) x -> s |= A_notin_lenv x.

Theorem anotinlenv_elim :
  forall s x,
    s |= A_notin_lenv x -> ~ EnvMod.indom (getlenv s) x /\ s |= Aemp.

Theorem astar_l_alvarenv_intro :
  forall s x t l Q,
    s |= Q -> (snd l = 0%Z /\ EnvMod.get (getlenv s) x = Some (fst l ,t )) -> s |= Alvarenv x t l ** Q.

Theorem astar_l_alvarenv_elim :
  forall s x t l Q,
    s |= Alvarenv x t l ** Q ->
    (snd l = 0%Z /\ EnvMod.get (getlenv s) x = Some (fst l ,t )) /\ s |= Q.

Theorem alvarenv_intro :
  forall s x t l,
    s |= Aemp -> (snd l = 0%Z /\ EnvMod.get (getlenv s) x = Some (fst l ,t )) -> s |= Alvarenv x t l.

Theorem alvarenv_elim :
  forall s x t l,
    s |= Alvarenv x t l -> (snd l = 0%Z /\ EnvMod.get (getlenv s) x = Some (fst l ,t )) /\ s |= Aemp.

Theorem astar_l_agvarenv_intro :
  forall s x t l Q,
    s |= Q -> (snd l = 0%Z /\ EnvMod.get (getgenv s) x = Some (fst l , t )) -> s |= Agvarenv x t l ** Q.

Theorem astar_l_agvarenv_elim :
  forall s x t l Q,
    s |= Agvarenv x t l ** Q ->
    (snd l = 0%Z /\ EnvMod.get (getgenv s) x = Some (fst l , t )) /\ s |= Q.

Theorem agvarenv_intro :
  forall s x t l,
    s |= Aemp -> (snd l = 0%Z /\ EnvMod.get (getgenv s) x = Some (fst l ,t )) -> s |= Agvarenv x t l.

Theorem agvarenv_elim :
  forall s x t l,
    s |= Agvarenv x t l -> (snd l = 0%Z /\ EnvMod.get (getgenv s) x = Some (fst l ,t )) /\ s |= Aemp.

Theorem astar_l_aop´_intro :
  forall s aop Q,
    s |= Q -> getabsop s = aop -> s |= <|| aop ||> ** Q.

Theorem astar_l_aop´_elim :
  forall s aop Q,
    s |= <|| aop ||> ** Q ->
    getabsop s = aop /\ s |= Q.

Theorem aop´_intro :
  forall s aop,
    s |= Aemp -> getabsop s = aop -> s |= <|| aop ||>.

Theorem aop´_elim :
  forall s aop,
    s |= <|| aop ||> -> getabsop s = aop /\ s |= Aemp.
Theorem change_aop_rule:
  forall o O aop aop´ P,
    (o ,O ,aop ) |= P -> can_change_aop P -> (o ,O ,aop´) |= P.

Fixpoint can_be_cancelled (p : asrt) : bool :=
  match p with
    | Astar p1 p2 => andb (can_be_cancelled p1) (can_be_cancelled p2)
    | Aemp => true
    | Amapsto l t v => true
    | Amapstolsval l t vl => true
    | Aabsdata id data => true
    | _ => false
  end.

Theorem cancellation_rule :
  forall A B C G E isr aux aop G´ E´ isr´ aux´ aop´,
    (forall m O, (G ,E ,m ,isr ,aux ,O ,aop ) |= B -> (G´,E´,m ,isr´,aux´,O ,aop´) |= C) ->
    can_be_cancelled A = true ->
    (forall m O, (G ,E ,m ,isr ,aux ,O ,aop ) |= A ** B -> (G´,E´,m ,isr´,aux´,O ,aop´) |= A ** C).

Lemma absdata_elim :
  forall s O gamma x y P,
    (s , O , gamma ) |= Aabsdata x y ** P ->
    OSAbstMod.get O x = Some y.

Lemma absdata_elim´ :
  forall s O O´ gamma x y P,
    (s , O , gamma ) |= Aabsdata x y ** P ->
    OSAbstMod.disj O O´ ->
    OSAbstMod.get (OSAbstMod.merge O O´) x = Some y.

Lemma absdata_elim´´ : forall (s : taskst) (O O´ O´´ : OSAbstMod.map)
  (gamma : absop) (x x´: absdataid) (y y´ y´´ : absdata) (P : asrt),
        O´´ = OSAbstMod.set O x y´´ ->
       (s , O , gamma ) |= Aabsdata x y ** Aabsdata x´ y´ ** P ->
       OSAbstMod.disj O O´ -> OSAbstMod.get (OSAbstMod.merge O´´ O´) x´ = Some y´ /\
                              OSAbstMod.disj O´´ O´.