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

Section invariants.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Λ Σ.

Lemma tac_inv_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
12
  IsFSA Q E fsa fsaV Φ 
13
  fsaV  nclose N  E  (of_envs Δ  inv N P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
14
  envs_app false (Esnoc Enil i ( P)) Δ = Some Δ' 
15
  (Δ'  fsa (E  nclose N) (λ a,  P  Φ a))  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
Proof.
17
  intros ????? HΔ'. rewrite (is_fsa Q) -(inv_fsa fsa _ _ P) //.
18
  rewrite // -always_and_sep_l. apply and_intro; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20 21 22
  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
Qed.

Lemma tac_inv_fsa_timeless {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
23
  IsFSA Q E fsa fsaV Φ 
24
  fsaV  nclose N  E  (of_envs Δ  inv N P)  TimelessP P 
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
26
  (Δ'  fsa (E  nclose N) (λ a, P  Φ a))  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Proof.
28
  intros ?????? HΔ'. rewrite (is_fsa Q) -(inv_fsa fsa _ _ P) //.
29 30 31 32 33
  rewrite // -always_and_sep_l. apply and_intro, wand_intro_l; first done.
  trans (|={E  N}=> P  Δ)%I; first by rewrite pvs_timeless pvs_frame_r.
  apply (fsa_strip_pvs _).
  rewrite envs_app_sound //; simpl. rewrite right_id HΔ' wand_elim_r.
  apply: fsa_mono=> v. by rewrite -later_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35 36
Qed.
End invariants.

37
Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
38
  eapply tac_inv_fsa with _ _ _ _ N H _ _;
39
    [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
40
     apply _ || fail "iInv: cannot viewshift in goal" P
41
    |trivial with fsaV
42
    |solve_ndisj
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44
    |iAssumption || fail "iInv: invariant" N "not found"
    |env_cbv; reflexivity
45
    |simpl (* get rid of FSAs *)].
Robbert Krebbers's avatar
Robbert Krebbers committed
46

47 48
Tactic Notation "iInv" constr(N) "as" constr(pat) :=
  let H := iFresh in iInvCore N as H; last iDestruct H as pat.
49
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
50
    constr(pat) :=
51 52 53 54 55 56 57 58 59
  let H := iFresh in iInvCore N as H; last iDestruct H as (x1) pat.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) ")" constr(pat) :=
  let H := iFresh in iInvCore N as H; last iDestruct H as (x1 x2) pat.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
  let H := iFresh in iInvCore N as H; last iDestruct H as (x1 x2 x3) pat.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
60
    constr(pat) :=
61
  let H := iFresh in iInvCore N as H; last iDestruct H as (x1 x2 x3 x4) pat.
62 63

Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _;
65
    [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
66
     apply _ || fail "iInv: cannot viewshift in goal" P
67
    |trivial with fsaV
68
    |solve_ndisj
Robbert Krebbers's avatar
Robbert Krebbers committed
69 70 71 72
    |iAssumption || fail "iOpenInv: invariant" N "not found"
    |let P := match goal with |- TimelessP ?P => P end in
     apply _ || fail "iInv:" P "not timeless"
    |env_cbv; reflexivity
73 74 75 76
    |simpl (* get rid of FSAs *)].

Tactic Notation "iInv>" constr(N) "as" constr(pat) :=
  let H := iFresh in iInvCore> N as H; last iDestruct H as pat.
77
Tactic Notation "iInv>" constr(N) "as" "(" simple_intropattern(x1) ")"
78
    constr(pat) :=
79 80 81 82 83 84 85 86 87
  let H := iFresh in iInvCore> N as H; last iDestruct H as (x1) pat.
Tactic Notation "iInv>" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) ")" constr(pat) :=
  let H := iFresh in iInvCore> N as H; last iDestruct H as (x1 x2) pat.
Tactic Notation "iInv>" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
  let H := iFresh in iInvCore> N as H; last iDestruct H as (x1 x2 x3) pat.
Tactic Notation "iInv>" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
88
    constr(pat) :=
89
  let H := iFresh in iInvCore> N as H; last iDestruct H as (x1 x2 x3 x4) pat.