Commit 664c0693 authored by Léon Gondelman's avatar Léon Gondelman

Merge branch 'vcgen' of gitlab.science.ru.nl:lgg/iris-c-monad into vcgen

parents f7fa492f 982e612e
......@@ -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 *)
......
This diff is collapsed.
This diff is collapsed.
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