Add original expressions to values in the reified syntax

F_mu_ref_conc/reflection.v

@@ -4,7 +4,7 @@ Import lang.
 
 Module R.
 Inductive expr :=
-  | Val (v : lang.val)
+  | Val (v : lang.val) (e : lang.expr) (Hev : to_val e = Some v)
   | ClosedExpr (e : lang.expr) `{Closed ∅ e}  
   | Var (x : string)
   | Rec (f x : binder) (e : expr)
@@ -43,7 +43,7 @@ Inductive expr :=
 
 Fixpoint to_expr (e : expr) : lang.expr :=
   match e with
-  | Val v => of_val v
+  | Val v e _ => e
   | ClosedExpr e _ => e
   | Var x => lang.Var x
   | Rec f x e => lang.Rec f x (to_expr e)
@@ -109,15 +109,11 @@ Ltac of_expr e :=
   | lang.TLam ?e => let e := of_expr e in constr:(TLam e)
   | lang.TApp ?e => let e := of_expr e in constr:(TApp e)
   | to_expr ?e => e
-  | of_val ?v => constr:(Val v)
+  | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
   | _ =>
     lazymatch goal with
     | [H : to_val e = Some ?ev |- _] =>
-      (* DF: The reason why we do /not/ produce `Val ev` here is that
-       `of_val ev` is generally not going to be definitionally equal
-       to `e`. Since we want to solve certain things "by computation"
-       this sort of defats the purpose. *)
-      constr:(@ClosedExpr e (to_val_closed e ev H))
+      constr:(Val ev e H)
     | [H : Closed ∅ e |- _] => constr:(@ClosedExpr e H)
     | [H : Is_true (is_closed ∅ e) |- _] => constr:(@ClosedExpr e H)
     end
@@ -125,7 +121,7 @@ Ltac of_expr e :=
 
 Fixpoint is_closed (X : gset string) (e : expr) : bool :=
   match e with
-  | Val v => true
+  | Val _ _ _ => true
   | ClosedExpr e _ => true
   | Var x => bool_decide (x ∈ X)
   | Lit l => true
@@ -144,13 +140,13 @@ Lemma is_closed_correct X e : is_closed X e → lang.is_closed X (to_expr e).
 Proof.
   revert X.
   induction e; cbn; try naive_solver. 
-  - intros. eapply of_val_closed'.
+  - intros. rewrite -(of_to_val _ _ Hev). eapply of_val_closed'.
   - intros. eapply is_closed_weaken; eauto. set_solver.
 Qed.
 
 Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   match e with
-  | Val _ => e
+  | Val _ _ _ => e
   | ClosedExpr _ _ => e
   | Var y => if decide (x = y) then es else Var y
   | Rec f y e =>
@@ -187,7 +183,8 @@ Lemma subst_correct x es e :
   lang.subst x (to_expr es) (to_expr e) = to_expr (subst x es e).
 Proof.
   induction e; cbn; try (congruence || naive_solver).
-  - by rewrite (@Closed_subst_id _ _ _ (of_val_closed v)).
+  - rewrite -(of_to_val _ _ Hev).
+    by rewrite (@Closed_subst_id _ _ _ (of_val_closed v)).
   - by rewrite (@Closed_subst_id _ _ _ H).
   - case_match; eauto.
   - case_match; eauto. congruence.
@@ -199,7 +196,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 (x :b: f :b: ∅) e) is left H
      then Some (@RecV f x (to_expr e) (is_closed_correct _ _ H)) else None
@@ -276,9 +273,6 @@ Ltac solve_closed2 :=
 Hint Extern 1 (Closed _ _) => solve_closed2 : typeclass_instances.
 (* Hint Extern 1 (Closed _ _) => solve_closed2. *)
 
-(* DF: I used it for automatically discharging assumptions for the PureExec instances *)
-Hint Extern 1 (to_val _ = Some _) => eassumption : typeclass_instances.
-
 Ltac simpl_subst :=
   cbn[subst'];
   repeat match goal with