siprop.v 12.3 KB
Newer Older
1 2
From iris.algebra Require Export ofe.
From iris.bi Require Import notation.
3
From iris Require Import options.
4

Robbert Krebbers's avatar
Robbert Krebbers committed
5 6 7
(** The type [siProp] defines "plain" step-indexed propositions, on which we
define the usual connectives of higher-order logic, and prove that these satisfy
the usual laws of higher-order logic. *)
8 9 10 11 12 13
Record siProp := SiProp {
  siProp_holds :> nat  Prop;
  siProp_closed n1 n2 : siProp_holds n1  n2  n1  siProp_holds n2
}.
Arguments siProp_holds : simpl never.
Add Printing Constructor siProp.
Ralf Jung's avatar
Ralf Jung committed
14 15

Declare Scope siProp_scope.
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
Delimit Scope siProp_scope with SI.
Bind Scope siProp_scope with siProp.

Section cofe.
  Inductive siProp_equiv' (P Q : siProp) : Prop :=
    { siProp_in_equiv :  n, P n  Q n }.
  Instance siProp_equiv : Equiv siProp := siProp_equiv'.
  Inductive siProp_dist' (n : nat) (P Q : siProp) : Prop :=
    { siProp_in_dist :  n', n'  n  P n'  Q n' }.
  Instance siProp_dist : Dist siProp := siProp_dist'.
  Definition siProp_ofe_mixin : OfeMixin siProp.
  Proof.
    split.
    - intros P Q; split.
      + by intros HPQ n; split=> i ?; apply HPQ.
      + intros HPQ; split=> n; apply HPQ with n; auto.
    - intros n; split.
      + by intros P; split=> i.
      + by intros P Q HPQ; split=> i ?; symmetry; apply HPQ.
      + intros P Q Q' HP HQ; split=> i ?.
        by trans (Q i);[apply HP|apply HQ].
    - intros n P Q HPQ; split=> i ?; apply HPQ; auto.
  Qed.
39
  Canonical Structure siPropO : ofeT := OfeT siProp siProp_ofe_mixin.
40

41
  Program Definition siProp_compl : Compl siPropO := λ c,
42 43 44 45 46
    {| siProp_holds n := c n n |}.
  Next Obligation.
    intros c n1 n2 ??; simpl in *.
    apply (chain_cauchy c n2 n1); eauto using siProp_closed.
  Qed.
47
  Global Program Instance siProp_cofe : Cofe siPropO := {| compl := siProp_compl |}.
48 49 50 51 52 53 54 55 56 57 58 59 60 61
  Next Obligation.
    intros n c; split=>i ?; symmetry; apply (chain_cauchy c i n); auto.
  Qed.
End cofe.

(** logical entailement *)
Inductive siProp_entails (P Q : siProp) : Prop :=
  { siProp_in_entails :  n, P n  Q n }.
Hint Resolve siProp_closed : siProp_def.

(** logical connectives *)
Program Definition siProp_pure_def (φ : Prop) : siProp :=
  {| siProp_holds n := φ |}.
Solve Obligations with done.
62
Definition siProp_pure_aux : seal (@siProp_pure_def). Proof. by eexists. Qed.
63 64 65 66 67 68 69
Definition siProp_pure := unseal siProp_pure_aux.
Definition siProp_pure_eq :
  @siProp_pure = @siProp_pure_def := seal_eq siProp_pure_aux.

