Commit 791a505d authored by Ralf Jung's avatar Ralf Jung

port to gen_proofmode

parent 3aa2c6c8
Pipeline #10266 passed with stage
in 10 minutes
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2018-06-23.0.a6e581d0") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-06-21.3.94b2c6c1") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -57,10 +57,12 @@ Proof.
iDestruct 1 as (x) "[#Hγ Hx]"; iDestruct 1 as (x') "[#Hγ' Hx']".
iAssert ( (x x'))%I as "Hxx".
{ iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
rewrite own_valid csum_validI /= agree_validI agree_equivI uPred.later_equivI /=.
rewrite own_valid csum_validI /= agree_validI agree_equivI bi.later_equivI /=.
rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
rewrite (ne_proper (cFunctor_map F) (cid, cid) (_ _, _ _)); last first.
{ by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
assert (HF : cFunctor_map F (cid, cid) cFunctor_map F (iProp_fold (Σ:=Σ) iProp_unfold, iProp_fold (Σ:=Σ) iProp_unfold)).
{ apply ne_proper; first by apply _.
by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
rewrite (HF x). rewrite (HF x').
rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
iNext. iRewrite -"Hxx" in "Hx'".
iExists x; iFrame "Hγ". iApply (Ψ_join with "Hx Hx'").
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From stdpp Require Import functions.
From iris.base_logic Require Import big_op lib.saved_prop lib.sts.
From iris.base_logic Require Import lib.saved_prop lib.sts.
From iris.heap_lang Require Import proofmode.
From iris_examples.barrier Require Export barrier.
From iris_examples.barrier Require Import protocol.
......@@ -148,7 +148,7 @@ Proof.
return to the client *)
iDestruct "Hr" as (Ψ) "[HΨ Hsp]".
iDestruct (big_opS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
iAssert ( Ψ i [ set] j I {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
iAssert ( (Ψ i [ set] j I {[i]}, Ψ j))%I with "[HΨ]" as "[HΨ HΨ']".
{ iNext. iApply (big_opS_delete _ _ i); first done. by iApply "HΨ". }
iMod ("Hclose" $! (State High (I {[ i ]})) with "[HΨ' Hl Hsp]").
{ iSplit; [iPureIntro; by eauto using wait_step|].
......
......@@ -91,7 +91,7 @@ Section stack_works.
- The resources for the successful and failing pop must be disjoint.
Instead, there should be a normal conjunction between them.
Open question: How does this relate to a logically atomic spec? *)
Theorem stack_works ι P Q Q' Q'' Φ :
Theorem stack_works ι P Q Q' Q'' (Φ : val iProp Σ) :
( (f f : val),
((( v vs, P (v :: vs) ={⊤∖↑ι}= Q v P vs) (* pop *)
(P [] ={⊤∖↑ι}= Q' P []) -
......
......@@ -144,7 +144,7 @@ Section stack_works.
Qed.
(* Whole-stack invariant (P). *)
Theorem stack_works {channelG0 : channelG Σ} N P Q Q' Q'' Φ :
Theorem stack_works {channelG0 : channelG Σ} N P Q Q' Q'' (Φ : val iProp Σ) :
( (f f : val),
(((( v vs, P (v :: vs) ={ N}= Q v P vs)
(P [] ={ N}= Q' P []) -
......
......@@ -76,7 +76,7 @@ Section proof.
Lemma bag_contents_agree γb X Y :
bag_contents γb X - bag_contents γb Y - X = Y.
Proof.
rewrite /bag_contents. apply uPred.wand_intro_r.
rewrite /bag_contents. apply bi.wand_intro_r.
rewrite -own_op own_valid uPred.discrete_valid.
f_equiv=> /=. rewrite pair_op.
by intros [_ ?%agree_op_invL'].
......
......@@ -3,9 +3,9 @@
<http://www.kasv.dk/articles/hocap-ext.pdf>
*)
From iris.heap_lang Require Import proofmode notation.
From iris.bi.lib Require Import fractional.
From iris.algebra Require Import cmra agree frac csum excl.
From iris.heap_lang.lib Require Import assert.
From iris.base_logic.lib Require Import fractional.
From iris_examples.hocap Require Export abstract_bag shared_bag lib.oneshot.
Set Default Proof Using "Type".
......@@ -208,11 +208,11 @@ Section contents.
( (body bag : val), r = (body, bag)%V
bagS b (N.@"bag") (λ x y, γ γ', isTask (body,x) γ γ' y P Q) γ bag
r a: val, (runner γ P Q r P a - WP body r a {{ v, Q a v }}))%I.
Proof. rewrite /runner. by rewrite {1}fixpoint_unfold. Qed.
Proof. rewrite /runner. by rewrite {1}(fixpoint_unfold (pre_runner _ _ _) r). Qed.
Global Instance runner_persistent γ r P Q :
Persistent (runner γ P Q r).
Proof. rewrite /runner fixpoint_unfold. apply _. Qed.
Proof. rewrite /runner (fixpoint_unfold (pre_runner _ _ _) r). apply _. Qed.
Lemma newTask_spec γb (r a : val) P (Q : val val iProp Σ) :
{{{ runner γb P Q r P a }}}
......@@ -231,14 +231,13 @@ Section contents.
iFrame. iSplitL; iExists _,_,_; iFrame "Hinv"; eauto.
Qed.
Lemma task_Join_spec γb γ γ' (te : expr) (r t a : val) P Q
`{!IntoVal te t}:
Lemma task_Join_spec γb γ γ' (te : expr) (r t a : val) P Q :
IntoVal te t
{{{ runner γb P Q r task γ γ' t a P Q }}}
task_Join te
{{{ res, RET res; Q a res }}}.
Proof.
iIntros (Φ) "[#Hrunner Htask] HΦ".
rewrite -(of_to_val te t into_val).
iIntros (<- Φ) "[#Hrunner Htask] HΦ".
iLöb as "IH".
rewrite {2}/task_Join.
iDestruct "Htask" as (r' state res) "(% & Htoken & #Htask)". simplify_eq.
......@@ -386,16 +385,14 @@ Section contents.
- iNext. by iApply runner_runTasks_spec.
Qed.
Lemma newRunner_spec P Q (fe ne : expr) (f : val) (n : nat)
`{!IntoVal fe f} `{!IntoVal ne (#n)}:
Lemma newRunner_spec P Q (fe ne : expr) (f : val) (n : nat) :
IntoVal fe f IntoVal ne (#n)
{{{ (γ: name Σ b) (r: val),
a: val, (runner γ P Q r P a - WP f r a {{ v, Q a v }}) }}}
newRunner fe ne
{{{ γb r, RET r; runner γb P Q r }}}.
Proof.
iIntros (Φ) "#Hf HΦ".
rewrite -(of_to_val fe f into_val).
rewrite -(of_to_val ne #n into_val).
iIntros (<- <- Φ) "#Hf HΦ".
unfold newRunner. iApply wp_fupd.
repeat wp_pure _.
wp_bind (newBag b #()).
......@@ -408,15 +405,13 @@ Section contents.
iNext. iIntros (r) "Hr". by iApply "HΦ".
Qed.
Lemma runner_Fork_spec γb (re ae:expr) (r a:val) P Q
`{!IntoVal re r} `{!IntoVal ae a}:
Lemma runner_Fork_spec γb (re ae:expr) (r a:val) P Q :
IntoVal re r IntoVal ae a
{{{ runner γb P Q r P a }}}
runner_Fork re ae
{{{ γ γ' t, RET t; task γ γ' t a P Q }}}.
Proof.
iIntros (Φ) "[#Hrunner HP] HΦ".
rewrite -(of_to_val re r into_val).
rewrite -(of_to_val ae a into_val).
iIntros (<- <- Φ) "[#Hrunner HP] HΦ".
rewrite /runner_Fork runner_unfold.
iDestruct "Hrunner" as (body bag) "(% & #Hbag & #Hbody)". simplify_eq.
Local Opaque newTask.
......
......@@ -97,7 +97,7 @@ Section proof.
Lemma bag_contents_agree γb X Y :
bag_contents γb X - bag_contents γb Y - X = Y.
Proof.
rewrite /bag_contents. apply uPred.wand_intro_r.
rewrite /bag_contents. apply bi.wand_intro_r.
rewrite -own_op own_valid uPred.discrete_valid.
f_equiv=> /=. rewrite pair_op.
by intros [_ ?%agree_op_invL'].
......
From iris.proofmode Require Import tactics.
From iris.bi.lib Require Import fractional.
From iris.algebra Require Import cmra agree frac csum.
From iris.base_logic.lib Require Import fractional.
From iris_examples.hocap Require Export abstract_bag shared_bag.
Set Default Proof Using "Type".
......
......@@ -10,7 +10,6 @@ From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import cmra agree frac csum excl.
From iris.heap_lang.lib Require Import lock spin_lock.
From iris.base_logic.lib Require Import fractional.
From iris_examples.hocap Require Import abstract_bag shared_bag concurrent_runners.
Section contents.
......
......@@ -70,7 +70,7 @@ Section proof.
iInv NI as (X) "[>Hb2 HPs]" "Hcl".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (bag_contents_update b Y with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
rewrite big_sepMS_union uPred.later_sep big_sepMS_singleton.
rewrite big_sepMS_union bi.later_sep big_sepMS_singleton.
iDestruct "HPs" as "[HP HPs]".
iMod ("Hcl" with "[-HP Hb1]") as "_".
{ iNext. iExists _; iFrame. }
......
......@@ -43,7 +43,7 @@ Section ccounter.
Lemma is_ccounter_op γ₁ γ₂ q1 q2 (n1 n2 : nat) :
is_ccounter γ₁ γ₂ (q1 + q2) (n1 + n2)%nat ⊣⊢ is_ccounter γ₁ γ₂ q1 n1 is_ccounter γ₁ γ₂ q2 n2.
Proof.
apply uPred.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
apply bi.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
- iIntros "[? #?]".
iFrame "#"; iFrame.
- iIntros "[[? #?] [? _]]".
......
......@@ -593,7 +593,7 @@ Section ccounter.
Lemma is_ccounter_op γ q1 q2 (n1 n2 : nat) :
is_ccounter γ (q1 + q2) (n1 + n2)%nat ⊣⊢ is_ccounter γ q1 n1 is_ccounter γ q2 n2.
Proof.
apply uPred.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
apply bi.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
- iIntros "[? #?]".
iFrame "#"; iFrame.
- iIntros "[[? #?] [? _]]".
......
......@@ -304,8 +304,8 @@ Qed.
The specifications are explained in the Iris Lecture Notes. *)
Lemma foldr_spec_PI P I (f a hd : val) (e_f e_a e_hd : expr) (xs : list val)
`{Hef : !IntoVal e_f f} `{Hea : !IntoVal e_a a} `{Hehd : !IntoVal e_hd hd} :
Lemma foldr_spec_PI P I (f a hd : val) (e_f e_a e_hd : expr) (xs : list val) :
IntoVal e_f f IntoVal e_a a IntoVal e_hd hd
{{{ ( (x a' : val) (ys : list val),
{{{ P x I ys a'}}}
e_f (x, a')
......@@ -320,10 +320,7 @@ Lemma foldr_spec_PI P I (f a hd : val) (e_f e_a e_hd : expr) (xs : list val)
I xs r
}}}.
Proof.
apply of_to_val in Hef as <-.
apply of_to_val in Hea as <-.
apply of_to_val in Hehd as <-.
iIntros (ϕ) "(#H_f & H_isList & H_Px & H_Iempty) H_inv".
iIntros (<- <- <- ϕ) "(#H_f & H_isList & H_Px & H_Iempty) H_inv".
iInduction xs as [|x xs'] "IH" forall (ϕ a hd); wp_rec; do 2 wp_let; iSimplifyEq.
- wp_match. iApply "H_inv". eauto.
- iDestruct "H_isList" as (l hd') "[% [H_l H_isList]]".
......@@ -338,8 +335,8 @@ Proof.
iExists l, hd'. by iFrame.
Qed.
Lemma foldr_spec_PPI P I (f a hd : val ) (e_f e_a e_hd : expr) (xs : list val)
`{Hef : !IntoVal e_f f} `{Hea : !IntoVal e_a a} `{Hehd : !IntoVal e_hd hd} :
Lemma foldr_spec_PPI P I (f a hd : val ) (e_f e_a e_hd : expr) (xs : list val) :
IntoVal e_f f IntoVal e_a a IntoVal e_hd hd
{{{ ( (x a' : val) (ys : list val),
{{{ P x I ys a'}}}
e_f (x, a')
......@@ -353,10 +350,7 @@ Lemma foldr_spec_PPI P I (f a hd : val ) (e_f e_a e_hd : expr) (xs : list val)
I xs r
}}}.
Proof.
apply of_to_val in Hef as <-.
apply of_to_val in Hea as <-.
apply of_to_val in Hehd as <-.
iIntros (ϕ) "(#H_f & H_isList & H_Iempty) H_inv".
iIntros (<- <- <- ϕ) "(#H_f & H_isList & H_Iempty) H_inv".
rewrite about_isList. iDestruct "H_isList" as "(H_isList & H_Pxs)".
iApply (foldr_spec_PI with "[-H_inv]").
- iFrame. by iFrame "H_f".
......@@ -426,8 +420,8 @@ Proof.
Qed.
Lemma map_spec P Q (e_f e_hd : expr) (f hd : val) (xs : list val)
`{Hef : !IntoVal e_f f} `{Hehd : !IntoVal e_hd hd} :
Lemma map_spec P Q (e_f e_hd : expr) (f hd : val) (xs : list val) :
IntoVal e_f f IntoVal e_hd hd
{{{
is_list hd xs
( (x : val), {{{ P x }}}
......@@ -442,9 +436,7 @@ Lemma map_spec P Q (e_f e_hd : expr) (f hd : val) (xs : list val)
List.length ys = List.length xs
}}}.
Proof.
apply of_to_val in Hef as <-.
apply of_to_val in Hehd as <-.
iIntros (ϕ) "[H_is_list [#H1 H_P_xs]] H_ϕ".
iIntros (<- <- ϕ) "[H_is_list [#H1 H_P_xs]] H_ϕ".
do 3 (wp_pure _).
iApply (foldr_spec_PI
P
......
......@@ -5,7 +5,7 @@ From iris.heap_lang Require Export lang proofmode notation.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import agree frac frac_auth.
From iris.base_logic.lib Require Import fractional.
From iris.bi.lib Require Import fractional.
From iris.heap_lang.lib Require Import par.
......@@ -39,9 +39,9 @@ Section cnt_model.
Definition makeElem (q : Qp) (m : Z) : cntCmra := (q, to_agree m).
Notation "γ ⤇[ q ] m" := (own γ (makeElem q m))
(at level 20, q at level 50, format "γ ⤇[ q ] m") : uPred_scope.
(at level 20, q at level 50, format "γ ⤇[ q ] m") : bi_scope.
Notation "γ ⤇½ m" := (own γ (makeElem (1/2) m))
(at level 20, format "γ ⤇½ m") : uPred_scope.
(at level 20, format "γ ⤇½ m") : bi_scope.
Global Instance makeElem_fractional γ m: Fractional (λ q, γ [q] m)%I.
Proof.
......@@ -98,9 +98,9 @@ Section cnt_model.
End cnt_model.
Notation "γ ⤇[ q ] m" := (own γ (makeElem q m))
(at level 20, q at level 50, format "γ ⤇[ q ] m") : uPred_scope.
(at level 20, q at level 50, format "γ ⤇[ q ] m") : bi_scope.
Notation "γ ⤇½ m" := (own γ (makeElem (1/2) m))
(at level 20, format "γ ⤇½ m") : uPred_scope.
(at level 20, format "γ ⤇½ m") : bi_scope.
Section cnt_spec.
Context `{!heapG Σ, !cntG Σ} (N : namespace).
......@@ -158,7 +158,7 @@ Section cnt_spec.
{{{ Cnt γ P }}} incr # @ E {{{ (m : Z), RET #m; Cnt γ Q m}}}.
Proof.
iIntros (Hsubset) "#HVS".
iIntros (Φ) "!# [HInc HP] HCont".
iIntros (Φ) "!# [#HInc HP] HCont".
iLöb as "IH".
wp_rec.
wp_bind (! _)%E.
......@@ -178,13 +178,13 @@ Section cnt_spec.
{ iNext; iExists _; iFrame. }
iModIntro.
wp_if.
iApply "HCont"; iFrame.
iApply "HCont"; by iFrame.
- wp_cas_fail.
iMod ("HClose" with "[Hpt Hown]") as "_".
{ iNext; iExists _; iFrame. }
iModIntro.
wp_if.
iApply ("IH" with "HInc HP HCont").
iApply ("IH" with "HP HCont").
Qed.
Theorem wk_incr_spec (γ : gname) (E : coPset) (P Q : iProp Σ) ( : loc) (n : Z) (q : Qp):
......@@ -193,7 +193,7 @@ Section cnt_spec.
{{{ Cnt γ γ [q] n P}}} wk_incr # @ E {{{ RET #(); Cnt γ Q}}}.
Proof.
iIntros (Hsubset) "#HVS".
iIntros (Φ) "!# [HInc [Hγ HP]] HCont".
iIntros (Φ) "!# [#HInc [Hγ HP]] HCont".
wp_lam.
wp_bind (! _)%E.
iInv (N .@ "internal") as (m) "[>Hpt >Hown]" "HClose".
......@@ -211,7 +211,7 @@ Section cnt_spec.
iMod ("HClose" with "[Hpt Hown]") as "_".
{ iNext; iExists _; iFrame. }
iModIntro.
iApply "HCont"; iFrame.
iApply "HCont"; by iFrame.
Qed.
Theorem wk_incr_spec' (γ : gname) (E : coPset) (P Q : iProp Σ) ( : loc) (n : Z) (q : Qp):
......
......@@ -50,8 +50,8 @@ Definition myrec : val :=
(* Here is the specification for the recursion through the store function.
See the Iris Lecture Notes for an in-depth discussion of both the specification and
the proof. *)
Lemma myrec_spec (P: val -> iProp Σ) (Q: val -> val -> iProp Σ) (F v1: val) (e_F e_v : expr)
`{HeF : !IntoVal e_F F} `{Hev1 : !IntoVal e_v v1}:
Lemma myrec_spec (P: val -> iProp Σ) (Q: val -> val -> iProp Σ) (F v1: val) (e_F e_v : expr) :
IntoVal e_F F IntoVal e_v v1
{{{
( e_f:expr,f : val, v2:val, IntoVal e_f f - {{{( v3 :val, {{{P v3 }}} e_f v3 {{{u, RET u; Q u v3 }}})
P v2 }}}
......@@ -62,9 +62,7 @@ Lemma myrec_spec (P: val -> iProp Σ) (Q: val -> val -> iProp Σ) (F v1: val) (e
myrec e_F e_v
{{{u, RET u; Q u v1}}}.
Proof.
apply of_to_val in HeF as <-.
apply of_to_val in Hev1 as <-.
iIntros (ϕ) "[#H P] Q".
iIntros (<- <- ϕ) "[#H P] Q".
wp_lam.
wp_alloc r as "r".
wp_let.
......@@ -183,11 +181,10 @@ Section factorial_client.
myfac n
{{{v, RET v; v = #(fac_int n')}}}.
Proof.
iIntros (H%of_to_val Hleq Φ) "_ ret"; simplify_eq.
iIntros (<- Hleq Φ) "_ ret"; simplify_eq.
iApply (myrec_spec (fun v => ⌜∃m' : Z, 0 m' to_val v = Some #m'%I)
(fun u => fun v => ⌜∃m' : Z, to_val v = Some #m' u = #(fac_int m')%I)).
- iSplit; last eauto. iIntros (e_f f v) "%". iAlways. iIntros (Φ') "spec_f ret".
apply of_to_val in a as <-.
- iSplit; last eauto. iIntros (e_f f v <-). iAlways. iIntros (Φ') "spec_f ret".
wp_lam. wp_lam. iDestruct "spec_f" as "[spec_f %]".
destruct H as [m' [Hleqm' Heq%of_to_val]]; simplify_eq.
wp_binop.
......
......@@ -2,7 +2,6 @@ From iris_examples.logrel.F_mu Require Export logrel.
From iris.program_logic Require Import lifting.
From iris.proofmode Require Import tactics.
From iris_examples.logrel.F_mu Require Import rules.
From iris.base_logic Require Export big_op.
Definition log_typed `{irisG F_mu_lang Σ} (Γ : list type) (e : expr) (τ : type) := Δ vs,
env_Persistent Δ
......@@ -74,12 +73,12 @@ Section fundamental.
iIntros (w) "?". by rewrite interp_subst.
- (* Fold *)
smart_wp_bind FoldCtx v "#Hv" IHtyped; cbn. iApply wp_value.
rewrite /= -interp_subst fixpoint_unfold /=.
rewrite /= -interp_subst fixpoint_interp_rec1_eq /=.
iAlways; eauto.
- (* Unfold *)
iApply (wp_bind (fill [UnfoldCtx]));
iApply wp_wand_l; iSplitL; [|iApply IHtyped; trivial].
iIntros (v) "#Hv". rewrite /= fixpoint_unfold.
iIntros (v) "#Hv /=". rewrite /= fixpoint_interp_rec1_eq.
change (fixpoint _) with ( TRec τ Δ); simpl.
iDestruct "Hv" as (w) "#[% Hw]"; subst; simpl.
iApply wp_pure_step_later; auto. iApply wp_value; iNext.
......
......@@ -181,10 +181,10 @@ Export F_mu.
Hint Extern 20 (PureExec _ _ _) => progress simpl : typeclass_instances.
Hint Extern 5 (IntoVal _ _) => eapply to_of_val : typeclass_instances.
Hint Extern 5 (IntoVal _ _) => eapply of_to_val; fast_done : typeclass_instances.
Hint Extern 10 (IntoVal _ _) =>
rewrite /IntoVal /= ?to_of_val /=; eauto : typeclass_instances.
rewrite /IntoVal; eapply of_to_val; rewrite /= !to_of_val /=; solve [ eauto ] : typeclass_instances.
Hint Extern 5 (AsVal _) => eexists; eapply to_of_val : typeclass_instances.
Hint Extern 5 (AsVal _) => eexists; eapply of_to_val; fast_done : typeclass_instances.
Hint Extern 10 (AsVal _) =>
eexists; rewrite /IntoVal /= ?to_of_val /=; eauto : typeclass_instances.
\ No newline at end of file
eexists; rewrite /IntoVal; eapply of_to_val; rewrite /= !to_of_val /=; solve [ eauto ] : typeclass_instances.
......@@ -2,7 +2,6 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris_examples.logrel.F_mu Require Export lang typing.
From iris.algebra Require Import list.
From iris.base_logic Require Import big_op.
Import uPred.
(** interp : is a unary logical relation. *)
......@@ -15,7 +14,7 @@ Section logrel.
Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
from_option id (cconst True)%I (Δ !! x).
Solve Obligations with solve_proper_alt.
Solve Obligations with solve_proper.
Definition interp_unit : listC D -n> D := λne Δ w, (w = UnitV)%I.
......@@ -48,6 +47,10 @@ Section logrel.
(interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
Proof. by solve_contractive. Qed.
Lemma fixpoint_interp_rec1_eq (interp : listC D -n> D) Δ x :
fixpoint (interp_rec1 interp Δ) x interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.
Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
fixpoint (interp_rec1 interp Δ).
Next Obligation.
......@@ -88,7 +91,7 @@ Section logrel.
env_Persistent Δ Persistent ( τ Δ v) := _.
Proof.
revert v Δ; induction τ=> v Δ HΔ; simpl; try apply _.
rewrite /Persistent /interp_rec fixpoint_unfold /interp_rec1 /=.
rewrite /Persistent fixpoint_interp_rec1_eq /interp_rec1 /= intuitionistically_into_persistently.
by apply persistently_intro'.
Qed.
Global Instance interp_env_base_persistent Δ Γ vs :
......@@ -112,7 +115,9 @@ Section logrel.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
(* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
......@@ -129,14 +134,17 @@ Section logrel.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
(* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..].
destruct (x - length Δ1) as [|n] eqn:?; simpl.
case EQ: (x - length Δ1) => [|n]; simpl.
{ symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
Lemma interp_subst Δ2 τ τ' : τ ( τ' Δ2 :: Δ2) τ.[τ'/] Δ2.
Lemma interp_subst Δ2 τ τ' v : τ ( τ' Δ2 :: Δ2) v τ.[τ'/] Δ2 v.
Proof. apply (interp_subst_up []). Qed.
Lemma interp_env_length Δ Γ vs : Γ * Δ vs length Γ = length vs.
......
......@@ -24,8 +24,8 @@ Section lang_rules.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec :=
unfold IntoVal, AsVal in *; subst;
repeat match goal with H : is_Some _ |- _ => destruct H as [??] end;
unfold IntoVal in *; subst;
repeat match goal with H : AsVal _ |- _ => destruct H as [??] end;
apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
Global Instance pure_lam e1 e2 `{!AsVal e2} :
......
......@@ -2,7 +2,6 @@ From iris_examples.logrel.F_mu_ref Require Export logrel.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import lifting.
From iris_examples.logrel.F_mu_ref Require Import rules.
From iris.base_logic Require Export big_op.
Definition log_typed `{heapG Σ} (Γ : list type) (e : expr) (τ : type) := Δ vs,
env_Persistent Δ
......@@ -28,11 +27,11 @@ Section fundamental.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHtyped1.
smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2.
iApply wp_value; eauto 10.
iApply wp_value. eauto 10.
- (* fst *)
smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
iApply wp_pure_step_later; auto; by iApply wp_value.
iApply wp_pure_step_later; auto. by iApply wp_value.
- (* snd *)
smart_wp_bind (SndCtx) v "# Hv" IHtyped; cbn.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
......@@ -73,12 +72,12 @@ Section fundamental.
iIntros (w) "?". by rewrite interp_subst.
- (* Fold *)
smart_wp_bind FoldCtx v "#Hv" IHtyped; cbn.
iApply wp_value. rewrite /= -interp_subst fixpoint_unfold /=.
iApply wp_value. rewrite /= -interp_subst fixpoint_interp_rec1_eq /=.
iAlways; eauto.
- (* Unfold *)
iApply (wp_bind (fill [UnfoldCtx]));
iApply wp_wand_l; iSplitL; [|iApply IHtyped; auto].
iIntros (v) "#Hv". rewrite /= fixpoint_unfold.
iIntros (v) "#Hv". rewrite /= fixpoint_interp_rec1_eq.
change (fixpoint _) with (interp (TRec τ) Δ); simpl.
iDestruct "Hv" as (w) "#[% Hw]"; subst.
iApply wp_pure_step_later; cbn; auto using to_of_val.
......
From iris_examples.logrel.F_mu_ref Require Export logrel_binary.
From iris.algebra Require Import list.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import lifting.
From iris_examples.logrel.F_mu_ref Require Import rules_binary.
From iris.base_logic Require Export big_op.
Section bin_log_def.
Context `{heapG Σ,cfgSG Σ}.
......@@ -216,7 +216,7 @@ Section fundamental.
iIntros (v); iDestruct 1 as (w) "[Hv #Hiv]".
iApply wp_value. repeat rewrite /= to_of_val; eauto.
iExists (FoldV w); iFrame "Hv".
rewrite fixpoint_unfold /= -interp_subst.
rewrite fixpoint_interp_rec1_eq /= -interp_subst.
iAlways; iExists (_, _); eauto.
Qed.
......@@ -229,7 +229,7 @@ Section fundamental.
[|iApply ('`IHHtyped _ _ _ (UnfoldCtx :: K));
rewrite ?fill_app; simpl; repeat iSplitR; trivial].
iIntros (v). iDestruct 1 as (v') "[Hw #Hiw]".
rewrite /= fixpoint_unfold /=.
rewrite /= fixpoint_interp_rec1_eq /=.
change (fixpoint _) with (interp (TRec τ) Δ).
iDestruct "Hiw" as ([w w']) "#[% Hiz]"; simplify_eq/=.
iMod (step_Fold _ _ K (of_val w') with "* [-]") as "Hz"; eauto.
......
......@@ -227,13 +227,13 @@ Export F_mu_ref.
Hint Extern 20 (PureExec _ _ _) => progress simpl : typeclass_instances.
Hint Extern 5 (IntoVal _ _) => eapply to_of_val : typeclass_instances.
Hint Extern 5 (IntoVal _ _) => eapply of_to_val; fast_done : typeclass_instances.
Hint Extern 10 (IntoVal _ _) =>
rewrite /IntoVal /= ?to_of_val /=; eauto : typeclass_instances.
rewrite /IntoVal; eapply of_to_val; rewrite /= !to_of_val /=; solve [ eauto ] : typeclass_instances.
Hint Extern 5 (AsVal _) => eexists; eapply to_of_val : typeclass_instances.
Hint Extern 5 (AsVal _) => eexists; eapply of_to_val; fast_done : typeclass_instances.
Hint Extern 10 (AsVal _) =>
eexists; rewrite /IntoVal /= ?to_of_val /=; eauto : typeclass_instances.
eexists; rewrite /IntoVal; eapply of_to_val; rewrite /= !to_of_val /=; solve [ eauto ] : typeclass_instances.
Definition is_atomic (e : expr) : Prop :=
match e with
......
......@@ -2,7 +2,6 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris_examples.logrel.F_mu_ref Require Export rules typing.
From iris.algebra Require Import list.
From iris.base_logic Require Import big_op.
Import uPred.
Definition logN : namespace := nroot .@ "logN".
......@@ -17,7 +16,7 @@ Section logrel.
Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
from_option id (cconst True)%I (Δ !! x).