Commit 53325866 authored by Ralf Jung's avatar Ralf Jung

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

parents 19e70e9e 5d3fe67e
Pipeline #2579 passed with stage
in 4 minutes and 14 seconds
......@@ -504,8 +504,6 @@ Section ucmra.
Context {A : ucmraT}.
Implicit Types x y z : A.
Global Instance ucmra_unit_inhabited : Inhabited A := populate .
Lemma ucmra_unit_validN n : {n} (:A).
Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
Lemma ucmra_unit_leastN n x : {n} x.
......
......@@ -106,17 +106,17 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma coerce_f {k j} (H : S k = S j) (x : A k) :
coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x).
Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
Lemma gg_gg {k i i1 i2 j} : (H1: k = i + j) (H2: k = i2 + (i1 + j)) (x: A k),
gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
Proof.
assert (i = i2 + i1) by lia; move:H1=>H1; simplify_eq/=. revert j x H1.
intros ? -> x. assert (i = i2 + i1) as -> by lia. revert j x H1.
induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=;
[by rewrite coerce_id|by rewrite g_coerce IH].
Qed.
Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
Lemma ff_ff {k i i1 i2 j} : (H1: i + k = j) (H2: i1 + (i2 + k) = j) (x: A k),
coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
Proof.
assert (i = i1 + i2) by lia; move:H1=>H1; simplify_eq/=.
intros ? <- x. assert (i = i1 + i2) as -> by lia.
induction i1 as [|i1 IH]; simplify_eq/=;
[by rewrite coerce_id|by rewrite coerce_f IH].
Qed.
......
......@@ -349,7 +349,7 @@ Proof.
refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Instance expr_inhabited : Inhabited (expr) := populate (Lit LitUnit).
Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
Canonical Structure stateC := leibnizC state.
......
......@@ -567,6 +567,8 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
Class Empty A := empty: A.
Notation "∅" := empty : C_scope.
Instance empty_inhabited `(Empty A) : Inhabited A := populate .
Class Top A := top : A.
Notation "⊤" := top : C_scope.
......
......@@ -2,7 +2,7 @@ From iris.algebra Require Import upred.
From iris.proofmode Require Import tactics.
(** This proves that we need the ▷ in a "Saved Proposition" construction with
name-dependend allocation. *)
name-dependent allocation. *)
Module savedprop. Section savedprop.
Context (M : ucmraT).
Notation iProp := (uPred M).
......@@ -128,7 +128,7 @@ Module inv. Section inv.
apply pvs_mono. by rewrite -HP -(uPred.exist_intro a).
Qed.
(** Now to the actual counterexample. We start with a weird for of saved propositions. *)
(** Now to the actual counterexample. We start with a weird form of saved propositions. *)
Definition saved (γ : gname) (P : iProp) : iProp :=
i, inv i (start γ (finished γ P)).
Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
......
......@@ -30,7 +30,7 @@ Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
(* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
atomic e
ElimVs (|={E1,E2}=> P) P
ElimVs (|={E1,E2}=> P) P
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
End weakestpre.
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