Commit a39b10c9 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 09e52924 8d983adf
...@@ -256,22 +256,28 @@ Ltac f_equiv := ...@@ -256,22 +256,28 @@ Ltac f_equiv :=
let H := fresh "Proper" in let H := fresh "Proper" in
assert (Proper (R ==> R ==> R) f) as H by (eapply _); assert (Proper (R ==> R ==> R) f) as H by (eapply _);
apply H; clear H; f_equiv apply H; clear H; f_equiv
(* Next, try to infer the relation *) (* Next, try to infer the relation. Unfortunately, there is an instance
of Proper for (eq ==> _), which will always be matched. *)
(* TODO: Can we exclude that instance? *)
(* TODO: If some of the arguments are the same, we could also (* TODO: If some of the arguments are the same, we could also
query for "pointwise_relation"'s. But that leads to a combinatorial query for "pointwise_relation"'s. But that leads to a combinatorial
explosion about which arguments are and which are not the same. *) explosion about which arguments are and which are not the same. *)
| |- ?R (?f ?x) (?f _) => | |- ?R (?f ?x) (?f _) =>
let R1 := fresh "R" in let H := fresh "Proper" in let R1 := fresh "R" in let H := fresh "HProp" in
let T := type of x in evar (R1: relation T); let T := type of x in evar (R1: relation T);
assert (Proper (R1 ==> R) f) as H by (subst R1; eapply _); assert (Proper (R1 ==> R) f) as H by (subst R1; eapply _);
subst R1; apply H; clear H; f_equiv subst R1; apply H; clear H; f_equiv
| |- ?R (?f ?x ?y) (?f _ _) => | |- ?R (?f ?x ?y) (?f _ _) =>
let R1 := fresh "R" in let R2 := fresh "R" in let R1 := fresh "R" in let R2 := fresh "R" in
let H := fresh "Proper" in let H := fresh "HProp" in
let T1 := type of x in evar (R1: relation T1); let T1 := type of x in evar (R1: relation T1);
let T2 := type of y in evar (R2: relation T2); let T2 := type of y in evar (R2: relation T2);
assert (Proper (R1 ==> R2 ==> R) f) as H by (subst R1 R2; eapply _); assert (Proper (R1 ==> R2 ==> R) f) as H by (subst R1 R2; eapply _);
subst R1 R2; apply H; clear H; f_equiv subst R1 R2; apply H; clear H; f_equiv
(* In case the function symbol differs, but the arguments are the same,
maybe we have a pointwise_relation in our context. *)
| H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) =>
apply H; f_equiv
end | idtac (* Let the user solve this goal *) end | idtac (* Let the user solve this goal *)
]. ].
...@@ -288,6 +294,10 @@ Ltac solve_proper := ...@@ -288,6 +294,10 @@ Ltac solve_proper :=
end; end;
(* Unfold the head symbol, which is the one we are proving a new property about *) (* Unfold the head symbol, which is the one we are proving a new property about *)
lazymatch goal with lazymatch goal with
| |- ?R (?f _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _ _ _) (?f _ _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _ _) (?f _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _) (?f _ _ _ _) => unfold f | |- ?R (?f _ _ _ _) (?f _ _ _ _) => unfold f
| |- ?R (?f _ _ _) (?f _ _ _) => unfold f | |- ?R (?f _ _ _) (?f _ _ _) => unfold f
| |- ?R (?f _ _) (?f _ _) => unfold f | |- ?R (?f _ _) (?f _ _) => unfold f
......
...@@ -40,7 +40,7 @@ Section auth. ...@@ -40,7 +40,7 @@ Section auth.
Implicit Types γ : gname. Implicit Types γ : gname.
Global Instance auth_own_ne n γ : Proper (dist n ==> dist n) (auth_own γ). Global Instance auth_own_ne n γ : Proper (dist n ==> dist n) (auth_own γ).
Proof. by rewrite auth_own_eq /auth_own_def=> a b ->. Qed. Proof. rewrite auth_own_eq; solve_proper. Qed.
Global Instance auth_own_proper γ : Proper (() ==> ()) (auth_own γ). Global Instance auth_own_proper γ : Proper (() ==> ()) (auth_own γ).
Proof. by rewrite auth_own_eq /auth_own_def=> a b ->. Qed. Proof. by rewrite auth_own_eq /auth_own_def=> a b ->. Qed.
Global Instance auth_own_timeless γ a : TimelessP (auth_own γ a). Global Instance auth_own_timeless γ a : TimelessP (auth_own γ a).
......
...@@ -9,6 +9,7 @@ Local Hint Extern 10 (✓{_} _) => ...@@ -9,6 +9,7 @@ Local Hint Extern 10 (✓{_} _) =>
| H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
end; solve_validN. end; solve_validN.
(* TODO: Consider sealing this, like all the definitions in upred.v. *)
Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ := Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
{| uPred_holds n r1 := rf k Ef σ, {| uPred_holds n r1 := rf k Ef σ,
0 < k n (E1 E2) Ef = 0 < k n (E1 E2) Ef =
......
...@@ -52,22 +52,20 @@ Section sts. ...@@ -52,22 +52,20 @@ Section sts.
(** Setoids *) (** Setoids *)
Global Instance sts_inv_ne n γ : Global Instance sts_inv_ne n γ :
Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv γ). Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv γ).
Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed. Proof. solve_proper. Qed.
Global Instance sts_inv_proper γ : Global Instance sts_inv_proper γ :
Proper (pointwise_relation _ () ==> ()) (sts_inv γ). Proper (pointwise_relation _ () ==> ()) (sts_inv γ).
Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed. Proof. solve_proper. Qed.
Global Instance sts_ownS_proper γ : Proper (() ==> () ==> ()) (sts_ownS γ). Global Instance sts_ownS_proper γ : Proper (() ==> () ==> ()) (sts_ownS γ).
Proof. Proof. rewrite sts_ownS_eq. solve_proper. Qed.
intros S1 S2 HS T1 T2 HT. by rewrite !sts_ownS_eq /sts_ownS_def HS HT.
Qed.
Global Instance sts_own_proper γ s : Proper (() ==> ()) (sts_own γ s). Global Instance sts_own_proper γ s : Proper (() ==> ()) (sts_own γ s).
Proof. intros T1 T2 HT. by rewrite !sts_own_eq /sts_own_def HT. Qed. Proof. rewrite sts_own_eq. solve_proper. Qed.
Global Instance sts_ctx_ne n γ N : Global Instance sts_ctx_ne n γ N :
Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx γ N). Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx γ N).
Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed. Proof. solve_proper. Qed.
Global Instance sts_ctx_proper γ N : Global Instance sts_ctx_proper γ N :
Proper (pointwise_relation _ () ==> ()) (sts_ctx γ N). Proper (pointwise_relation _ () ==> ()) (sts_ctx γ N).
Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed. Proof. solve_proper. Qed.
(* The same rule as implication does *not* hold, as could be shown using (* The same rule as implication does *not* hold, as could be shown using
sts_frag_included. *) sts_frag_included. *)
......
...@@ -30,6 +30,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset) ...@@ -30,6 +30,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset)
wp_go (E Ef) (wp_pre E Φ) wp_go (E Ef) (wp_pre E Φ)
(wp_pre (λ _, True%I)) k rf e1 σ1) (wp_pre (λ _, True%I)) k rf e1 σ1)
wp_pre E Φ e1 n r1. wp_pre E Φ e1 n r1.
(* TODO: Consider sealing this, like all the definitions in upred.v. *)
Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ) Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ)
(Φ : val Λ iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}. (Φ : val Λ iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}.
Next Obligation. Next Obligation.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment