From 43eeb0a9c2557e6683fa4ae15223907d9e46f09a Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Mon, 25 Sep 2017 12:51:38 +0200 Subject: [PATCH] Reify expressions into values if `to_val e=Some v` is in the context Expression `e` such that `to_val e = Some v` is in the context gets reflected into value `v` together with the proof that `to_val e = Some v`. This is helpful for substitution and for `solve_to_val` operating on the reflected syntax. --- theories/heap_lang/tactics.v | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v index bf81b68a..97a7b0a7 100644 --- a/theories/heap_lang/tactics.v +++ b/theories/heap_lang/tactics.v @@ -8,7 +8,8 @@ expressions into this type we can implementation substitution, closedness checking, atomic checking, and conversion into values, by computation. *) Module W. Inductive expr := - | Val (v : val) + (* Value together with the original expression *) + | Val (v : val) (e : heap_lang.expr) (H : to_val e = Some v) | ClosedExpr (e : heap_lang.expr) `{!Closed [] e} (* Base lambda calculus *) | Var (x : string) @@ -37,7 +38,7 @@ Inductive expr := Fixpoint to_expr (e : expr) : heap_lang.expr := match e with - | Val v => of_val v + | Val v e' _ => e' | ClosedExpr e _ => e | Var x => heap_lang.Var x | Rec f x e => heap_lang.Rec f x (to_expr e) @@ -90,13 +91,16 @@ Ltac of_expr e := let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(CAS e0 e1 e2) | to_expr ?e => e - | of_val ?v => constr:(Val v) - | _ => match goal with H : Closed [] e |- _ => constr:(@ClosedExpr e H) end + | of_val ?v => constr:(Val v (of_val v) (to_of_val v)) + | _ => match goal with + | H : to_val e = Some ?v |- _ => constr:(Val v e H) + | H : Closed [] e |- _ => constr:(@ClosedExpr e H) + end end. Fixpoint is_closed (X : list string) (e : expr) : bool := match e with - | Val _ | ClosedExpr _ _ => true + | Val _ _ _ | ClosedExpr _ _ => true | Var x => bool_decide (x ∈ X) | Rec f x e => is_closed (f :b: x :b: X) e | Lit _ => true @@ -110,7 +114,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool := Lemma is_closed_correct X e : is_closed X e → heap_lang.is_closed X (to_expr e). Proof. revert X. - induction e; naive_solver eauto using is_closed_of_val, is_closed_weaken_nil. + induction e; naive_solver eauto using is_closed_of_val, is_closed_to_val, is_closed_weaken_nil. Qed. (* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr] @@ -119,7 +123,7 @@ about apart from being closed. Notice that the reverse implication of [to_val_Some] thus does not hold. *) Fixpoint to_val (e : expr) : option val := match e with - | Val v => Some v + | Val v _ _ => Some v | Rec f x e => if decide (is_closed (f :b: x :b: []) e) is left H then Some (@RecV f x (to_expr e) (is_closed_correct _ _ H)) else None @@ -142,7 +146,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed. Fixpoint subst (x : string) (es : expr) (e : expr) : expr := match e with - | Val v => Val v + | Val v e H => Val v e H | ClosedExpr e H => @ClosedExpr e H | Var y => if decide (x = y) then es else Var y | Rec f y e => @@ -168,7 +172,7 @@ Lemma to_expr_subst x er e : to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e). Proof. induction e; simpl; repeat case_decide; - f_equal; auto using subst_is_closed_nil, is_closed_of_val, eq_sym. + f_equal; eauto using subst_is_closed_nil, is_closed_of_val, is_closed_to_val, eq_sym. Qed. Definition atomic (e : expr) := @@ -213,11 +217,15 @@ Ltac solve_to_val := match goal with | |- to_val ?e = Some ?v => let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v); - apply W.to_val_Some; simpl; unfold W.to_expr; unlock; reflexivity + apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity + | |- IntoVal ?e ?v => + let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v); + apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity | |- is_Some (to_val ?e) => let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e'))); apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I end. +Hint Extern 10 (IntoVal _ _) => solve_to_val : typeclass_instances. Ltac solve_atomic := match goal with -- GitLab