Commit 3a40fb69 authored by Dan Frumin's avatar Dan Frumin

Get rid of some admits in denv.v

parent 664c0693
......@@ -630,12 +630,11 @@ Section denv_spec.
Lemma denv_wf_merge E m1 m2 :
denv_wf E m1 denv_wf E m2 denv_wf E (denv_merge m1 m2).
Proof.
induction m1 as [|[denv1|] ms1]; simpl.
revert m2. induction m1 as [|doenv1 ms1]; simpl; intros m2.
- destruct m2; eauto.
- destruct denv1; simpl. intros. destruct_and!.
destruct m2 as [|doenv2 ms2]; simpl.
+ split_and; eauto.
Admitted.
- destruct doenv1 as [denv1|]; try (destruct denv1);
destruct m2 as [|[denv2|] ms2]; try (destruct denv2); naive_solver.
Qed.
Lemma denv_wf_stack_merge ms E :
Forall (denv_wf E) ms
......@@ -653,13 +652,30 @@ Section denv_spec.
split_and. eapply dval_wf_mono; eauto. apply IHms; eauto.
Qed.
Lemma denv_delete_full_aux_wf E i m m' q dv :
denv_wf E m denv_delete_full_aux i m = Some (m', q, dv)
denv_wf E m' dval_wf E dv.
Proof.
revert i m'; induction m as [|[di|] m]; intros i m'; simpl; first naive_solver.
- destruct di as [dl df dval]. destruct i.
case_option_guard; simplify_eq/=; try naive_solver.
intros ? ?; destruct_and!.
destruct (denv_delete_full_aux i m) as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=.
split_and!; eauto; eapply IHm; eauto.
- destruct i; first naive_solver.
intros ??.
destruct (denv_delete_full_aux i m) as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=.
eapply IHm; 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/=. *)
Proof.
rewrite /denv_lookup.
destruct (denv_delete_full_aux i m) as [[[? q0] dv0]|] eqn:Hdel; last naive_solver.
intros; simplify_eq/=.
eapply denv_delete_full_aux_wf; eauto.
Qed.
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).
......@@ -667,7 +683,12 @@ Section denv_spec.
Lemma denv_wf_delete_full E dv i m m':
denv_wf E m denv_delete_full i m = Some (m', dv) denv_wf E m'.
Proof. Admitted.
Proof.
rewrite /denv_delete_full.
destruct (denv_delete_full_aux i m) as [[[m0 q0] dv0]|] eqn:Hdel; last naive_solver.
simpl; intros; case_option_guard; simplify_eq/=.
eapply denv_delete_full_aux_wf; eauto.
Qed.
Lemma denv_interp_mono E E' m :
denv_wf E m E `prefix_of` E'
......
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