Library lemmasforseplog

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 [ [ [ [ [ [ ] ] ] ] ] ];
  simpl in *.

Lemma TcbMod_disj_merge_eq :
  forall ta tb,
    TcbMod.disj ta tb ->
    TcbMod.merge ta tb = TcbMod.merge tb ta.

Lemma SemMod_disj_merge_eq :
  forall ta tb,
    SemMod.disj ta tb ->
    SemMod.merge ta tb = SemMod.merge tb ta.

Lemma MsgqMod_disj_merge_eq :
  forall ta tb,
    MsgqMod.disj ta tb ->
    MsgqMod.merge ta tb = MsgqMod.merge tb ta.

Lemma TcbMod_merge_emp_l :
  forall m,
    TcbMod.merge TcbMod.emp m = m.

Lemma SemMod_merge_emp_l :
  forall m,
    SemMod.merge SemMod.emp m = m.

Lemma MsgqMod_merge_emp_l :
  forall m,
    MsgqMod.merge MsgqMod.emp m = m.

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

Theorem TrueI : forall s, s |= Atrue.

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

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

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

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

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

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

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

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

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

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

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

Theorem Star2TrueI :
  Atrue ==> Atrue ** Atrue.

Theorem Star2TrueE :
  Atrue ** Atrue ==> Atrue.

Theorem Star2PureI :
  forall P Q:Prop,
    [| P /\ Q |] ==> [| P |] ** [| Q |].

Theorem Star2PureE :
  forall P Q:Prop,
    [| P |] ** [| Q |] ==> [| P /\ Q |].

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

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

Theorem StarTrueI :
  forall P, P ==> P ** Atrue.

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

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

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

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

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

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

Theorem Star2PureLE :
  forall P Q R,
    [| P |] ** [| Q |] ** R ==> [| P /\ Q |] ** R.

Theorem Star2PureRE : forall P Q R,
  P ** [| Q |] ** [| R |] ==> P ** [| Q /\ R |].

Theorem Star2PureLI :
  forall P Q R,
    [| P /\ Q |] ** R ==> [| P |] ** [| Q |] ** R.

Theorem Star2PureRI :
  forall P Q R,
    P ** [| Q /\ R |] ==> P ** [| Q |] ** [| R |].

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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