Commit f0856ce4 authored by jihgfee's avatar jihgfee

Re-instated missing operator.

Moved Iris specific stuff into a utility file.
parent 2c2d38c5
......@@ -5,6 +5,7 @@ theories/utils/llist.v
theories/utils/compare.v
theories/utils/contribution.v
theories/utils/group.v
theories/utils/misc.v
theories/channel/channel.v
theories/channel/proto_model.v
theories/channel/proto_channel.v
......
......@@ -18,7 +18,7 @@ and [chan_own]:
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import excl auth list.
From actris.utils Require Import auth_excl llist.
From actris.utils Require Import auth_excl llist misc.
Set Default Proof Using "Type".
Inductive side := Left | Right.
......@@ -75,6 +75,7 @@ Proof.
|apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
Qed.
Section channel.
Context `{!heapG Σ, !chanG Σ} (N : namespace).
......@@ -126,9 +127,9 @@ Section channel.
wp_lam.
wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (lsγ) "[Hls Hls']".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (lsγ) "[Hls Hls']".
{ by apply auth_both_valid. }
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
{ by apply auth_both_valid. }
wp_apply (newlock_spec N ( ls rs,
llist sbi_internal_eq l ls own lsγ ( to_auth_excl ls)
......
......@@ -15,8 +15,7 @@ depends on the communicated value V and the dependent tail
propositions of the logic.
The type is defined as a solution to a recursive domain
equation, as it is self-referential under the guard of ▶.
*)
equation, as it is self-referential under the guard of ▶.*)
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
......
From iris.heap_lang Require Import notation.
Set Default Proof Using "Type".
(** MOVE TO IRIS *)
Global Instance fst_atomic a v1 v2 : Atomic a (Fst (v1,v2)%V).
Proof.
apply strongly_atomic_atomic, ectx_language_atomic;
[inversion 1; naive_solver
|apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
Qed.
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