Commit 80623a8c by Dan Frumin

Get rid of a superflous argument to `fresh_locs`.

parent 5123ac6b
 ... ... @@ -685,7 +685,7 @@ Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 : Proof. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed. Lemma alloc_fresh v n σ : let l := fresh_locs (dom (gset loc) σ.(heap)) n in let l := fresh_locs (dom (gset loc) σ.(heap)) in 0 < n → head_step (AllocN ((Val \$ LitV \$ LitInt \$ n)) (Val v)) σ [] (Val \$ LitV \$ LitLoc l) (state_init_heap l n v σ) []. ... ...
 ... ... @@ -30,13 +30,13 @@ Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed. Instance loc_add_inj l : Inj eq eq (loc_add l). Proof. destruct l; rewrite /Inj /loc_add /=; intros; simplify_eq; lia. Qed. Definition fresh_locs (ls : gset loc) (n : Z) : loc := Definition fresh_locs (ls : gset loc) : loc := {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r)%Z 1%Z ls |}. Lemma fresh_locs_fresh ls n i : (0 ≤ i)%Z → (i < n)%Z → fresh_locs ls n +ₗ i ∉ ls. Lemma fresh_locs_fresh ls i : (0 ≤ i)%Z → fresh_locs ls +ₗ i ∉ ls. Proof. intros Hi _. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh_locs ls n) + i)%Z. intros Hi. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh_locs ls) + i)%Z. { intros help Hf%help. simpl in *. lia. } apply (set_fold_ind_L (λ r ls, ∀ l, l ∈ ls → (loc_car l < r + i)%Z)); set_solver by eauto with lia. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!