iron.v 11.7 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
(** This file defines the main constructs of the Iron logic. It does do so in
two stages:

1. It defines the [ironInvG] class that expresses the cameras that are needed
   to get the Iron reasoning principles in the basic Iron logic.
2. It defines the type [ironProp] of propositions of the Iron++ logic.
 
The latter is done by instantiating the general construction of predicates over
fractions (as in the file [bi/fracpred]) with a concrete BI: that of Iris
propositions, i.e:

<<<
Notation ironProp Σ := (fracPred (iProp Σ)).
>>>

From the generic [fracPred] construction we get all of the standard BI
connectives, but this file defines some notions that are missing:

- The [perm π] connective, which is denoted [𝖊(π)] in the paper.
- The type class [Uniform], which expresses that an Iron++ proposition is
  uniform w.r.t fractions. We provide instances showing that uniform
  propositions are closed under affine propositions, (big) separating
  conjunction, disjunctions, and existential quantifiers.
- A lifted version of fancy updates [|={E1,E2}=>] that threads through the
  [perm π] connective. This is done by instantiating Iris's [BiFUpdMixin] type
  class so that we get overloaded notations, and can share common derived
  results. *)
From iron.bi Require Export fracpred.
From iris.bi.lib Require Export fractional.
From iris.base_logic.lib Require Export fancy_updates invariants.
From iris.base_logic.lib Require Export cancelable_invariants.
From iris.algebra Require Import frac_auth.
33
From iris.algebra Require Import ufrac.
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35 36 37 38 39 40 41
From iris.proofmode Require Import tactics.
From iron.proofmode Require Import fracpred.

