Commit 61dde255 authored by Dan Frumin's avatar Dan Frumin

Attempt some well-formedness lemmas

parent 3c9f273a
......@@ -307,25 +307,21 @@ Qed.
Lemma dun_op_eval_dSome_wf E dv u dw:
dval_wf E dv dun_op_eval E u dv = dSome dw dval_wf E dw.
Proof.
Admitted.
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
Lemma dun_op_eval_dUnknown_wf E dv u w:
dval_wf E dv dun_op_eval E u dv = dUnknown (Some w) dval_wf E w.
Proof.
Admitted.
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
Lemma dbin_op_eval_dSome_wf E dv1 dv2 op dw:
dval_wf E dv1 dval_wf E dv2
dbin_op_eval E op dv1 dv2 = dSome dw dval_wf E dw.
Proof.
Admitted.
Proof. destruct op, dv1,dv2; simpl; repeat case_match; intros; simplify_eq/=; done. Qed.
Lemma dbin_op_eval_dUnknown_wf E dv1 dv2 op w:
dval_wf E dv1 dval_wf E dv2
dbin_op_eval E op dv1 dv2 = dUnknown (Some w) dval_wf E w.
Proof.
Admitted.
Proof. Admitted.
(** / Well-foundness of dcexpr w.r.t. known_locs *)
......
......@@ -787,19 +787,37 @@ Section denv_spec.
(** ** Well-foundness of denv *)
Lemma denv_wf_mono E E' m :
denv_wf E m E `prefix_of` E' denv_wf E' m.
Proof. Admitted.
Proof.
induction m as [|[denv|] ms]; simpl; eauto.
destruct denv; simpl. intros. destruct_and!.
split_and. eapply dval_wf_mono; eauto. apply IHms; eauto.
Qed.
Lemma denv_wf_merge E m1 m2 :
denv_wf E m1 denv_wf E m2 denv_wf E (denv_merge m1 m2).
Proof. Admitted.
Lemma denv_wf_unlock E m1 :
denv_wf E m1 denv_wf E (denv_unlock m1).
Proof. Admitted.
Proof.
induction m1 as [|[denv1|] ms1]; simpl.
- destruct m2; eauto.
- destruct denv1; simpl. intros. destruct_and!.
destruct m2 as [|doenv2 ms2]; simpl.
+ split_and; eauto.
Admitted.
Lemma denv_wf_unlock E m :
denv_wf E m denv_wf E (denv_unlock m).
Proof.
induction m as [|[denv|] ms]; simpl; eauto.
destruct denv; simpl. intros. destruct_and!.
split_and. eapply dval_wf_mono; eauto. apply IHms; eauto.
Qed.
Lemma denv_lookup_wf E i m q dv :
denv_wf E m denv_lookup i m = Some (q, dv) dval_wf E dv.
Proof. Admitted.
(* rewrite /denv_lookup. *)
(* induction m as [|[denv|] ms]; simpl; first naive_solver. *)
(* destruct denv. destruct i. *)
(* case_option_guard; simplify_eq/=. *)
Lemma denv_wf_insert E i x q dv m:
denv_wf E m dval_wf E dv denv_wf E (denv_insert i x q dv m).
......
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