Commit 672d60be by Ralf Jung

### Merge branch 'ralf/saved_prop' into 'master'

```saved predicates: use ofe_fun, not ofe_mor

See merge request FP/iris-coq!86```
parents bbc61206 3b0c15c3
 ... ... @@ -87,22 +87,23 @@ Proof. Qed. (* Saved predicates. *) Notation savedPredG Σ A := (savedAnythingG Σ (constCF A -n> ▶ ∙)). Notation savedPredΣ A := (savedAnythingΣ (constCF A -n> ▶ ∙)). Notation savedPredG Σ A := (savedAnythingG Σ (A -c> ▶ ∙)). Notation savedPredΣ A := (savedAnythingΣ (A -c> ▶ ∙)). Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A -n> iProp Σ) := saved_anything_own (F := A -n> ▶ ∙) γ (CofeMor Next ◎ Φ). Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) := saved_anything_own (F := A -c> ▶ ∙) γ (CofeMor Next ∘ Φ). Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ). Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ : (A -c> iProp Σ) → iProp Σ). Proof. solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | f_contractive | f_equiv ]). solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]). Qed. Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -n> iProp Σ) : Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) : (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ)%I. Proof. iApply saved_anything_alloc_strong. Qed. Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A -n> iProp Σ) : Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A → iProp Σ) : (|==> ∃ γ, saved_pred_own γ Φ)%I. Proof. iApply saved_anything_alloc. Qed. ... ... @@ -111,7 +112,7 @@ Lemma saved_pred_agree `{savedPredG Σ A} γ Φ Ψ x : saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x). Proof. iIntros "HΦ HΨ". unfold saved_pred_own. iApply later_equivI. iDestruct (ofe_morC_equivI (CofeMor Next ◎ Φ) (CofeMor Next ◎ Ψ)) as "[FE _]". iDestruct (ofe_funC_equivI (CofeMor Next ∘ Φ) (CofeMor Next ∘ Ψ)) as "[FE _]". simpl. iApply ("FE" with "[-]"). iApply (saved_anything_agree with "HΦ HΨ"). Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!