Commit 613aeee6 authored by Dan Frumin's avatar Dan Frumin

Cleanup commit

parent fb69d00c
......@@ -87,7 +87,7 @@ Proof.
done.
Qed.
(* TODO: beter heuristics here for operations like sub and div *)
(* TODO: beter heuristics here for operations like sub and div *)
Definition dbin_op_eval_nat (op : bin_op) (n1 n2 : nat) : dbase_lit :=
match op with
| PlusOp => dLitInt $ dNat $ (n1 + n2)%nat
......@@ -165,7 +165,7 @@ Definition dbin_op_eval
Definition dptr_plus_eval (E: known_locs) (dv1 dv2 : dval) : option dval :=
match dv1,dv2 with
| dLocV (dLoc i j), dLitV (dLitInt (dNat o)) =>
(* TODO: here we need to additionaly check wether the argument
(* TODO: here we need to additionaly check wether the argument
is a natural number *)
match offset_of_val (LitV (LitInt o)) with
| None => None
......@@ -181,8 +181,8 @@ Proof.
destruct dv1 as [?|??|[??|]|u1],dv2 as [[]|??|?|u2]; try naive_solver.
rewrite /cbin_op_eval /=.
destruct d; last by inversion 1.
case_option_guard; inversion 1.
rewrite cloc_of_to_val /=.
case_option_guard; inversion 1.
rewrite cloc_of_to_val /=.
case_option_guard; last contradiction. simpl.
rewrite cloc_plus_plus //.
Qed.
......@@ -337,7 +337,6 @@ Fixpoint dce_subst (E: known_locs)
(to_of_val _ )) we)
end.
(** Well-formedness of dcexpr w.r.t. known_locs *)
Definition dloc_wf (E: known_locs) (dl : dloc) : bool :=
match dl with
......@@ -421,7 +420,7 @@ Lemma dexpr_wf_weaken X Y E de :
X Y
dexpr_wf Y E de.
Proof.
revert X Y; induction de; try naive_solver (eauto; set_solver).
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.
......@@ -462,7 +461,7 @@ Lemma dce_subst_dcexpr_wf X E s dv1 de2 :
dcexpr_wf (s::X) E de2
dcexpr_wf X E (dce_subst E s dv1 de2).
Proof.
revert X. induction de2; intros X Hdv1 Hwf2;
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;
......
......@@ -49,7 +49,7 @@ Section denv.
| Some (DenvItem _ _ dv) :: m' => dval_wf E dv && denv_wf_val E m'
| None :: m' => denv_wf_val E m'
end.
Definition denv_wf_len (E: known_locs) (m: denv) : bool :=
bool_decide (length m length E)%nat.
......@@ -741,7 +741,7 @@ Section denv_spec.
Lemma denv_wf_mono E E' m :
denv_wf E m E `prefix_of` E' denv_wf E' m.
Proof.
Proof.
rewrite !andb_True. intros [Hm Hlen] Hpre.
split_and; last first.
{ by eapply denv_wf_len_mono. }
......@@ -838,7 +838,7 @@ Section denv_spec.
rewrite /denv_wf_len. bool_decide_unfold.
revert m1 m2. induction E; destruct m1, m2; try naive_solver omega.
simpl. intros.
apply le_n_S. eapply IHE; omega.
apply le_n_S. eapply IHE; omega.
Qed.
Lemma denv_wf_merge E m1 m2 :
......@@ -870,7 +870,7 @@ Section denv_spec.
Lemma denv_wf_len_unlock E m :
denv_wf_len E m denv_wf_len E (denv_unlock m).
Proof.
rewrite /denv_wf_len. bool_decide_unfold.
rewrite /denv_wf_len. bool_decide_unfold.
revert m; induction E; destruct m; try naive_solver omega.
simpl. intros. apply le_n_S. eapply IHE. omega.
Qed.
......@@ -1007,7 +1007,7 @@ Section denv_spec.
* rewrite denv_singleton_length. lia.
* rewrite -Nat.succ_max_distr. f_equal.
eapply IHi'.
Qed.
Qed.
Lemma denv_wf_len_insert E i x q dv m:
dloc_wf E (dLoc i 0)
......@@ -1015,7 +1015,7 @@ Section denv_spec.
denv_wf_len E (denv_insert i x q dv m).
Proof.
rewrite /denv_wf /denv_wf_len /dloc_wf. intros Hi.
bool_decide_unfold.
bool_decide_unfold.
rewrite denv_insert_length.
apply lookup_lt_is_Some in Hi. lia.
Qed.
......
......@@ -804,7 +804,7 @@ Section vcg_spec.
destruct ms as [|?m' ms]; simplify_eq.
pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen.
assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen); simplify_eq.
rewrite vcg_sp_correct; eauto. simpl.
rewrite vcg_sp_correct; eauto. simpl.
rewrite denv_merge_nil_r. clear Hsp Hlen. simplify_eq /=.
by iFrame.
Qed.
......
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