From 6fc9c27e74bc89239e3191ccca6b1d3f77e2fe44 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 12 Mar 2017 22:56:25 +0100
Subject: [PATCH] Define `fill` in terms of a `foldl` over `fill_item`.
This has some advantages:
- Evaluation contexts behave like a proper "Huet's zipper", and thus:
+ We no longer need to reverse the list of evaluation context items in the
`reshape_expr` tactic.
+ The `fill` function becomes tail-recursive.
- It gives rise to more definitional equalities in simulation proofs using
binary logical relations proofs.
In the case of binary logical relations, we simulate an expressions in some
ambient context, i.e. `fill K e`. Now, whenever we reshape `e` by turning it
into `fill K' e'`, we end up with `fill K (fill K' e')`. In order to use the
rules for the expression that is being simulated, we need to turn
`fill K (fill K' e')` into `fill K'' e'` for some `K'`. In case of the old
`foldr`-based approach, we had to rewrite using the lemma `fill_app` to
achieve that. However, in case of the old `foldl`-based `fill`, we have that
`fill K (fill K' e')` is definitionally equal to `fill (K' ++ K) e'` provided
that `K'` consists of a bunch of `cons`es (which is always the case, since we
obtained `K'` by reshaping `e`).
Note that this change hardly affected `heap_lang`. Only the proof of
`atomic_correct` broke. I fixed this by proving a more general lemma
`ectxi_language_atomic` about `ectxi`-languages, which should have been there
in the first place.
---
theories/heap_lang/tactics.v | 24 +++++------
theories/program_logic/ectxi_language.v | 55 ++++++++++++++++---------
2 files changed, 46 insertions(+), 33 deletions(-)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 92765fd94..c59a73fdf 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -185,19 +185,15 @@ Definition atomic (e : expr) :=
end.
Lemma atomic_correct e : atomic e → language.atomic (to_expr e).
Proof.
- intros He. apply ectx_language_atomic.
- - intros σ e' σ' ef.
- intros H; apply language.val_irreducible; revert H.
- destruct e; simpl; try done; repeat (case_match; try done);
- inversion 1; rewrite ?to_of_val; eauto. subst.
- unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
- - intros [|Ki K] e' Hfill Hnotval; [done|exfalso].
- apply (fill_not_val K), eq_None_not_Some in Hnotval. apply Hnotval. simpl.
- revert He. destruct e; simpl; try done; repeat (case_match; try done);
- rewrite ?bool_decide_spec;
- destruct Ki; inversion Hfill; subst; clear Hfill;
- try naive_solver eauto using to_val_is_Some.
- move=> _ /=; destruct decide as [|Nclosed]; [by eauto | by destruct Nclosed].
+ intros He. apply ectxi_language_atomic.
+ - intros σ e' σ' ef Hstep; simpl in *.
+ apply language.val_irreducible; revert Hstep.
+ destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
+ inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
+ unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto.
+ - intros Ki e' Hfill []%eq_None_not_Some; simpl in *.
+ destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
+ naive_solver eauto using to_val_is_Some.
Qed.
End W.
@@ -264,7 +260,7 @@ Ltac reshape_val e tac :=
Ltac reshape_expr e tac :=
let rec go K e :=
match e with
- | _ => tac (reverse K) e
+ | _ => tac K e
| App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
| App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
| UnOp ?op ?e => go (UnOpCtx op :: K) e
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index ee9851867..82c0e4ab0 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -45,17 +45,18 @@ Section ectxi_language.
Implicit Types (e : expr) (Ki : ectx_item).
Notation ectx := (list ectx_item).
- Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
+ Definition fill (K : ectx) (e : expr) : expr := foldl (flip fill_item) e K.
- Lemma fill_app (K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
- Proof. apply fold_right_app. Qed.
+ Lemma fill_app (K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K2 (fill K1 e).
+ Proof. apply foldl_app. Qed.
Instance fill_inj K : Inj (=) (=) (fill K).
- Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
+ Proof. induction K as [|Ki K IH]; rewrite /Inj; naive_solver. Qed.
Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
Proof.
- induction K; simpl; first done. intros ?%fill_item_val. eauto.
+ revert e.
+ induction K as [|Ki K IH]=> e //=. by intros ?%IH%fill_item_val.
Qed.
Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
@@ -66,23 +67,39 @@ Section ectxi_language.
other words, [e] also contains the reducible expression *)
Lemma step_by_val K K' e1 e1' σ1 e2 σ2 efs :
fill K e1 = fill K' e1' → to_val e1 = None → head_step e1' σ1 e2 σ2 efs →
- exists K'', K' = K ++ K''. (* K `prefix_of` K' *)
+ exists K'', K' = K'' ++ K. (* K `prefix_of` K' *)
Proof.
- intros Hfill Hred Hnval; revert K' Hfill.
- induction K as [|Ki K IH]; simpl; intros K' Hfill; first by eauto.
- destruct K' as [|Ki' K']; simplify_eq/=.
- { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
- eauto using fill_not_val, head_ctx_step_val. }
- cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
- eauto using fill_item_no_val_inj, val_stuck, fill_not_val.
+ intros Hfill Hred Hstep; revert K' Hfill.
+ induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
+ destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
+ { rewrite fill_app in Hstep.
+ exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
+ eauto using fill_not_val, head_ctx_step_val. }
+ rewrite !fill_app /= in Hfill.
+ assert (Ki = Ki') as ->
+ by eauto using fill_item_no_val_inj, val_stuck, fill_not_val.
+ simplify_eq. destruct (IH K') as [K'' ->]; auto.
+ exists K''. by rewrite assoc.
Qed.
- Global Program Instance : EctxLanguage expr val ectx state :=
- (* For some reason, Coq always rejects the record syntax claiming I
- fixed fields of different records, even when I did not. *)
- Build_EctxLanguage expr val ectx state of_val to_val [] (++) fill head_step _ _ _ _ _ _ _ _ _.
- Solve Obligations with eauto using to_of_val, of_to_val, val_stuck,
- fill_not_val, fill_app, step_by_val, fold_right_app, app_eq_nil.
+ Global Program Instance ectxi_lang_ectx : EctxLanguage expr val ectx state := {|
+ ectx_language.of_val := of_val; ectx_language.to_val := to_val;
+ empty_ectx := []; comp_ectx := flip (++); ectx_language.fill := fill;
+ ectx_language.head_step := head_step |}.
+ Solve Obligations with simpl; eauto using to_of_val, of_to_val, val_stuck,
+ fill_not_val, fill_app, step_by_val, foldl_app.
+ Next Obligation. intros K1 K2 ?%app_eq_nil; tauto. Qed.
+
+ Lemma ectxi_language_atomic e :
+ (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
+ (∀ Ki e', e = fill_item Ki e' → to_val e' = None → False) →
+ atomic e.
+ Proof.
+ intros Hastep Hafill. apply ectx_language_atomic=> //= {Hastep} K e'.
+ destruct K as [|Ki K IH] using @rev_ind=> //=.
+ rewrite fill_app /= => He Hnval.
+ destruct (Hafill Ki (fill K e')); auto using fill_not_val.
+ Qed.
Global Instance ectxi_lang_ctx_item Ki :
LanguageCtx (ectx_lang expr) (fill_item Ki).
--
GitLab