sts.v 1.89 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10
From iris.proofmode Require Import coq_tactics pviewshifts.
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export sts.
Import uPred.

Section sts.
Context `{stsG Λ Σ sts} (φ : sts.state sts  iPropG Λ Σ).
Implicit Types P Q : iPropG Λ Σ.

Lemma tac_sts_fsa {A} (fsa : FSA Λ _ A) fsaV Δ E N i γ S T Q Φ :
11
  IsFSA Q E fsa fsaV Φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13
  fsaV 
  envs_lookup i Δ = Some (false, sts_ownS γ S T) 
14
  (of_envs Δ  sts_ctx γ N φ)  nclose N  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16
  ( s, s  S   Δ',
    envs_simple_replace i false (Esnoc Enil i ( φ s)) Δ = Some Δ' 
17 18
    (Δ'  fsa (E  nclose N) (λ a,  s' T',
       sts.steps (s, T) (s', T')   φ s'  (sts_own γ s' T' - Φ a)))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20
  Δ  Q.
Proof.
21
  intros ????? HΔ'. rewrite (is_fsa Q) -(sts_fsaS φ fsa) //.
22
  rewrite // -always_and_sep_l. apply and_intro; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24
  rewrite envs_lookup_sound //; simpl; apply sep_mono_r.
  apply forall_intro=>s; apply wand_intro_l.
25
  rewrite -assoc; apply pure_elim_sep_l=> Hs.
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27 28 29 30 31 32 33 34 35 36 37 38
  destruct (HΔ' s) as (Δ'&?&?); clear HΔ'; auto.
  rewrite envs_simple_replace_sound' //; simpl.
  by rewrite right_id wand_elim_r.
Qed.
End sts.

Tactic Notation "iSts" constr(H) "as"
    simple_intropattern(s) simple_intropattern(Hs) :=
  match type of H with
  | string => eapply tac_sts_fsa with _ _ _ _ _ _ H _ _ _ _
  | gname => eapply tac_sts_fsa with _ _ _ _ _ _ _ H _ _ _
  | _ => fail "iSts:" H "not a string or gname"
  end;
39
    [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41 42 43 44 45 46
     apply _ || fail "iSts: cannot viewshift in goal" P
    |try fast_done (* atomic *)
    |iAssumptionCore || fail "iSts:" H "not found"
    |iAssumption || fail "iSts: invariant not found"
    |done || eauto with ndisj (* [eauto with ndisj] is slow *)
    |intros s Hs; eexists; split; [env_cbv; reflexivity|simpl]].
Tactic Notation "iSts" constr(H) "as" simple_intropattern(s) := iSts H as s ?.