Commit d13b876d authored by Dan Frumin's avatar Dan Frumin

Add more relational tactics

parent f7b78e01
......@@ -101,7 +101,7 @@ Tactic Notation "rel_rec_l" :=
[tac_bind_helper (* e = fill K' _ *)
|solve_of_val_unlock
|try solve_closed
|fast_done (* to_val e' = Some v *)
|solve_to_val (* to_val e' = Some v *)
|try fast_done (* eres = subst ... *)
|try simpl_subst/=; iNext (* new goal *)]
end)
......@@ -110,6 +110,154 @@ Tactic Notation "rel_rec_l" :=
Tactic Notation "rel_seq_l" := rel_rec_l.
Tactic Notation "rel_let_l" := rel_rec_l.
Lemma tac_rel_fst_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e e1 e2 v1 v2 K' t τ :
e = fill K' (Fst (Pair e1 e2))
to_val e1 = Some v1
to_val e2 = Some v2
(Δ bin_log_related E1 E1 Γ (fill K' e1) t τ)
(Δ bin_log_related E1 E1 Γ e t τ).
Proof.
intros ????.
subst e.
rewrite -(of_to_val e1 v1); auto. rewrite -(of_to_val e2 v2); auto.
rewrite -(bin_log_related_fst_l Γ E1).
by rewrite (of_to_val e1 v1).
Qed.
Tactic Notation "rel_fst_l" :=
iStartProof;
eapply (tac_rel_fst_l);
[tac_bind_helper (* e = fill K' ... *)
|solve_to_val
|solve_to_val
|iNext (* new goal *)].
Lemma tac_rel_snd_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e e1 e2 v1 v2 K' t τ :
e = fill K' (Snd (Pair e1 e2))
to_val e1 = Some v1
to_val e2 = Some v2
(Δ bin_log_related E1 E1 Γ (fill K' e2) t τ)
(Δ bin_log_related E1 E1 Γ e t τ).
Proof.
intros ????.
subst e.
rewrite -(of_to_val e1 v1); auto. rewrite -(of_to_val e2 v2); auto.
rewrite -(bin_log_related_snd_l Γ E1).
by rewrite (of_to_val e2 v2).
Qed.
Tactic Notation "rel_snd_l" :=
iStartProof;
eapply (tac_rel_snd_l);
[tac_bind_helper (* e = fill K' ... *)
|solve_to_val
|solve_to_val
|iNext (* new goal *)].
Lemma tac_rel_unfold_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e e1 v K' t τ :
e = fill K' (Unfold (Fold e1))
to_val e1 = Some v
(Δ bin_log_related E1 E1 Γ (fill K' e1) t τ)
(Δ bin_log_related E1 E1 Γ e t τ).
Proof.
intros ???.
subst e.
rewrite -(bin_log_related_fold_l Γ E1); eassumption.
Qed.
Tactic Notation "rel_unfold_l" :=
iStartProof;
eapply (tac_rel_unfold_l);
[tac_bind_helper (* e = fill K' ... *)
|solve_to_val
|iNext (* new goal *)].
Tactic Notation "rel_fold_l" := rel_unfold_l.
Lemma tac_rel_if_true_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e e1 e2 K' t τ :
e = fill K' (If (# true) e1 e2)
Closed e1
Closed e2
(Δ bin_log_related E1 E1 Γ (fill K' e1) t τ)
(Δ bin_log_related E1 E1 Γ e t τ).
Proof.
intros ????.
subst e.
rewrite -(bin_log_related_if_true_l Γ E1); eassumption.
Qed.
Tactic Notation "rel_if_true_l" :=
iStartProof;
eapply (tac_rel_if_true_l);
[tac_bind_helper (* e = fill K' ... *)
|try solve_closed
|try solve_closed
|iNext (* new goal *)].
Lemma tac_rel_if_false_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e e1 e2 K' t τ :
e = fill K' (If (# false) e1 e2)
Closed e1
Closed e2
(Δ bin_log_related E1 E1 Γ (fill K' e2) t τ)
(Δ bin_log_related E1 E1 Γ e t τ).
Proof.
intros ????.
subst e.
rewrite -(bin_log_related_if_false_l Γ E1); eassumption.
Qed.
Tactic Notation "rel_if_false_l" :=
iStartProof;
eapply (tac_rel_if_false_l);
[tac_bind_helper (* e = fill K' ... *)
|try solve_closed
|try solve_closed
|iNext (* new goal *)].
Lemma tac_rel_case_inl_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e e0 v e1 e2 K' t τ :
e = fill K' (Case (InjL e0) e1 e2)
to_val e0 = Some v
Closed e1
Closed e2
(Δ bin_log_related E1 E1 Γ (fill K' (e1 e0)) t τ)
(Δ bin_log_related E1 E1 Γ e t τ).
Proof.
intros ?????.
subst e.
rewrite -(bin_log_related_case_inl_l Γ E1); eassumption.
Qed.
Tactic Notation "rel_case_inl_l" :=
iStartProof;
eapply (tac_rel_case_inl_l);
[tac_bind_helper (* e = fill K' ... *)
|solve_to_val || fail 2 "In 'case: InjL v of ..' cannot show that 'v' is a value"
|try solve_closed
|try solve_closed
|iNext (* new goal *)].
Lemma tac_rel_case_inr_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e e0 v e1 e2 K' t τ :
e = fill K' (Case (InjR e0) e1 e2)
to_val e0 = Some v
Closed e1
Closed e2
(Δ bin_log_related E1 E1 Γ (fill K' (e2 e0)) t τ)
(Δ bin_log_related E1 E1 Γ e t τ).
Proof.
intros ?????.
subst e.
rewrite -(bin_log_related_case_inr_l Γ E1); eassumption.
Qed.
Tactic Notation "rel_case_inr_l" :=
iStartProof;
eapply (tac_rel_case_inr_l);
[tac_bind_helper (* e = fill K' ... *)
|solve_to_val || fail 2 "In 'case: InjR v of ..' cannot show that 'v' is a value"
|try solve_closed
|try solve_closed
|iNext (* new goal *)].
Lemma tac_rel_binop_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e K' op a b eres t τ :
e = fill K' (BinOp op (#n a) (#n b))
eres = of_val (binop_eval op a b)
......@@ -268,6 +416,30 @@ Tactic Notation "rel_load_l" "under" constr(N) "as" constr(nam) constr(nam_cl) :
|env_cbv; reflexivity || fail "rel_load_l: this should not happen"
|(* new goal *)].
Lemma tac_rel_load_l_simp `{heapIG Σ, !cfgSG Σ} Δ1 Δ2 E1 i1 l v K' Γ e t τ :
e = fill K' (Load (Loc l))
IntoLaterNEnvs 1 Δ1 Δ2
envs_lookup i1 Δ2 = Some (false, l ↦ᵢ v)%I
(Δ2 bin_log_related E1 E1 Γ (fill K' (of_val v)) t τ)
(Δ1 bin_log_related E1 E1 Γ e t τ).
Proof.
intros ??? HΔ2.
subst e.
rewrite into_laterN_env_sound envs_lookup_split //; simpl.
rewrite uPred.later_sep.
rewrite HΔ2.
apply uPred.wand_elim_l'.
by rewrite -(bin_log_related_load_l' Γ E1).
Qed.
Tactic Notation "rel_load_l" :=
iStartProof;
eapply (tac_rel_alloc_l_simp);
[tac_bind_helper (* e = fill K' .. *)
|apply _ (* IntoLaterNenvs 1 Δ1 Δ2 *)
|iAssumptionCore || fail 3 "rel_load_l: cannot find ? ↦ᵢ ?"
| (* new goal *)].
Lemma tac_rel_store_l `{heapIG Σ, !cfgSG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l e' v' K' Γ e t τ :
nclose N E1
envs_lookup i1 Δ1 = Some (p, inv N P)
......@@ -508,7 +680,7 @@ Tactic Notation "rel_load_r" :=
eapply (tac_rel_load_r);
[solve_ndisj || fail "rel_load_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
|iAssumptionCore || fail "rel_load_l: cannot find ? ↦ₛ ?"
|iAssumptionCore || fail "rel_load_r: cannot find ? ↦ₛ ?"
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
|simpl (* new goal *)].
......
......@@ -442,13 +442,13 @@ Section properties.
Lemma bin_log_related_load_l' Γ E1 K l v' t τ :
(l ↦ᵢ v') -
(l ↦ᵢ v' - {E1,E1;Γ} fill K (of_val v') log t : τ)
(l ↦ᵢ v' - ({E1,E1;Γ} fill K (of_val v') log t : τ))
- {E1,E1;Γ} fill K (Load (Loc l)) log t : τ.
Proof.
iIntros "Hl Hlog".
iApply (bin_log_related_load_l); auto.
iExists v'.
iModIntro.
iModIntro.
by iFrame.
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