Library simplrulesound

Require Import include.
Require Import memory.
Require Import memdata.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import simulation.
Require Import lemmasforseplog.
Require Import inferules.
Require Import tacticsforseplog.
Require Import includeLib.
Require Import baseTac.
Require Import auxdef.

Lemma pure_split_rule_sound:
  forall P (p:Prop) Spec sd I r ri Q s,
    (
      p ->
      RuleSem Spec sd I r ri P s Q
    ) ->
    RuleSem Spec sd I r ri (P ** [| p |]) s Q.

Lemma ex_intro_rule_sound:
  forall Spec sd I r ri {tp:Type} q s p,
    (forall v´, RuleSem Spec sd I r ri (p v´) s q) ->
    RuleSem Spec sd I r ri (EX v : tp, p v) s q.

Lemma disj_rule_sound:
  forall Spec sd I r ri p1 p2 q s,
    RuleSem Spec sd I r ri p1 s q ->
    RuleSem Spec sd I r ri p2 s q ->
    RuleSem Spec sd I r ri (p1\\//p2) s q.

Lemma pfalse_rule_sound: forall Spec sd I r ri q s,
                    RuleSem Spec sd I r
                        ri Afalse s q .

Lemma genv_introret_rule_sound_aux : forall (Spec : funspec) sd (I : Inv) (r : retasrt)
     (ri : asrt) (q : asrt) (G : env) (C : code)
     (o : taskst) (aop : absop) (O : osabst),
   G = get_genv (get_smem o) ->
   ( {[Spec, sd, I, r, ri, lift q ]} ||- (C, o) <_msim (aop, O )) ->
    {[Spec, sd, I, (fun v => (Agenv G//\\ r v)), ri, lift q ]} ||- (C, o) <_msim (aop,
   O ).

Lemma genv_introret_rule_sound : forall Spec sd I r ri p q s G,
                               RuleSem Spec sd I r ri p s q ->
                              RuleSem Spec sd I (fun v => (Agenv G //\\ r v)) ri
                        (Agenv G //\\ p) s q .

Lemma genv_introexint_rule_sound_aux :
  forall (Spec : funspec) sd (I : Inv) (r : retasrt)
     (ri : asrt) (q : asrt) (G : env) (C : code)
     (o : taskst) (aop : absop) (O : osabst),
   G = get_genv (get_smem o) ->
   ( {[Spec, sd, I, r, ri, lift q ]} ||- (C, o) <_msim (aop, O )) ->
    {[Spec, sd, I, r, Agenv G//\\ ri, lift q ]} ||- (C, o) <_msim (aop,
   O ).

Lemma genv_introexint_rule_sound : forall Spec sd I r ri p q s G,
                               RuleSem Spec sd I r ri p s q ->
                              RuleSem Spec sd I r (Agenv G //\\ ri)
                        (Agenv G //\\ p) s q .

Lemma sim_retspec_intro :forall p sd C gamma o O I q ,
           ({[p, sd, I, arfalse , Afalse, q]} ||- (C, o) <_msim (gamma, O)) ->
           forall r ri , ({[p, sd, I,r , ri, q]} ||- (C, o) <_msim (gamma, O)) .

Lemma retspec_intro_rule_sound : forall Spec sd I ri r p q s ,
                RuleSem Spec sd I arfalse Afalse p s q ->
                  RuleSem Spec sd I r ri p s q .