Class ironInvG (Σ : gFunctors) := IronInvG {
  perm : frac  iProp Σ;
  perm_fractional :> Fractional perm;
  perm_timeless π :> Timeless (perm π);
  fcinv_cinvG :> cinvG Σ;
42
  fcinv_inG :> inG Σ (frac_authR ufracR);
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44
}.
Notation ironProp Σ := (fracPred (iProp Σ)).
45
Notation ironPropC Σ := (fracPredO (iProp Σ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
46 47 48 49 50 51 52 53 54 55
Notation ironPropI Σ := (fracPredI (uPredI (iResUR Σ))).
Notation ironPropSI Σ := (fracPredSI (uPredSI (iResUR Σ))).

Instance perm_as_fractional `{ironInvG Σ} π : AsFractional (perm π) perm π.
Proof. split. done. apply _. Qed.

Class Uniform `{ironInvG Σ} (P : ironProp Σ) :=
  uniform π1 π2 : P (Some (π1  π2))  P (Some π1)  perm π2.
Arguments Uniform {_ _} _%I.
Hint Mode Uniform + + ! : typeclass_instances.
56
Instance: Params (@Uniform) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58 59 60 61

Class ExistPerm `{ironInvG Σ} (P : ironProp Σ) :=
  exist_perm : P None  False.
Arguments ExistPerm {_ _} _%I.
Hint Mode ExistPerm + - ! : typeclass_instances.
62
Instance: Params (@ExistPerm) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254

Definition iron_fupd_def `{ironInvG Σ, invG Σ} (E1 E2 : coPset)
    (P : ironProp Σ) : ironProp Σ := FracPred (λ π2,  π1,
  perm π1 ={E1,E2}=
     π1' π2',  π1 ? π2 = π1' ? π2'   perm π1'  P π2')%I.
Definition iron_fupd_aux `{ironInvG Σ, invG Σ} : seal iron_fupd_def. by eexists. Qed.
Definition iron_fupd `{ironInvG Σ, invG Σ} : FUpd _ := iron_fupd_aux.(unseal).
Definition iron_fupd_eq `{ironInvG Σ, invG Σ} : @fupd _ iron_fupd = _ :=
  iron_fupd_aux.(seal_eq).

Section iron.
Context `{ironInvG Σ, invG Σ}.
Implicit Types P : ironProp Σ.

(** Fancy updates *)
Lemma iron_fupd_mixin : BiFUpdMixin (ironPropSI Σ) iron_fupd.
Proof.
  split; rewrite iron_fupd_eq.
  - split=>/= π. solve_proper.
  - intros E1 E2 P HE12. split=>/= π2. apply bi.forall_intro=> π1.
    rewrite -(bi.exist_intro π1) -(bi.exist_intro π2) bi.pure_True // left_id.
    apply bi.wand_intro_l. rewrite (fupd_intro_mask E1 E2 (P _)) // fupd_frame_l.
    do 2 f_equiv. apply bi.forall_intro=> π1'.
    rewrite -(bi.exist_intro π1') -(bi.exist_intro π2) bi.pure_True // left_id.
    apply bi.wand_intro_l. by rewrite fupd_frame_l.
  - intros E1 E2 P. split=>/= π2. rewrite fracPred_at_except_0 /=.
    apply bi.forall_intro=> π1. apply bi.wand_intro_l.
    by rewrite (bi.forall_elim π1) bi.except_0_frame_l bi.wand_elim_r except_0_fupd.
  - intros E1 E2 P Q HPQ. split=>/= π2. by setoid_rewrite HPQ.
  - intros E1 E2 E3 P. split=>/= π2. f_equiv=> π1. f_equiv.
    rewrite -(fupd_trans E1 E2 E3). f_equiv.
    apply bi.exist_elim=> π1'; apply bi.exist_elim=> π2'. apply bi.pure_elim_l=> ->.
    by rewrite (bi.forall_elim π1') bi.wand_elim_r.
  - intros E1 E2 Ef P HE1f. split=>/= π2. f_equiv=> π1. f_equiv.
    rewrite -fupd_mask_frame_r' //. f_equiv. apply bi.impl_intro_l, bi.pure_elim_l=> ?.
    f_equiv=> π1'; f_equiv=> π2'. by rewrite (bi.pure_True (_ ## _)) // left_id.
  - intros E1 E2 P Q. split=>/= π2. rewrite fracPred_at_sep /=.
    apply bi.exist_elim=> π21. apply bi.exist_elim=> π22. apply bi.pure_elim_l=> ->.
    apply bi.forall_intro=> π1. apply bi.wand_intro_l.
    rewrite (bi.forall_elim π1) assoc bi.wand_elim_r fupd_frame_r.
    repeat setoid_rewrite bi.sep_exist_r. f_equiv. f_equiv=> π1'.
    apply bi.exist_elim=> π2'. rewrite -(bi.exist_intro (π2'  π22)).
    rewrite -!bi.persistent_and_sep_assoc -!cmra_opM_opM_assoc_L.
    apply bi.pure_elim_l=> ->. rewrite bi.pure_True // left_id.
    by rewrite -assoc -fracPred_at_sep_2.
Qed.
Global Instance iron_bi_fupd : BiFUpd (ironPropSI Σ) :=
  {| bi_fupd_mixin := iron_fupd_mixin |}.

Lemma fracPred_at_fupd π2 E1 E2 P :
  (|={E1,E2}=> P) π2   π1, perm π1 ={E1,E2}=
     π1' π2',  π1 ? π2 = π1' ? π2'   perm π1'  P π2'.
Proof. by rewrite iron_fupd_eq. Qed.
Lemma fracPred_at_fupd_2 π2 E1 E2 P : (|={E1,E2}=> P π2)  (|={E1,E2}=> P) π2.
Proof.
  rewrite fracPred_at_fupd. apply bi.forall_intro=> π1. apply bi.wand_intro_l.
  rewrite -(bi.exist_intro π1) -(bi.exist_intro π2) bi.pure_True // left_id.
  by rewrite fupd_frame_l.
Qed.

Global Instance iron_bi_bupd_fupd : BiBUpdFUpd (ironPropSI Σ).
Proof.
  intros E P. split=>/= π2. rewrite fracPred_at_bupd -fracPred_at_fupd_2 /=.
  by rewrite bupd_fupd.
Qed.

Global Instance make_fracPred_at_fupd E1 E2 π2 P Φ :
  ( π, MakeFracPredAt π P (Φ π)) 
  MakeFracPredAt π2 (|={E1,E2}=> P) ( π1,
    perm π1 ={E1,E2}=  π1' π2',  π1 ? π2 = π1' ? π2'   perm π1'  Φ π2')%I.
Proof. rewrite /MakeFracPredAt fracPred_at_fupd=> HP. by setoid_rewrite HP. Qed.

(* Higher precendence than elim_modal_bupd_fupd *)
Global Instance elim_modal_bupd_fupd_affine E1 E2 P P' Q :
  FromAffinely P' P 
  ElimModal True true false (|==> P) P' (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 0.
Proof.
  rewrite /FromAffinely /ElimModal /= => <- _.
  rewrite bi.intuitionistically_affinely fracPred_affinely_bupd.
  by rewrite bupd_frame_r bi.wand_elim_r (bupd_fupd E1) fupd_trans.
Qed.

(* TODO: The class [BiEmbedFUpd PROP fracPredSI] holds only in one direction,
we could declare proof mode instance manually for the direction that holds,
but so far, that did not appear to be useful. *)

(** Instances of the Uniform type class*)

(* The following lemma is not an instance, to avoid excessive backtracking it
should only be used at the leaves of type class search. Hence, it's declared as
a [Hint Immediate] in the end of this file. *)
Lemma affine_uniform P : Affine P  Uniform P.
Proof.
  intros ? π1 π2. apply (anti_symm _).
  - rewrite {1}(affine P) fracPred_at_emp bi.pure_False // bi.affinely_False.
    apply bi.False_elim.
  - rewrite {1}(affine P) fracPred_at_emp bi.pure_False // bi.affinely_False.
    rewrite left_absorb. apply bi.False_elim.
Qed.

Global Instance Uniform_proper : Proper (() ==> iff) Uniform.
Proof. intros P1 P2 HP; split=> ? π π'. by rewrite -HP. by rewrite HP. Qed.

Global Instance False_uniform : Uniform False.
Proof. apply affine_uniform, _. Qed.
Global Instance emp_uniform : Uniform emp.
Proof. by apply affine_uniform. Qed.
Global Instance sep_uniform P1 P2 : Uniform P1  Uniform P2  Uniform (P1  P2).
Proof.
  rewrite /Uniform=> HP1 HP2 π1 π2. rewrite !fracPred_at_sep. apply (anti_symm _).
  - apply bi.exist_elim=> -[π1'|]; apply bi.exist_elim=> -[π2'|];
      apply bi.pure_elim_l; rewrite ?(inj_iff Some) //.
    + intros. destruct (Qp_cross_split (π1 + π2) π1 π2 π1' π2')
        as (π'&π''&π'''&π''''&<-&<-&<-&<-)=> //.
      rewrite HP1 HP2 -(bi.exist_intro (Some π')) -(bi.exist_intro (Some π'')).
      rewrite bi.pure_True // left_id fractional. solve_sep_entails.
    + intros <-. rewrite HP1 -(bi.exist_intro (Some π1)) -(bi.exist_intro ε).
      rewrite bi.pure_True // left_id. solve_sep_entails.
    + intros <-. rewrite HP2 -(bi.exist_intro ε) -(bi.exist_intro (Some π1)).
      rewrite bi.pure_True // left_id. solve_sep_entails.
  - repeat setoid_rewrite bi.sep_exist_r.
    apply bi.exist_elim=> π1'; apply bi.exist_elim=> π2'.
    rewrite -bi.persistent_and_sep_assoc; apply bi.pure_elim_l.
    destruct π1' as [π1'|], π2' as [π2'|]; rewrite ?(inj_iff Some) // => ->.
    + rewrite -(bi.exist_intro (Some π1')) -(bi.exist_intro (Some (π2'  π2))).
      rewrite -assoc_L bi.pure_True // left_id HP2. solve_sep_entails.
    + rewrite -(bi.exist_intro (Some (π1'  π2))) -(bi.exist_intro ε).
      rewrite right_id_L bi.pure_True // left_id HP1. solve_sep_entails.
    + rewrite -(bi.exist_intro ε) -(bi.exist_intro (Some (π2'  π2))).
      rewrite bi.pure_True // left_id HP2. solve_sep_entails.
Qed.
Global Instance big_sepL_uniform {A} (Φ : A  ironProp Σ) l :
  ( x, Uniform (Φ x))  Uniform ([ list] x  l, Φ x).
Proof. intros; induction l; simpl; apply _. Qed.
Global Instance exist_uniform {A} (Φ : A  fracPred _) :
  ( x, Uniform (Φ x))  Uniform ( x, Φ x).
Proof.
  rewrite /Uniform=> HΦ π1 π2. rewrite !fracPred_at_exist bi.sep_exist_r.
  by setoid_rewrite HΦ.
Qed.
Global Instance or_uniform P1 P2 : Uniform P1  Uniform P2  Uniform (P1  P2).
Proof. intros ??. rewrite bi.or_alt. by apply exist_uniform=> -[]. Qed.

Global Instance affinely_uniform P : Uniform (<affine> P).
Proof. apply affine_uniform, _. Qed.
Global Instance intuitionistically_uniform P : Uniform ( P).
Proof. apply affine_uniform, _. Qed.
Global Instance and_uniform_l P1 P2 :
  Uniform P1  Persistent P2  Absorbing P2  Uniform (P1  P2).
Proof. intros. rewrite bi.persistent_and_affinely_sep_r. apply _. Qed.
Global Instance and_uniform_r P1 P2 :
  Persistent P1  Absorbing P1  Uniform P2  Uniform (P1  P2).
Proof. intros. rewrite bi.persistent_and_affinely_sep_l. apply _. Qed.

(** ExistPerm *)
Global Instance ExistPerm_proper : Proper (() ==> iff) ExistPerm.
Proof. solve_proper. Qed.

Global Instance False_exist_perm : ExistPerm False.
Proof. by rewrite /ExistPerm fracPred_at_pure. Qed.
Global Instance sep_exist_perm_l P1 P2 : ExistPerm P1  ExistPerm (P1  P2).
Proof.
  rewrite /ExistPerm=> HP. rewrite fracPred_at_sep.
  apply bi.exist_elim=> -[π1'|]; apply bi.exist_elim=> -[π2'|];
    apply bi.pure_elim_l=> ? //.
  by rewrite HP left_absorb.
Qed.
Global Instance sep_exist_perm_r P1 P2 : ExistPerm P2  ExistPerm (P1  P2).
Proof. rewrite comm. apply _. Qed.
Global Instance exist_exist_perm {A} (Φ : A  fracPred _) :
  ( x, ExistPerm (Φ x))  ExistPerm ( x, Φ x).
Proof.
  rewrite /ExistPerm=> HΦ. rewrite !fracPred_at_exist.
  apply bi.exist_elim=> x. by rewrite HΦ.
Qed.
Global Instance or_exist_perm P1 P2 : ExistPerm P1  ExistPerm P2  ExistPerm (P1  P2).
Proof. intros ??. rewrite bi.or_alt. by apply exist_exist_perm=> -[]. Qed.

Global Instance and_exist_perm_l P1 P2 : ExistPerm P1  ExistPerm (P1  P2).
Proof. rewrite /ExistPerm=> HP. by rewrite fracPred_at_and HP left_absorb. Qed.
Global Instance and_exist_perm_r P1 P2 : ExistPerm P2  ExistPerm (P1  P2).
Proof. rewrite comm; apply _. Qed.

Global Instance from_assumption_fracPred_None p P QQ :
  ExistPerm P  FromAssumption p (P None) QQ.
Proof.
  rewrite /ExistPerm /FromAssumption=> ->.
  by rewrite bi.intuitionistically_if_False bi.False_elim.
Qed.
End iron.

Hint Immediate affine_uniform : typeclass_instances.