Commit 8a13d685 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (⊢ changes).

parent 8b55e227
Pipeline #25566 passed with stage
in 17 minutes and 51 seconds
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [ depends: [
"coq-iris" { (= "dev.2020-03-10.6.79f576aa") | (= "dev") } "coq-iris" { (= "dev.2020-03-16.0.62be0a86") | (= "dev") }
] ]
...@@ -411,7 +411,7 @@ Section proto. ...@@ -411,7 +411,7 @@ Section proto.
iProto_le p1 p2 iProto_le_aux (fixpoint iProto_le_aux) p1 p2. iProto_le p1 p2 iProto_le_aux (fixpoint iProto_le_aux) p1 p2.
Proof. apply: (fixpoint_unfold iProto_le_aux). Qed. Proof. apply: (fixpoint_unfold iProto_le_aux). Qed.
Lemma iProto_le_refl p : iProto_le p p. Lemma iProto_le_refl p : iProto_le p p.
Proof. Proof.
iLöb as "IH" forall (p). destruct (proto_case p) as [->|([]&pc&->)]. iLöb as "IH" forall (p). destruct (proto_case p) as [->|([]&pc&->)].
- rewrite iProto_le_unfold. iLeft; by auto. - rewrite iProto_le_unfold. iLeft; by auto.
......
...@@ -116,7 +116,7 @@ Section mapper. ...@@ -116,7 +116,7 @@ Section mapper.
Proof. intros [i1 y1] [i2 y2]. destruct (total ()%Z i1 i2); [left|right]; done. Qed. Proof. intros [i1 y1] [i2 y2]. destruct (total ()%Z i1 i2); [left|right]; done. Qed.
Instance RZB_trans : Transitive RZB. Instance RZB_trans : Transitive RZB.
Proof. by apply (prod_relation_trans _). Qed. Proof. by apply (prod_relation_trans _). Qed.
Lemma RZB_cmp_spec : cmp_spec IZB RZB cmpZfst. Lemma RZB_cmp_spec : cmp_spec IZB RZB cmpZfst.
Proof. Proof.
iIntros ([i1 y1] [i2 y2] v1 v2) "!>"; iIntros (Φ) "[HI1 HI2] HΦ". iIntros ([i1 y1] [i2 y2] v1 v2) "!>"; iIntros (Φ) "[HI1 HI2] HΦ".
iDestruct "HI1" as (w1 ->) "HI1". iDestruct "HI2" as (w2 ->) "HI2 /=". iDestruct "HI1" as (w1 ->) "HI1". iDestruct "HI2" as (w2 ->) "HI2 /=".
......
...@@ -15,7 +15,7 @@ Definition cmp_spec `{!heapG Σ} {A} (I : A → val → iProp Σ) ...@@ -15,7 +15,7 @@ Definition cmp_spec `{!heapG Σ} {A} (I : A → val → iProp Σ)
Definition IZ `{!heapG Σ} (x : Z) (v : val) : iProp Σ := v = #x%I. Definition IZ `{!heapG Σ} (x : Z) (v : val) : iProp Σ := v = #x%I.
Definition cmpZ : val := λ: "x" "y", "x" "y". Definition cmpZ : val := λ: "x" "y", "x" "y".
Lemma cmpZ_spec `{!heapG Σ} : cmp_spec IZ () cmpZ. Lemma cmpZ_spec `{!heapG Σ} : cmp_spec IZ () cmpZ.
Proof. Proof.
rewrite /IZ. iIntros (x x' v v' Φ [-> ->]) "!> HΦ". rewrite /IZ. iIntros (x x' v v' Φ [-> ->]) "!> HΦ".
wp_lam. wp_pures. by iApply "HΦ". wp_lam. wp_pures. by iApply "HΦ".
......
...@@ -50,7 +50,7 @@ Section contribution. ...@@ -50,7 +50,7 @@ Section contribution.
Global Instance client_proper γ : Proper (() ==> ()) (client γ). Global Instance client_proper γ : Proper (() ==> ()) (client γ).
Proof. apply (ne_proper _). Qed. Proof. apply (ne_proper _). Qed.
Lemma contribution_init : (|==> γ, server γ 0 ε)%I. Lemma contribution_init : |==> γ, server γ 0 ε.
Proof. Proof.
iMod (own_alloc ( (Some (Cinr (Excl ()))) (Some (Cinr (Excl ()))))) iMod (own_alloc ( (Some (Cinr (Excl ()))) (Some (Cinr (Excl ())))))
as (γ) "[Hγ Hγ']"; first by apply auth_both_valid_2. as (γ) "[Hγ Hγ']"; first by apply auth_both_valid_2.
...@@ -152,7 +152,7 @@ Section contribution. ...@@ -152,7 +152,7 @@ Section contribution.
(** Derived *) (** Derived *)
Lemma contribution_init_pow n : Lemma contribution_init_pow n :
(|==> γ, server γ n ε [] replicate n (client γ ε))%I. |==> γ, server γ n ε [] replicate n (client γ ε).
Proof. Proof.
iMod (contribution_init) as (γ) "Hs". iExists γ. iMod (contribution_init) as (γ) "Hs". iExists γ.
iInduction n as [|n] "IH"; simpl; first by iFrame. iInduction n as [|n] "IH"; simpl; first by iFrame.
......
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