Commit 9dc07689 authored by Dan Frumin's avatar Dan Frumin

Make `inv_head_step` available from lang.v

parent 04f63a10
......@@ -12,18 +12,6 @@ Definition lamsubst (e : expr) (v : val) : expr :=
Notation "e $/ v" := (lamsubst e%E v%V) (at level 71, left associativity) : expr_scope.
(* ^ this should be left associative at a level lower than that of `bin_log_related` *)
Ltac inv_head_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : _ = of_val ?v |- _ =>
is_var v; destruct v; first[discriminate H|injection H as H]
| H : head_step ?e _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
Section hax.
Context `{logrelG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
......
......@@ -431,3 +431,17 @@ Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances.
(* This lemma is helpful for tactics on locked values and for reifying locked values. *)
Lemma of_val_unlock v e : of_val v = e of_val (locked v) = e.
Proof. by unlock. Qed.
(* Some other useful tactics *)
Ltac inv_head_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : _ = of_val ?v |- _ =>
is_var v; destruct v; first[discriminate H|injection H as H]
| H : head_step ?e _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
......@@ -140,7 +140,7 @@ Section properties.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- do 3 eexists. econstructor; eauto.
- by inversion H0.
- by inv_head_step.
Qed.
Lemma bin_log_related_snd_l Γ E K v1 v2 e τ :
......@@ -150,7 +150,7 @@ Section properties.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- do 3 eexists. econstructor; eauto.
- by inversion H0.
- by inv_head_step.
Qed.
Lemma bin_log_related_rec_l Γ E K (f x : binder) e e' v t τ
......@@ -171,9 +171,7 @@ Section properties.
destruct f, x; cbn-[union]; rewrite ?dom_insert ?dom_singleton ?dom_empty;
set_solver. (* TODO: kinda slow, dom_insert_binder *)
- do 3 eexists. econstructor; eauto.
- match goal with
| H : head_step _ _ _ _ _ |- _ => inversion H
end. done.
- by inv_head_step.
Qed.
Lemma bin_log_related_tlam_l Γ E K e t τ
......@@ -184,9 +182,7 @@ Section properties.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- do 3 eexists. econstructor; eauto.
- match goal with
| H : head_step _ _ _ _ _ |- _ => inversion H
end. done.
- by inv_head_step.
Qed.
Lemma bin_log_related_fold_l Γ E K e v t τ :
......@@ -197,9 +193,7 @@ Section properties.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- do 3 eexists. econstructor; eauto.
- match goal with
| H : head_step _ _ _ _ _ |- _ => inversion H
end. done.
- by inv_head_step.
Qed.
Lemma bin_log_related_pack_l Γ E K e e' v t τ
......@@ -211,9 +205,7 @@ Section properties.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- do 3 eexists. econstructor; eauto.
- match goal with
| H : head_step _ _ _ _ _ |- _ => inversion H
end. done.
- by inv_head_step.
Qed.
Lemma bin_log_related_case_inl_l Γ E K e v e1 e2 t τ
......@@ -226,9 +218,7 @@ Section properties.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- do 3 eexists. econstructor; eauto.
- match goal with
| H : head_step _ _ _ _ _ |- _ => inversion H
end. done.
- by inv_head_step.
Qed.
Lemma bin_log_related_case_inr_l Γ E K e v e1 e2 t τ
......@@ -241,9 +231,7 @@ Section properties.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- do 3 eexists. econstructor; eauto.
- match goal with
| H : head_step _ _ _ _ _ |- _ => inversion H
end. done.
- by inv_head_step.
Qed.
Lemma bin_log_related_if_true_l Γ E K e1 e2 t τ
......@@ -255,9 +243,7 @@ Section properties.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros.
- do 3 eexists. econstructor; eauto.
- match goal with
| H : head_step _ _ _ _ _ |- _ => inversion H
end. done.
- by inv_head_step.
Qed.
Lemma bin_log_related_if_true_masked_l Γ E1 E2 K e1 e2 t τ
......@@ -267,9 +253,9 @@ Section properties.
{E1,E2;Γ} fill K (If (# true) e1 e2) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_masked_l with "Hlog"); auto.
iApply (bin_log_pure_masked_l with "Hlog"); auto; intros.
- do 3 eexists. econstructor; eauto.
- by inversion 1.
- by inv_head_step.
Qed.
Lemma bin_log_related_if_false_l Γ E K e1 e2 t τ
......@@ -279,11 +265,9 @@ Section properties.
{E,E;Γ} (fill K (If (# false) e1 e2)) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
iApply (bin_log_pure_l with "Hlog"); auto; intros.
- do 3 eexists. econstructor; eauto.
- match goal with
| H : head_step _ _ _ _ _ |- _ => inversion H
end. done.
- by inv_head_step.
Qed.
Lemma bin_log_related_if_false_masked_l Γ E1 E2 K e1 e2 t τ
......@@ -293,9 +277,9 @@ Section properties.
{E1,E2;Γ} (fill K (If (# false) e1 e2)) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_masked_l with "Hlog"); auto.
iApply (bin_log_pure_masked_l with "Hlog"); auto; intros.
- do 3 eexists. econstructor; eauto.
- by inversion 1.
- by inv_head_step.
Qed.
Lemma bin_log_related_binop_l Γ E K op a b t τ :
......@@ -303,11 +287,9 @@ Section properties.
{E,E;Γ} (fill K (BinOp op (#n a) (#n b))) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
iApply (bin_log_pure_l with "Hlog"); auto; intros.
- do 3 eexists. econstructor; eauto.
- match goal with
| H : head_step _ _ _ _ _ |- _ => inversion H
end. done.
- by inv_head_step.
Qed.
(** *** Stateful reductions *)
......@@ -371,7 +353,7 @@ Section properties.
iApply ("Hlog" with "HΦ").
Qed.
(* TODO: how to make eauto do this? *)
(* TODO: simplify this monstrosity *)
Ltac rewrite_closed :=
try (let F := fresh in
intro F); simpl;
......
......@@ -30,18 +30,6 @@ Section lang_rules.
Implicit Types Φ : val iProp Σ.
Implicit Types σ : state.
Ltac inv_head_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : _ = of_val ?v |- _ =>
is_var v; destruct v; first[discriminate H|injection H as H]
| H : head_step ?e _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
Local Hint Extern 0 (atomic _) => solve_atomic.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
......
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