Commit ef354c38 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Lifted stype over OFEs. Fixed residuals in channel.v

parent 1a47979d
......@@ -4,4 +4,3 @@ theories/list.v
theories/auth_excl.v
theories/typing.v
theories/channel.v
theories/logrel.v
\ No newline at end of file
......@@ -32,11 +32,7 @@ Section auth_excl.
iDestruct (own_valid_2 with "Hauth Hfrag") as %Hvalid.
apply auth_valid_discrete_2 in Hvalid.
destruct Hvalid as [Hincl _].
apply Excl_included in Hincl.
unfold to_auth_excl.
rewrite Hincl.
iFrame.
eauto.
by apply Excl_included in Hincl.
Qed.
Lemma excl_update γ x y z :
......
......@@ -164,7 +164,7 @@ Section channel.
wp_load. wp_apply (lsnoc_spec with "Hlvs"). iIntros (lhd' Hlvs).
wp_bind (_ <- _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
iDestruct (excl_eq with "Hvs Hchan") as %->.
iDestruct (excl_eq with "Hvs Hchan") as %->%leibniz_equiv.
iMod (excl_update _ _ _ (vs ++ [v]) with "Hvs Hchan") as "[Hvs Hchan]".
wp_store. iMod ("HΦ" with "Hchan") as "HΦ".
iModIntro.
......@@ -193,7 +193,7 @@ Section channel.
wp_bind (! _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
wp_load.
iDestruct (excl_eq with "Hvs Hchan") as %->.
iDestruct (excl_eq with "Hvs Hchan") as %->%leibniz_equiv.
destruct vs as [|v vs]; simpl.
- iDestruct "Hlvs" as %->.
iDestruct "HΦ" as "[HΦ _]".
......
......@@ -71,18 +71,26 @@ Section stype_ofe.
+ intros st. induction st; constructor; repeat intro; auto.
+ intros st1 st2. induction 1; constructor; repeat intro; auto.
symmetry; auto.
+ intros st1 st2 st3 H1 H2. revert H1. revert st1.
induction 1.
* inversion H2. constructor.
* inversion H2. eauto.
admit.
- intros n st1 st2. induction 1; constructor; auto.
Admitted.
+ intros st1 st2 st3 H1 H2.
revert H2. revert st3.
induction H1 as [| a P1 P2 st1 st2 HP Hst12 IH]=> //.
inversion 1. subst. constructor.
** by transitivity P2.
** intros v. by apply IH.
- intros n st1 st2. induction 1; constructor.
+ intros v. apply dist_S. apply H.
+ intros v. apply H1.
Qed.
Canonical Structure stypeC : ofeT := OfeT (stype A) stype_ofe_mixin.
Global Instance TSR_stype_ne a n :
Proper (pointwise_relation _ (dist n) ==> pointwise_relation _ (dist n) ==> dist n) (TSR a).
Proof. Admitted.
Proof.
intros P1 P2 HP st1 st2 Hst.
constructor.
- apply HP.
- intros v. apply Hst.
Qed.
Global Instance TSR_stype_proper a :
Proper (pointwise_relation _ () ==> pointwise_relation _ () ==> ()) (TSR a).
Proof.
......@@ -91,14 +99,25 @@ Section stype_ofe.
Qed.
Global Instance dual_stype_ne : NonExpansive dual_stype.
Proof. Admitted.
Proof.
intros n. induction 1 as [| a P1 P2 st1 st2 HP Hst IH].
- constructor.
- destruct a.
+ constructor. apply HP. intros v. apply IH.
+ constructor. apply HP. intros v. apply IH.
Qed.
Global Instance dual_stype_proper : Proper (() ==> ()) dual_stype.
Proof. apply (ne_proper _). Qed.
Global Instance dual_stype_involutive : Involutive () dual_stype.
Proof.
intros st.
Admitted.
induction st.
- constructor.
- simpl. destruct a.
+ constructor. reflexivity. intros v. apply H.
+ constructor. reflexivity. intros v. apply H.
Qed.
End stype_ofe.
Fixpoint stype_map {A B} (f : A B) (st : stype A) : stype B :=
......@@ -109,26 +128,38 @@ Fixpoint stype_map {A B} (f : A → B) (st : stype A) : stype B :=
Lemma stype_map_ext_ne {A} {B : ofeT} (f g : A B) (st : stype A) n :
( x, f x {n} g x) stype_map f st {n} stype_map g st.
Proof.
intros Hf. induction st; simpl.
Admitted.
intros Hf. induction st as [| a P st IH]; constructor.
- intros v. apply Hf.
- intros v. apply IH.
Qed.
Lemma stype_map_ext {A} {B : ofeT} (f g : A B) (st : stype A) :
( x, f x g x) stype_map f st stype_map g st.
Proof.
intros Hf. induction st; simpl.
Admitted.
Instance styope_map_ne {A B : ofeT} (f : A B) n:
intros Hf. apply equiv_dist.
intros n. apply stype_map_ext_ne.
intros x. apply equiv_dist.
apply Hf.
Qed.
Instance stype_map_ne {A B : ofeT} (f : A B) n:
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (stype_map f).
Proof.
intros Hf st1 st2. induction 1; simpl; constructor.
Admitted.
intros Hf st1 st2. induction 1 as [| a P1 P2 st1 st2 HP Hst IH]; constructor.
- intros v. f_equiv. apply HP.
- intros v. apply IH.
Qed.
Lemma stype_fmap_id {A : ofeT} (st : stype A) : stype_map id st st.
Proof.
Admitted.
Check @list_fmap_compose.
induction st as [| a P st IH]; constructor.
- intros v. reflexivity.
- intros v. apply IH.
Qed.
Lemma stype_fmap_compose {A B C : ofeT} (f : A B) (g : B C) st :
stype_map (g f) st stype_map g (stype_map f st).
Proof.
Admitted.
induction st as [| a P st IH]; constructor.
- intros v. reflexivity.
- intros v. apply IH.
Qed.
Definition stypeC_map {A B} (f : A -n> B) : stypeC A -n> stypeC B :=
CofeMor (stype_map f : stypeC A stypeC B).
......
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