Commit c842dd43 authored by Dan Frumin's avatar Dan Frumin

Fix `dce_subst_dcexpr_wf`.

parent 9f8ab0ac
......@@ -408,6 +408,37 @@ Qed.
(* Turn the simplification in subst OFF again *)
Arguments subst : simpl never.
(* this is a strengthened version of a lemma from the `W` reification module *)
Lemma is_closed_correct X e : W.is_closed X e heap_lang.is_closed X (W.to_expr e).
Proof.
revert X.
induction e; naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
Qed.
(* TODO: combine it with dexpr_mono & dcexpr_mono? *)
Lemma dexpr_wf_weaken X Y E de :
dexpr_wf X E de
X Y
dexpr_wf Y E de.
Proof.
revert X Y; induction de; try naive_solver (eauto; set_solver).
simpl. intros ?? Hcl%is_closed_correct ?.
apply is_closed_correct.
by eapply is_closed_weaken.
Qed.
Lemma dcexpr_wf_weaken X Y E de :
dcexpr_wf X E de
X Y
dcexpr_wf Y E de.
Proof.
revert X Y; induction de; try naive_solver (eauto; set_solver).
- simpl. intros. by eapply dexpr_wf_weaken.
- simpl. intros ?? Hcl%is_closed_correct ?.
apply is_closed_correct.
by eapply is_closed_weaken.
Qed.
Lemma de_subst_dexpr_wf X E s dv1 de2 :
dval_wf E dv1
dexpr_wf (s::X) E de2
......@@ -419,9 +450,12 @@ Proof.
apply bool_decide_pack.
apply bool_decide_unpack in Hwf2.
set_solver.
- apply W.is_closed_correct in Hwf2.
admit.
Admitted.
- apply is_closed_correct in Hwf2.
apply is_closed_correct.
rewrite W.to_expr_subst.
apply is_closed_subst; last assumption.
by apply is_closed_correct.
Qed.
Lemma dce_subst_dcexpr_wf X E s dv1 de2 :
dval_wf E dv1
......@@ -431,15 +465,19 @@ Proof.
revert X. induction de2; intros X Hdv1 Hwf2;
simplify_eq/=; try naive_solver.
- by apply de_subst_dexpr_wf.
- destruct_and!. case_match; simpl; split_and; eauto.
+ subst.
(* use H0 *)
admit.
- destruct_and!. case_match; simpl; split_and; eauto;
simplify_eq/=.
+ eapply dcexpr_wf_weaken; eauto.
set_solver.
+ eapply IHde2_2; eauto.
admit.
- apply W.is_closed_correct in Hwf2.
admit. (* Need W.is_closed_correct in the opposite direction *)
Admitted.
eapply dcexpr_wf_weaken; eauto.
set_solver.
- apply is_closed_correct in Hwf2.
apply is_closed_correct.
rewrite W.to_expr_subst.
apply is_closed_subst; last assumption.
by apply is_closed_correct.
Qed.
(*TODO: Fuse wf_mono and interp_mono into one lemma for dval and dcexpr *)
Lemma dval_wf_mono (E E': known_locs) (dv: dval) :
......
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