Commit e57bb39a authored by Dan Frumin's avatar Dan Frumin

Fix the leibnizequiv problem

parent 4c08cbe9
From iris.algebra Require Import auth.
From iris.base_logic.lib Require Import auth.
From iris.program_logic Require Import adequacy ectxi_language.
From iris_logrel.F_mu_ref_conc Require Import lang tactics rel_tactics soundness_binary notation relational_properties hax.
From iris_logrel.F_mu_ref_conc.examples Require Import lock.
......@@ -315,7 +316,7 @@ Section Full_refinement.
end.
(* α. (α Unit) * (Unit Unit + α) * ((α Unit) Unit) *)
Lemma FG_CG_stack_refinement`{auth.authG Σ stackUR, logrelG Σ} Δ Γ :
Lemma FG_CG_stack_refinement `{authG Σ stackUR, logrelG Σ} Δ Γ :
{,;Δ;Γ} FG_stack log CG_stack : TForall (TProd (TProd
(TArrow (TVar 0) TUnit)
(TArrow TUnit (TSum TUnit (TVar 0))))
......@@ -349,7 +350,7 @@ Section Full_refinement.
change H with (@stack_inG _ istkG).
clearbody istkG. clear γ H1.
iAssert (@stack_owns _ istkG _ ) with "[Hemp]" as "Hoe".
{ rewrite /stack_owns big_sepM_empty.
{ rewrite /stack_owns big_sepM_empty fmap_empty.
iFrame "Hemp". }
iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
iAssert (StackLink τi (#istk, FoldV (InjLV (LitV Unit)))) with "[Histk]" as "#HLK".
......
......@@ -86,27 +86,28 @@ Section Rules.
Context `{logrelG Σ}.
Definition stack_owns (h : stackUR) : iProp Σ :=
(own stack_name ( h)
[ map] l v h, match agree_car v with
| v'::_ => l ↦ᵢ v'
| _ => False
end)%I.
Definition stack_owns (h : gmap loc val) : iProp Σ :=
(own stack_name ( (to_agree <$> h : stackUR))
[ map] l v h, l ↦ᵢ v)%I.
Lemma stack_owns_alloc h l v :
stack_owns h l ↦ᵢ v == stack_owns (<[l := to_agree v]> h) l ↦ˢᵗᵏ v.
stack_owns h l ↦ᵢ v == stack_owns (<[l := v]> h) l ↦ˢᵗᵏ v.
Proof.
iIntros "[[Hown Hall] Hl]".
iDestruct (own_valid with "Hown") as %Hvalid.
destruct (h !! l) as [av|] eqn:?.
iDestruct (own_valid with "Hown") as %Hvalid.
destruct (h !! l) as [av|] eqn:Hhl.
{ iDestruct (big_sepM_lookup with "Hall") as "Hl'"; first done.
destruct av as [[|v' av] Hav]; simpl; first by iExFalso.
by iDestruct (@mapsto_valid_2 loc val with "Hl Hl'") as %[]. }
iMod (own_update with "Hown") as "[Hown Hl']".
{ by eapply auth_update_alloc,
(alloc_singleton_local_update _ l (to_agree v)). }
iModIntro. rewrite /stack_owns. iFrame "Hown Hl'".
iApply big_sepM_insert; simpl; try iFrame; auto.
iDestruct (@mapsto_valid_2 loc val with "Hl Hl'") as %Hval.
cbv in Hval. exfalso; by apply Hval. }
{ iMod (own_update with "Hown") as "[Hown Hl']".
eapply auth_update_alloc.
eapply (alloc_singleton_local_update _ l (to_agree v)).
- rewrite lookup_fmap Hhl. by compute.
- by compute.
- iModIntro. rewrite /stack_owns. rewrite fmap_insert.
iFrame "Hown Hl'".
iApply big_sepM_insert; eauto.
by iFrame. }
Qed.
Lemma stack_owns_open_close h l v :
......@@ -114,17 +115,15 @@ Section Rules.
Proof.
iIntros "[Howns Hls] Hl".
iDestruct (own_valid_2 with "Howns Hl")
as %[[av' [Hl Hav']]%singleton_included ?]%auth_valid_discrete_2.
eapply leibniz_equiv in Hl.
iDestruct (big_sepM_lookup_acc with "Hls") as "[Hl' Hclose]"; first done.
destruct av' as [[|v' av'] ?]; first by iExFalso. simpl.
assert (v = v') as <-.
{ apply Some_included in Hav'.
destruct Hav' as [Hav' | Hav'%agree_included]; eapply leibniz_equiv in Hav'.
- by inversion Hav'.
- by inversion Hav'. }
iIntros "{$Hl'} Hl'". rewrite /stack_owns. iFrame "Howns". by iApply "Hclose".
Admitted.
as %[[? [[av [Hav ?]]%equiv_Some_inv_r' Hav']]%singleton_included ?]%auth_valid_discrete_2.
setoid_subst.
apply -> Some_included_total in Hav'.
move: Hav. rewrite lookup_fmap fmap_Some.
move=> [v' [Hl Hav]]; subst.
apply to_agree_included in Hav'; setoid_subst.
iDestruct (big_sepM_lookup_acc with "Hls") as "[$ Hclose]"; first done.
iIntros "Hl'". rewrite /stack_owns. iFrame "Howns". by iApply "Hclose".
Qed.
Lemma stack_owns_later_open_close h l v :
stack_owns h - l ↦ˢᵗᵏ v - (l ↦ᵢ v (l ↦ᵢ v - stack_owns h)).
......
......@@ -6,7 +6,7 @@ Class PureExec (P : Prop) (e1 e2 : expr) := {
}.
(* DF: Some tactics will loop pretty badly and consume lots of memory if you make this an instance *)
Lemma PureExec_Closed P e1 e2 `{Hcl : Closed X e1} `{HP: PureExec P e1 e2} : P -> Closed X e2.
Lemma PureExec_Closed P e1 e2 `{HP: PureExec P e1 e2} `{Hcl : Closed X e1} : P -> Closed X e2.
Proof.
destruct HP as [Hpure Hstep].
intros p. specialize (Hpure p). specialize (Hstep p).
......
......@@ -277,11 +277,7 @@ Hint Extern 1 (Closed _ _) => solve_closed2 : typeclass_instances.
(* Hint Extern 1 (Closed _ _) => solve_closed2. *)
(* DF: I used it for automatically discharging assumptions for the PureExec instances *)
Ltac lookup_to_val :=
lazymatch goal with
| [ H: to_val ?e = Some ?v |- to_val ?e = Some _ ] => apply H
end.
Hint Extern 1 (to_val _ = Some _) => lookup_to_val : typeclass_instances.
Hint Extern 1 (to_val _ = Some _) => eassumption : typeclass_instances.
Ltac simpl_subst :=
cbn[subst'];
......
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