Program Definition siProp_and_def (P Q : siProp) : siProp :=
  {| siProp_holds n := P n  Q n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
70
Definition siProp_and_aux : seal (@siProp_and_def). Proof. by eexists. Qed.
71 72 73 74 75 76
Definition siProp_and := unseal siProp_and_aux.
Definition siProp_and_eq: @siProp_and = @siProp_and_def := seal_eq siProp_and_aux.

Program Definition siProp_or_def (P Q : siProp) : siProp :=
  {| siProp_holds n := P n  Q n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
77
Definition siProp_or_aux : seal (@siProp_or_def). Proof. by eexists. Qed.
78 79 80 81 82 83
Definition siProp_or := unseal siProp_or_aux.
Definition siProp_or_eq: @siProp_or = @siProp_or_def := seal_eq siProp_or_aux.

Program Definition siProp_impl_def (P Q : siProp) : siProp :=
  {| siProp_holds n :=  n', n'  n  P n'  Q n' |}.
Next Obligation. intros P Q [|n1] [|n2]; auto with lia. Qed.
84
Definition siProp_impl_aux : seal (@siProp_impl_def). Proof. by eexists. Qed.
85 86 87 88 89 90 91
Definition siProp_impl := unseal siProp_impl_aux.
Definition siProp_impl_eq :
  @siProp_impl = @siProp_impl_def := seal_eq siProp_impl_aux.

Program Definition siProp_forall_def {A} (Ψ : A  siProp) : siProp :=
  {| siProp_holds n :=  a, Ψ a n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
92
Definition siProp_forall_aux : seal (@siProp_forall_def). Proof. by eexists. Qed.
93 94 95 96 97 98 99
Definition siProp_forall {A} := unseal siProp_forall_aux A.
Definition siProp_forall_eq :
  @siProp_forall = @siProp_forall_def := seal_eq siProp_forall_aux.

Program Definition siProp_exist_def {A} (Ψ : A  siProp) : siProp :=
  {| siProp_holds n :=  a, Ψ a n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
100
Definition siProp_exist_aux : seal (@siProp_exist_def). Proof. by eexists. Qed.
101 102 103 104 105
Definition siProp_exist {A} := unseal siProp_exist_aux A.
Definition siProp_exist_eq: @siProp_exist = @siProp_exist_def := seal_eq siProp_exist_aux.

Program Definition siProp_internal_eq_def {A : ofeT} (a1 a2 : A) : siProp :=
  {| siProp_holds n := a1 {n} a2 |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
Solve Obligations with naive_solver eauto 2 using dist_le.
107
Definition siProp_internal_eq_aux : seal (@siProp_internal_eq_def). Proof. by eexists. Qed.
108 109 110 111 112 113 114
Definition siProp_internal_eq {A} := unseal siProp_internal_eq_aux A.
Definition siProp_internal_eq_eq:
  @siProp_internal_eq = @siProp_internal_eq_def := seal_eq siProp_internal_eq_aux.

Program Definition siProp_later_def (P : siProp) : siProp :=
  {| siProp_holds n := match n return _ with 0 => True | S n' => P n' end |}.
Next Obligation. intros P [|n1] [|n2]; eauto using siProp_closed with lia. Qed.
115
Definition siProp_later_aux : seal (@siProp_later_def). Proof. by eexists. Qed.
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 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302
Definition siProp_later := unseal siProp_later_aux.
Definition siProp_later_eq :
  @siProp_later = @siProp_later_def := seal_eq siProp_later_aux.

(** Primitive logical rules.
    These are not directly usable later because they do not refer to the BI
    connectives. *)
Module siProp_primitive.
Definition unseal_eqs :=
  (siProp_pure_eq, siProp_and_eq, siProp_or_eq, siProp_impl_eq, siProp_forall_eq,
  siProp_exist_eq, siProp_internal_eq_eq, siProp_later_eq).
Ltac unseal := rewrite !unseal_eqs /=.

Section primitive.
Arguments siProp_holds !_ _ /.

Notation "P ⊢ Q" := (siProp_entails P Q)
  (at level 99, Q at level 200, right associativity).
Notation "'True'" := (siProp_pure True) : siProp_scope.
Notation "'False'" := (siProp_pure False) : siProp_scope.
Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : siProp_scope.
Infix "∧" := siProp_and : siProp_scope.
Infix "∨" := siProp_or : siProp_scope.
Infix "→" := siProp_impl : siProp_scope.
Notation "∀ x .. y , P" := (siProp_forall (λ x, .. (siProp_forall (λ y, P%SI)) ..)) : siProp_scope.
Notation "∃ x .. y , P" := (siProp_exist (λ x, .. (siProp_exist (λ y, P%SI)) ..)) : siProp_scope.
Notation "x ≡ y" := (siProp_internal_eq x y) : siProp_scope.
Notation "▷ P" := (siProp_later P) (at level 20, right associativity) : siProp_scope.

(** Below there follow the primitive laws for [siProp]. There are no derived laws
in this file. *)

(** Entailment *)
Lemma entails_po : PreOrder siProp_entails.
Proof.
  split.
  - intros P; by split=> i.
  - intros P Q Q' HP HQ; split=> i ?; by apply HQ, HP.
Qed.
Lemma entails_anti_symm : AntiSymm () siProp_entails.
Proof. intros P Q HPQ HQP; split=> n; by split; [apply HPQ|apply HQP]. Qed.
Lemma equiv_spec P Q : (P  Q)  (P  Q)  (Q  P).
Proof.
  split.
  - intros HPQ; split; split=> i; apply HPQ.
  - intros [??]. by apply entails_anti_symm.
Qed.

(** Non-expansiveness and setoid morphisms *)
Lemma pure_ne n : Proper (iff ==> dist n) siProp_pure.
Proof. intros φ1 φ2 Hφ. by unseal. Qed.
Lemma and_ne : NonExpansive2 siProp_and.
Proof.
  intros n P P' HP Q Q' HQ; unseal; split=> n' ?.
  split; (intros [??]; split; [by apply HP|by apply HQ]).
Qed.
Lemma or_ne : NonExpansive2 siProp_or.
Proof.
  intros n P P' HP Q Q' HQ; split=> n' ?.
  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
Qed.
Lemma impl_ne : NonExpansive2 siProp_impl.
Proof.
  intros n P P' HP Q Q' HQ; split=> n' ?.
  unseal; split; intros HPQ n'' ??; apply HQ, HPQ, HP; auto with lia.
Qed.
Lemma forall_ne A n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_forall A).
Proof.
   by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
Qed.
Lemma exist_ne A n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_exist A).
Proof.
  intros Ψ1 Ψ2 HΨ.
  unseal; split=> n' ?; split; intros [a ?]; exists a; by apply HΨ.
Qed.
Lemma later_contractive : Contractive siProp_later.
Proof.
  unseal; intros [|n] P Q HPQ; split=> -[|n'] ? //=; try lia.
  apply HPQ; lia.
Qed.
Lemma internal_eq_ne (A : ofeT) : NonExpansive2 (@siProp_internal_eq A).
Proof.
  intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
  - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
  - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
Qed.

(** Introduction and elimination rules *)
Lemma pure_intro (φ : Prop) P : φ  P   φ .
Proof. intros ?. unseal; by split. Qed.
Lemma pure_elim' (φ : Prop) P : (φ  True  P)   φ   P.
Proof. unseal=> HP; split=> n ?. by apply HP. Qed.
Lemma pure_forall_2 {A} (φ : A  Prop) : ( a,  φ a )    a, φ a .
Proof. by unseal. Qed.

Lemma and_elim_l P Q : P  Q  P.
Proof. unseal; by split=> n [??]. Qed.
Lemma and_elim_r P Q : P  Q  Q.
Proof. unseal; by split=> n [??]. Qed.
Lemma and_intro P Q R : (P  Q)  (P  R)  P  Q  R.
Proof. intros HQ HR; unseal; split=> n ?; by split; [apply HQ|apply HR]. Qed.

Lemma or_intro_l P Q : P  P  Q.
Proof. unseal; split=> n ?; left; auto. Qed.
Lemma or_intro_r P Q : Q  P  Q.
Proof. unseal; split=> n ?; right; auto. Qed.
Lemma or_elim P Q R : (P  R)  (Q  R)  P  Q  R.
Proof. intros HP HQ. unseal; split=> n [?|?]. by apply HP. by apply HQ. Qed.

Lemma impl_intro_r P Q R : (P  Q  R)  P  Q  R.
Proof.
  unseal=> HQ; split=> n ? n' ??.
  apply HQ; naive_solver eauto using siProp_closed.
Qed.
Lemma impl_elim_l' P Q R : (P  Q  R)  P  Q  R.
Proof. unseal=> HP; split=> n [??]. apply HP with n; auto. Qed.

Lemma forall_intro {A} P (Ψ : A  siProp) : ( a, P  Ψ a)  P   a, Ψ a.
Proof. unseal; intros HPΨ; split=> n ? a; by apply HPΨ. Qed.
Lemma forall_elim {A} {Ψ : A  siProp} a : ( a, Ψ a)  Ψ a.
Proof. unseal; split=> n HP; apply HP. Qed.

Lemma exist_intro {A} {Ψ : A  siProp} a : Ψ a   a, Ψ a.
Proof. unseal; split=> n ?; by exists a. Qed.
Lemma exist_elim {A} (Φ : A  siProp) Q : ( a, Φ a  Q)  ( a, Φ a)  Q.
Proof. unseal; intros HΨ; split=> n [a ?]; by apply HΨ with a. Qed.

(** Equality *)
Lemma internal_eq_refl {A : ofeT} P (a : A) : P  (a  a).
Proof. unseal; by split=> n ? /=. Qed.
Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A  siProp) :
  NonExpansive Ψ  a  b  Ψ a  Ψ b.
Proof.
  intros Hnonexp. unseal; split=> n Hab n' ? HΨ. eapply Hnonexp with n a; auto.
Qed.

Lemma fun_ext {A} {B : A  ofeT} (f g : discrete_fun B) : ( x, f x  g x)  f  g.
Proof. by unseal. Qed.
Lemma sig_eq {A : ofeT} (P : A  Prop) (x y : sig P) : `x  `y  x  y.
Proof. by unseal. Qed.
Lemma discrete_eq_1 {A : ofeT} (a b : A) : Discrete a  a  b  a  b.
Proof. unseal=> ?. split=> n. by apply (discrete_iff n). Qed.

Lemma prop_ext_2 P Q : ((P  Q)  (Q  P))  P  Q.
Proof.
  unseal; split=> n /= HPQ. split=> n' ?.
  move: HPQ=> [] /(_ n') ? /(_ n'). naive_solver.
Qed.

(** Later *)
Lemma later_eq_1 {A : ofeT} (x y : A) : Next x  Next y   (x  y).
Proof. by unseal. Qed.
Lemma later_eq_2 {A : ofeT} (x y : A) :  (x  y)  Next x  Next y.
Proof. by unseal. Qed.

Lemma later_mono P Q : (P  Q)   P   Q.
Proof. unseal=> HP; split=>-[|n]; [done|apply HP; eauto using cmra_validN_S]. Qed.
Lemma later_intro P : P   P.
Proof. unseal; split=> -[|n] /= HP; eauto using siProp_closed. Qed.

Lemma later_forall_2 {A} (Φ : A  siProp) : ( a,  Φ a)    a, Φ a.
Proof. unseal; by split=> -[|n]. Qed.
Lemma later_exist_false {A} (Φ : A  siProp) :
  (  a, Φ a)   False  ( a,  Φ a).
Proof. unseal; split=> -[|[|n]] /=; eauto. Qed.
Lemma later_false_em P :  P   False  ( False  P).
Proof.
  unseal; split=> -[|n] /= HP; [by left|right].
  intros [|n'] ?; eauto using siProp_closed with lia.
Qed.

(** Consistency/soundness statement *)
Lemma pure_soundness φ : (True   φ )  φ.
Proof. unseal=> -[H]. by apply (H 0). Qed.

Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True  x  y)  x  y.
Proof. unseal=> -[H]. apply equiv_dist=> n. by apply (H n). Qed.

Lemma later_soundness P : (True   P)  (True  P).
Proof.
  unseal=> -[HP]; split=> n _. apply siProp_closed with n; last done.
  by apply (HP (S n)).
Qed.
End primitive.
End siProp_primitive.