Commit 1330e552 authored by Dan Frumin's avatar Dan Frumin

Make tp_ more general and rewrite fundamental_binary using tactics

Slightly generalize the way tac_tp_bind works and rewrite the
fundamental property for F_mu_ref_conc using tp_ tactics
parent 94117113
......@@ -94,7 +94,7 @@ Section fundamental.
smart_wp_bind (FstCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ j (K ++ [FstCtx])); cbn.
iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq.
iApply wp_fst; eauto. iNext.
tp_fst j; eauto.
tp_fst j; eauto. tp_normalise j. eauto.
Qed.
Lemma bin_log_related_snd Γ e e' τ1 τ2
......@@ -105,7 +105,7 @@ Section fundamental.
smart_wp_bind (SndCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ j (K ++ [SndCtx])); cbn.
iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq.
iApply wp_snd; eauto. iNext.
tp_snd j; eauto.
tp_snd j; eauto. tp_normalise j; eauto.
Qed.
Lemma bin_log_related_injl Γ e e' τ1 τ2
......@@ -147,14 +147,14 @@ Section fundamental.
iDestruct "Hiv" as "[Hiv|Hiv]";
iDestruct "Hiv" as ([w w']) "[% Hw]"; simplify_eq.
- iApply fupd_wp.
tp_case_inl j; eauto.
tp_case_inl j; eauto; tp_normalise j.
iApply wp_case_inl; eauto using to_of_val. fold of_val. iNext.
asimpl.
erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('IHHtyped2 _ ((w,w') :: vvs)). repeat iSplit; eauto.
iApply interp_env_cons; auto.
- iApply fupd_wp.
tp_case_inr j; eauto.
tp_case_inr j; eauto; tp_normalise j.
iApply wp_case_inr; eauto using to_of_val. fold of_val. iNext.
asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('IHHtyped3 _ ((w,w') :: vvs)); repeat iSplit; eauto.
......@@ -171,9 +171,9 @@ Section fundamental.
smart_wp_bind (IfCtx _ _) v v' "[Hv #Hiv]"
('IHHtyped1 _ _ _ j (K ++ [IfCtx _ _])); cbn.
iDestruct "Hiv" as ([]) "[% %]"; simplify_eq/=; iApply fupd_wp.
- tp_if_true j; eauto.
- tp_if_true j; eauto; tp_normalise j.
iApply wp_if_true. iNext. iApply 'IHHtyped2; eauto.
- tp_if_false j; eauto.
- tp_if_false j; eauto; tp_normalise j.
iApply wp_if_false. iNext. iApply 'IHHtyped3; eauto.
Qed.
......@@ -190,7 +190,7 @@ Section fundamental.
iDestruct "Hiv" as (n) "[% %]"; simplify_eq/=.
iDestruct "Hiw" as (n') "[% %]"; simplify_eq/=.
iApply fupd_wp.
tp_nat_binop j; eauto.
tp_nat_binop j; eauto; tp_normalise j.
iApply wp_nat_binop. iNext. iModIntro. iExists _; iSplitL; eauto.
destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec;
try destruct lt_dec; eauto.
......@@ -208,7 +208,7 @@ Section fundamental.
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_rec; auto 1 using to_of_val. iNext.
iApply fupd_wp.
tp_rec j'; eauto.
tp_rec j'; eauto; tp_normalise j'.
asimpl. change (Rec ?e) with (of_val (RecV e)).
erewrite !n_closed_subst_head_simpl_2 by (rewrite ?fmap_length; eauto).
iApply ('IHHtyped _ ((_,_) :: (v,v') :: vvs)); repeat iSplit; eauto.
......@@ -237,7 +237,7 @@ Section fundamental.
iIntros "{$Hj} /= !#"; iIntros (τi ? j' K') "Hv /=".
iApply wp_tlam; iNext.
iApply fupd_wp.
tp_tlam j'; eauto.
tp_tlam j'; eauto; tp_normalise j'.
iApply 'IHHtyped; repeat iSplit; eauto. by iApply interp_env_ren.
Qed.
......@@ -282,7 +282,7 @@ Section fundamental.
change (fixpoint _) with (interp (TRec τ) Δ).
iDestruct "Hiw" as ([w w']) "#[% Hiz]"; simplify_eq/=.
iApply fupd_wp.
tp_fold j; eauto.
tp_fold j; eauto; tp_normalise j.
iApply wp_fold; cbn; auto.
iNext; iModIntro. iExists _; iFrame. by rewrite -interp_subst.
Qed.
......@@ -293,7 +293,7 @@ Section fundamental.
Proof.
iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iApply fupd_wp.
tp_fork j as i "Hi"; eauto.
tp_fork j as i "Hi"; eauto; tp_normalise j.
iApply wp_fork; iNext; iSplitL "Hj".
- iExists UnitV; eauto.
- iApply wp_wand_l; iSplitR; [|iApply ('IHHtyped _ _ _ _ [])]; eauto.
......@@ -306,14 +306,14 @@ Section fundamental.
iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (AllocCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ j (K ++ [AllocCtx])).
iApply fupd_wp.
iMod (step_alloc _ _ j K (of_val v') v' with "* [-]") as (l') "[Hj Hl]"; eauto.
tp_alloc j as k "Hk"; eauto. tp_normalise j.
iApply wp_atomic; eauto.
iApply wp_alloc; eauto. iNext.
iIntros (l) "Hl'".
iMod (inv_alloc (logN .@ (l,l')) _ ( w : val * val,
l ↦ᵢ w.1 l' ↦ₛ w.2 interp τ Δ w)%I with "[Hl Hl']") as "HN"; eauto.
{ iNext. iExists (v, v'); iFrame. iFrame "Hiv". }
iModIntro; iExists (LocV l'). iFrame "Hj". iExists (l, l'); eauto.
iIntros (l) "Hl".
iMod (inv_alloc (logN .@ (l,k)) _ ( w : val * val,
l ↦ᵢ w.1 k ↦ₛ w.2 interp τ Δ w)%I with "[Hl Hk]") as "HN"; eauto.
{ iNext. iExists (v, v'); simpl; iFrame. iFrame "Hiv". }
iModIntro; iExists (LocV k). iFrame "Hv". iExists (l, k); eauto.
Qed.
Lemma bin_log_related_load Γ e e' τ
......@@ -329,7 +329,7 @@ Section fundamental.
iModIntro.
iApply (wp_load with "Hw1").
iNext. iIntros "Hw1".
tp_load j.
tp_load j; tp_normalise j.
iMod ("Hclose" with "[Hw1 Hw2]").
{ iNext. iExists (w,w'); by iFrame. }
iModIntro. iExists w'; by iFrame.
......@@ -351,7 +351,7 @@ Section fundamental.
iModIntro.
iApply (wp_store with "Hv1"); auto using to_of_val.
iNext. iIntros "Hw2".
tp_store j; eauto.
tp_store j; eauto; tp_normalise j.
iMod ("Hclose" with "[Hw2 Hv2]").
{ iNext; iExists (w, w'); simpl; iFrame. iFrame "Hiw". }
iExists UnitV; iFrame; auto.
......@@ -384,14 +384,16 @@ Section fundamental.
simpl. iApply (wp_cas_suc with "Hv1"); eauto using to_of_val.
iNext. iIntros "Hv1".
tp_cas_suc j; subst; eauto using to_of_val.
tp_normalise j.
iMod ("Hclose" with "[Hv1 Hv2]").
{ iNext; iExists (_, _); by iFrame. }
iExists (#v true); iFrame; eauto.
iExists (#v true). iFrame "Hu"; eauto.
- iAssert ( v' w'⌝)%I as ">%".
{ rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
simpl. iApply (wp_cas_fail with "Hv1"); eauto.
iNext. iIntros "Hv1".
tp_cas_fail j; eauto.
tp_normalise j.
iMod ("Hclose" with "[Hv1 Hv2]").
{ iNext; iExists (_, _); by iFrame. }
iExists (#v false); eauto.
......
......@@ -76,10 +76,10 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
From iris_logrel.F_mu_ref_conc Require Import rules_binary.
(* ** bind *)
Lemma tac_tp_bind `{heapIG Σ, !cfgSG Σ} j Δ Δ' i p K K' e e' Q :
envs_lookup i Δ = Some (p, j fill K e)%I
fill K e = fill K' e'
envs_simple_replace i p (Esnoc Enil i (j fill K' e')) Δ = Some Δ'
Lemma tac_tp_bind_gen `{heapIG Σ, !cfgSG Σ} j Δ Δ' i p e e' Q :
envs_lookup i Δ = Some (p, j e)%I
e = e'
envs_simple_replace i p (Esnoc Enil i (j e')) Δ = Some Δ'
(Δ' Q)
(Δ Q).
Proof.
......@@ -87,18 +87,19 @@ Proof.
rewrite right_id. rewrite H1. by rewrite uPred.wand_elim_r.
Qed.
Lemma tac_tp_norm `{heapIG Σ, !cfgSG Σ} j Δ Δ' i p (e : expr) Q :
Lemma tac_tp_bind `{heapIG Σ, !cfgSG Σ} j Δ Δ' i p K' e e' Q :
envs_lookup i Δ = Some (p, j e)%I
envs_simple_replace i p (Esnoc Enil i (j fill [] e)) Δ = Some Δ'
e = fill K' e'
envs_simple_replace i p (Esnoc Enil i (j fill K' e')) Δ = Some Δ'
(Δ' Q)
(Δ Q).
Proof.
simpl. intros. rewrite envs_simple_replace_sound //. simpl.
rewrite right_id. rewrite H2. by rewrite uPred.wand_elim_r.
intros. by eapply tac_tp_bind_gen.
Qed.
Ltac tp_bind_helper :=
lazymatch goal with
rewrite ?fill_app /=;
lazymatch goal with
| |- fill ?K ?e = fill _ ?efoc =>
reshape_expr e ltac:(fun K' e' =>
unify e' efoc;
......@@ -106,9 +107,14 @@ Ltac tp_bind_helper :=
| ?K'' =>
replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app)
end)
| |- ?e = fill _ ?efoc =>
reshape_expr e ltac:(fun K' e' =>
unify e' efoc;
replace e with (fill K' e') by (by rewrite ?fill_app))
end; reflexivity.
Ltac tp_bind_helper_constr efoc :=
rewrite ?fill_app /=;
lazymatch goal with
| |- fill ?K ?e%I = fill _ _ =>
reshape_expr e ltac:(fun K' e' =>
......@@ -119,45 +125,44 @@ Ltac tp_bind_helper_constr efoc :=
with (fill K'' e')
by (rewrite ?fill_app; reflexivity)
end)
| |- ?e = fill _ _ =>
reshape_expr e ltac:(fun K' e' =>
unify e' efoc;
replace e with (fill K' e') by reflexivity)
end; reflexivity.
Tactic Notation "tp_bind" constr(j) open_constr(efoc) :=
(* TODO: this is quite slow *)
Tactic Notation "tp_normalise" constr(j) :=
iStartProof;
eapply (tac_tp_bind j);
(eapply (tac_tp_bind_gen j);
[iAssumptionCore (* prove the lookup *)
|tp_bind_helper_constr efoc (* do actual work *)
| lazymatch goal with
| |- fill ?K ?e = _ =>
by rewrite /= ?fill_app /=
| |- ?e = _ =>
idtac "nice"
end
|env_cbv; reflexivity
|(* new goal *)].
Lemma fill_nil e : fill [] e = e.
Proof. by compute. Qed.
|(* new goal *)]).
(* TODO: if the proposition is of the form
[j e], rewrite it to [j fill [] e] using fill_nil above
TODO: this is quite slow
*)
Tactic Notation "tp_normalise" constr(j) :=
Tactic Notation "tp_bind" constr(j) open_constr(efoc) :=
iStartProof;
(eapply (tac_tp_bind j);
eapply (tac_tp_bind j);
[iAssumptionCore (* prove the lookup *)
|by (simpl; rewrite ?fill_app); simpl (* do actual work *)
|tp_bind_helper_constr efoc (* do actual work *)
|env_cbv; reflexivity
|(* new goal *)]).
(* || (eapply (tac_tp_norm j); *)
(* [iAssumptionCore (* prove the lookup *) *)
(* |env_cbv; reflexivity *)
(* |(* new goal *)]). *)
|(* new goal *)].
(* TODO: figure out why the envs_simple_replace_sound lemma is not
strong enough. Try to see whether it is possible to generalize it
*)
Lemma tac_tp_store `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K K' e l e' v' v Q :
Lemma tac_tp_store `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e l e' v' v Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup_delete i2 Δ1 = Some (false, j fill K e, Δ2)%I
fill K e = fill K' (Store (Loc l) e')
envs_lookup_delete i2 Δ1 = Some (false, j e, Δ2)%I
e = fill K' (Store (Loc l) e')
envs_lookup i3 Δ2 = Some (false, l ↦ₛ v')%I
to_val e' = Some v
envs_simple_replace i3 false
......@@ -189,9 +194,9 @@ Tactic Notation "tp_store" constr(j) :=
|iAssumptionCore || fail "tp_store: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|iAssumptionCore || fail "tp_store: cannot find '? ↦ₛ ?'"
|fast_done || fail "tp_store: not a value"
|try fast_done
|env_cbv; reflexivity || fail "tp_store: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
(*
TODO:
......@@ -201,11 +206,11 @@ how can we prove that [i1 <> i2]? If we can do that then we can utilize
the lemma [envs_lookup_envs_delete_ne].
*)
Lemma tac_tp_load `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K K' e l v Q q :
Lemma tac_tp_load `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e l v Q q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup_delete i2 Δ1 = Some (false, j fill K e, Δ2)%I
fill K e = fill K' (Load (Loc l))
envs_lookup_delete i2 Δ1 = Some (false, j e, Δ2)%I
e = fill K' (Load (Loc l))
envs_lookup i3 Δ2 = Some (false, l ↦ₛ{q} v)%I
envs_simple_replace i3 false
(Esnoc (Esnoc Enil i2 (j fill K' (of_val v))) i3 (l ↦ₛ{q} v)%I) Δ2 = Some Δ3
......@@ -243,13 +248,13 @@ Tactic Notation "tp_load" constr(j) :=
|tp_bind_helper
|iAssumptionCore || fail "tp_load: cannot find '? ↦ₛ ?'"
|env_cbv; reflexivity || fail "tp_load: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_rec `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e1 e2 v Q :
Lemma tac_tp_rec `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e1 e2 v Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (App (Rec e1) e2)
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (App (Rec e1) e2)
to_val e2 = Some v
envs_simple_replace i2 false
(Esnoc Enil i2 (j fill K' (e1.[Rec e1,e2/]))) Δ1 = Some Δ2
......@@ -281,16 +286,16 @@ Tactic Notation "tp_rec" constr(j) :=
|iAssumptionCore || fail "tp_rec: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_rec: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|fast_done || fail "tp_rec: not a value"
|try fast_done
|env_cbv; reflexivity || fail "tp_rec: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_nat_binop `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e op a b Q :
Lemma tac_tp_nat_binop `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e op a b Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (BinOp op (#n a) (#n b))
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (BinOp op (#n a) (#n b))
envs_simple_replace i2 false
(Esnoc Enil i2 (j fill K' (of_val (binop_eval op a b)))) Δ1 = Some Δ2
(Δ2 |={E1,E2}=> Q)
......@@ -321,7 +326,7 @@ Tactic Notation "tp_nat_binop" constr(j) :=
|iAssumptionCore || fail "tp_nat_binop: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|env_cbv; reflexivity || fail "tp_nat_binop: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Tactic Notation "tp_op" constr(j) := tp_nat_binop j.
......@@ -333,11 +338,11 @@ Tactic Notation "tp_op" constr(j) := tp_nat_binop j.
(* ={E}= j fill K (# false) l ↦ₛ{q} v'. *)
Lemma tac_tp_cas_fail `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K K' e l e1 e2 v' v1 v2 Q q :
Lemma tac_tp_cas_fail `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e l e1 e2 v' v1 v2 Q q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup_delete i2 Δ1 = Some (false, j fill K e, Δ2)%I
fill K e = fill K' (CAS (Loc l) e1 e2)
envs_lookup_delete i2 Δ1 = Some (false, j e, Δ2)%I
e = fill K' (CAS (Loc l) e1 e2)
to_val e1 = Some v1
to_val e2 = Some v2
envs_lookup i3 Δ2 = Some (false, l ↦ₛ{q} v')%I
......@@ -377,18 +382,18 @@ Tactic Notation "tp_cas_fail" constr(j) :=
|iAssumptionCore || fail "tp_cas_fail: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_cas_fail: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|fast_done || fail "tp_cas_fail: not a value"
|fast_done || fail "tp_cas_fail: not a value"
|try fast_done
|try fast_done
|iAssumptionCore || fail "tp_cas_fail: cannot find '? ↦ ?'"
|(* v' v1 *)
|env_cbv; reflexivity || fail "tp_cas_fail: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_cas_suc `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K K' e l e1 e2 v' v1 v2 Q :
Lemma tac_tp_cas_suc `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e l e1 e2 v' v1 v2 Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup_delete i2 Δ1 = Some (false, j fill K e, Δ2)%I
fill K e = fill K' (CAS (Loc l) e1 e2)
envs_lookup_delete i2 Δ1 = Some (false, j e, Δ2)%I
e = fill K' (CAS (Loc l) e1 e2)
to_val e1 = Some v1
to_val e2 = Some v2
envs_lookup i3 Δ2 = Some (false, l ↦ₛ v')%I
......@@ -427,19 +432,19 @@ Tactic Notation "tp_cas_suc" constr(j) :=
|iAssumptionCore || fail "tp_cas_suc: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_cas_suc: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|fast_done || fail "tp_cas_suc: not a value"
|fast_done || fail "tp_cas_suc: not a value"
|try fast_done
|try fast_done
|iAssumptionCore || fail "tp_cas_suc: cannot find '? ↦ ?'"
|try reflexivity (* v' = v1 *)
|env_cbv; reflexivity || fail "tp_cas_suc: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_tlam `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e' Q :
Lemma tac_tp_tlam `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e' Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (TApp (TLam e'))
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (TApp (TLam e'))
envs_simple_replace i2 false
(Esnoc Enil i2 (j fill K' e')) Δ1 = Some Δ2
(Δ2 |={E1,E2}=> Q)
......@@ -468,13 +473,13 @@ Tactic Notation "tp_tlam" constr(j) :=
|iAssumptionCore || fail "tp_tlam: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|env_cbv; reflexivity || fail "tp_tlam: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_fold `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e' v Q :
Lemma tac_tp_fold `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e' v Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (Unfold (Fold e'))
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (Unfold (Fold e'))
to_val e' = Some v
envs_simple_replace i2 false
(Esnoc Enil i2 (j fill K' e')) Δ1 = Some Δ2
......@@ -503,16 +508,16 @@ Tactic Notation "tp_fold" constr(j) :=
|iAssumptionCore || fail "tp_fold: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_fold: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|fast_done || fail "tp_fold: not a value"
|try fast_done
|env_cbv; reflexivity || fail "tp_fold: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_fst `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e1 e2 v1 v2 Q :
Lemma tac_tp_fst `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e1 e2 v1 v2 Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (Fst (Pair e1 e2))
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (Fst (Pair e1 e2))
to_val e1 = Some v1
to_val e2 = Some v2
envs_simple_replace i2 false
......@@ -542,17 +547,17 @@ Tactic Notation "tp_fst" constr(j) :=
|iAssumptionCore || fail "tp_fst: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_fst: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|fast_done || fail "tp_fst: first component is not a value"
|fast_done || fail "tp_fst: second component is not a value"
|try fast_done
|try fast_done
|env_cbv; reflexivity || fail "tp_fst: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_snd `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e1 e2 v1 v2 Q :
Lemma tac_tp_snd `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e1 e2 v1 v2 Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (Snd (Pair e1 e2))
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (Snd (Pair e1 e2))
to_val e1 = Some v1
to_val e2 = Some v2
envs_simple_replace i2 false
......@@ -582,16 +587,16 @@ Tactic Notation "tp_snd" constr(j) :=
|iAssumptionCore || fail "tp_snd: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_snd: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|fast_done || fail "tp_snd: first component is not a value"
|fast_done || fail "tp_snd: second component is not a value"
|try fast_done
|try fast_done
|env_cbv; reflexivity || fail "tp_snd: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_case_inl `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e0 e1 e2 v Q :
Lemma tac_tp_case_inl `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e0 e1 e2 v Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (Case (InjL e0) e1 e2)
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (Case (InjL e0) e1 e2)
to_val e0 = Some v
envs_simple_replace i2 false
(Esnoc Enil i2 (j fill K' (e1.[e0/]))) Δ1 = Some Δ2
......@@ -620,16 +625,16 @@ Tactic Notation "tp_case_inl" constr(j) :=
|iAssumptionCore || fail "tp_case_inl: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_case_inl: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|fast_done || fail "tp_case_inl: not a value"
|try fast_done
|env_cbv; reflexivity || fail "tp_case_inl: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_case_inr `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e0 e1 e2 v Q :
Lemma tac_tp_case_inr `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e0 e1 e2 v Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (Case (InjR e0) e1 e2)
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (Case (InjR e0) e1 e2)
to_val e0 = Some v
envs_simple_replace i2 false
(Esnoc Enil i2 (j fill K' (e2.[e0/]))) Δ1 = Some Δ2
......@@ -658,15 +663,15 @@ Tactic Notation "tp_case_inr" constr(j) :=
|iAssumptionCore || fail "tp_case_inr: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_case_inr: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|fast_done || fail "tp_case_inr: not a value"
|try fast_done
|env_cbv; reflexivity || fail "tp_case_inr: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_if_true `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e1 e2 Q :
Lemma tac_tp_if_true `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e1 e2 Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (If (# true) e1 e2)
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (If (# true) e1 e2)
envs_simple_replace i2 false
(Esnoc Enil i2 (j fill K' e1)) Δ1 = Some Δ2
(Δ2 |={E1,E2}=> Q)
......@@ -695,13 +700,13 @@ Tactic Notation "tp_if_true" constr(j) :=
|iAssumptionCore || fail "tp_if_true: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|env_cbv; reflexivity || fail "tp_if_true: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_if_false `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e1 e2 Q :
Lemma tac_tp_if_false `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e1 e2 Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (If (# false) e1 e2)
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (If (# false) e1 e2)
envs_simple_replace i2 false
(Esnoc Enil i2 (j fill K' e2)) Δ1 = Some Δ2
(Δ2 |={E1,E2}=> Q)
......@@ -730,13 +735,13 @@ Tactic Notation "tp_if_false" constr(j) :=
|iAssumptionCore || fail "tp_if_false: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|env_cbv; reflexivity || fail "tp_if_false: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Lemma tac_tp_fork `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e' Q :
Lemma tac_tp_fork `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e' Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (Fork e')
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' (Fork e')
envs_simple_replace i2 false
(Esnoc Enil i2 (j fill K' Unit)) Δ1 = Some Δ2
(Δ2 ( (j' : nat), j' e' - |={E1,E2}=> Q)%I)
......@@ -772,7 +777,7 @@ Tactic Notation "tp_fork" constr(j) :=
|iAssumptionCore || fail "tp_fork: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|env_cbv; reflexivity || fail "tp_fork: this should not happen"
|(* new goal *)]; try (tp_normalise j).
|(* new goal *)].
Tactic Notation "tp_fork" constr(j) "as" ident(j') constr(H) :=
iStartProof;
......@@ -783,9 +788,8 @@ Tactic Notation "tp_fork" constr(j) "as" ident(j') constr(H) :=
|tp_bind_helper
|env_cbv; reflexivity || fail "tp_fork: this should not happen"
|(iIntros (j') || fail 1 "tp_fork: " j' " not fresh ");
(iIntros H || fail 1 "tp_fork: " H " not fresh");
try (tp_normalise j')
(* new goal *)]; try (tp_normalise j).
(iIntros H || fail 1 "tp_fork: " H " not fresh")
(* new goal *)].
Tactic Notation "tp_fork" constr(j) "as" ident(j') :=
let H := iFresh in tp_fork j as j' H.
......@@ -865,7 +869,7 @@ Lemma test1 E1 j K l n ρ :
Proof.
iIntros (?) "Hj #? Hl".
tp_load j.