Commit ab6066fe authored by Dan Frumin's avatar Dan Frumin
Browse files

Clean up denv.v

parent b81ea4fb
...@@ -44,12 +44,12 @@ Section denv. ...@@ -44,12 +44,12 @@ Section denv.
| [], _ => false | [], _ => false
end. end.
Lemma denv_wf_len_spec E m : Lemma denv_wf_len_spec E m :
denv_wf_len E m <-> length E >= length m. denv_wf_len E m <-> length E >= length m.
Proof. Proof.
revert m. induction E; destruct m; intros; try (simpl; lia). revert m. induction E; destruct m; intros; try (simpl; lia).
simpl. specialize (IHE m). rewrite IHE. lia. simpl. specialize (IHE m). rewrite IHE. lia.
Qed. Qed.
Definition denv_wf (E: known_locs) (m: denv) : bool := Definition denv_wf (E: known_locs) (m: denv) : bool :=
denv_wf_val E m && denv_wf_len E m. denv_wf_val E m && denv_wf_len E m.
...@@ -685,7 +685,7 @@ Section denv_spec. ...@@ -685,7 +685,7 @@ Section denv_spec.
Qed. Qed.
(** ** Well-foundness of denv *) (** ** Well-foundness of denv *)
Lemma denv_wf_len_mono E E' m : Lemma denv_wf_len_mono E E' m :
denv_wf_len E m denv_wf_len E m
E `prefix_of`E' E `prefix_of`E'
...@@ -712,7 +712,7 @@ Section denv_spec. ...@@ -712,7 +712,7 @@ Section denv_spec.
destruct m2; first done. destruct m2; first done.
* simpl in *. eapply IHE with (m1 ++ [o0]). * simpl in *. eapply IHE with (m1 ++ [o0]).
rewrite -app_assoc. naive_solver. rewrite -app_assoc. naive_solver.
Qed. Qed.
Lemma denv_wf_val_mono_r E m1 m2 : Lemma denv_wf_val_mono_r E m1 m2 :
denv_wf_val E (m1 ++ m2) denv_wf_val E (m1 ++ m2)
...@@ -770,35 +770,35 @@ Qed. ...@@ -770,35 +770,35 @@ Qed.
destruct m2 as [|[denv2|] ms2]; try (destruct denv2); naive_solver. destruct m2 as [|[denv2|] ms2]; try (destruct denv2); naive_solver.
Qed. Qed.
Lemma denv_wf_merge_len (E : known_locs) (m1 m2 : denv) : Lemma denv_wf_merge_len (E : known_locs) (m1 m2 : denv) :
denv_wf_len E m1 denv_wf_len E m1
denv_wf_len E m2 denv_wf_len E m2
denv_wf_len E (denv_merge m1 m2). denv_wf_len E (denv_merge m1 m2).
Proof. Proof.
revert m1 m2. induction E; destruct m1, m2; naive_solver. revert m1 m2. induction E; destruct m1, m2; naive_solver.
Qed. Qed.
Lemma denv_wf_merge E m1 m2 : Lemma denv_wf_merge E m1 m2 :
denv_wf E m1 denv_wf E m2 denv_wf E (denv_merge m1 m2). denv_wf E m1 denv_wf E m2 denv_wf E (denv_merge m1 m2).
Proof. Proof.
intros Hwf1 Hwf2. intros Hwf1 Hwf2.
unfold denv_wf in Hwf1; apply andb_True in Hwf1 as [Haux1 Hlen1]. unfold denv_wf in Hwf1; apply andb_True in Hwf1 as [Haux1 Hlen1].
unfold denv_wf in Hwf2; apply andb_True in Hwf2 as [Haux2 Hlen2]. unfold denv_wf in Hwf2; apply andb_True in Hwf2 as [Haux2 Hlen2].
specialize (denv_wf_merge_val E m1 m2 Haux1 Haux2) as Hwf. specialize (denv_wf_merge_val E m1 m2 Haux1 Haux2) as Hwf.
specialize (denv_wf_merge_len E m1 m2 Hlen1 Hlen2) as Hlen. specialize (denv_wf_merge_len E m1 m2 Hlen1 Hlen2) as Hlen.
unfold denv_wf. naive_solver. unfold denv_wf. naive_solver.
Qed. Qed.
Lemma denv_wf_stack_merge ms E : Lemma denv_wf_stack_merge ms E :
Forall (denv_wf E) ms Forall (denv_wf E) ms
denv_wf E (denv_stack_merge ms). denv_wf E (denv_stack_merge ms).
Proof. Proof.
induction ms as [|m ms]; simpl; eauto. induction ms as [|m ms]; simpl; eauto.
- intros; unfold denv_wf; by destruct E. - intros; unfold denv_wf; by destruct E.
- rewrite Forall_cons =>Hm. destruct Hm as [Hm Hms]. - rewrite Forall_cons =>Hm. destruct Hm as [Hm Hms].
apply denv_wf_merge; eauto. apply denv_wf_merge; eauto.
Qed. Qed.
Lemma denv_wf_val_unlock E m : Lemma denv_wf_val_unlock E m :
denv_wf_val E m denv_wf_val E (denv_unlock m). denv_wf_val E m denv_wf_val E (denv_unlock m).
...@@ -808,7 +808,7 @@ Qed. ...@@ -808,7 +808,7 @@ Qed.
split_and. eapply dval_wf_mono; eauto. apply IHms; eauto. split_and. eapply dval_wf_mono; eauto. apply IHms; eauto.
Qed. Qed.
Lemma denv_wf_len_unlock E m : Lemma denv_wf_len_unlock E m :
denv_wf_len E m denv_wf_len E (denv_unlock m). denv_wf_len E m denv_wf_len E (denv_unlock m).
Proof. Proof.
revert m; induction E; destruct m; try naive_solver. revert m; induction E; destruct m; try naive_solver.
...@@ -946,11 +946,11 @@ Qed. ...@@ -946,11 +946,11 @@ Qed.
assert ((i + S n)%nat = (S (i + n))%nat) as -> by omega. done. assert ((i + S n)%nat = (S (i + n))%nat) as -> by omega. done.
Admitted. *) Admitted. *)
Lemma denv_interp_aux_mono E E' m (i:nat) : Lemma denv_interp_aux_mono E E' m (i:nat) :
denv_wf E m E `prefix_of` E' denv_wf E m E `prefix_of` E'
denv_interp_aux E m i - denv_interp_aux E' m i. denv_interp_aux E m i - denv_interp_aux E' m i.
Proof. Proof.
iIntros (Hwf Hpre) "H". iIntros (Hwf Hpre) "H".
unfold denv_wf in Hwf; apply andb_True in Hwf as [Haux Hlen]. unfold denv_wf in Hwf; apply andb_True in Hwf as [Haux Hlen].
iInduction m as [|dio m i] "IHm" forall (i). iInduction m as [|dio m i] "IHm" forall (i).
- by unfold denv_interp_aux. - by unfold denv_interp_aux.
...@@ -992,8 +992,6 @@ Qed. ...@@ -992,8 +992,6 @@ Qed.
Proof. Proof.
intros. destruct m; first by naive_solver. intros. destruct m; first by naive_solver.
rewrite -!denv_interp_aux_0 denv_interp_aux_mono //. rewrite -!denv_interp_aux_0 denv_interp_aux_mono //.
(* destruct E; last done.
unfold denv_wf in H0. naive_solver. *)
Qed. Qed.
...@@ -1015,14 +1013,14 @@ Qed. ...@@ -1015,14 +1013,14 @@ Qed.
dval_wf E dv. dval_wf E dv.
Proof. Admitted. Proof. Admitted.
Lemma denv_wf_extend E m dv l x q : Lemma denv_wf_extend E m dv l x q :
denv_wf E m dval_wf E dv denv_wf E m dval_wf E dv
denv_wf (E ++ [l]) (denv_insert (length E) x q dv m). denv_wf (E ++ [l]) (denv_insert (length E) x q dv m).
Proof. Proof.
intros. intros.
assert (E `prefix_of` E ++ [l]). by eapply prefix_app_l; done. assert (E `prefix_of` E ++ [l]). by eapply prefix_app_l; done.
assert (dval_wf (E ++ [l]) dv). eapply dval_wf_mono; done. assert (dval_wf (E ++ [l]) dv). eapply dval_wf_mono; done.
apply denv_wf_insert; eauto. eapply denv_wf_mono; done. apply denv_wf_insert; eauto. eapply denv_wf_mono; done.
Qed. Qed.
End denv_spec. End denv_spec.
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