locations.v 1.59 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From stdpp Require Import countable numbers gmap.
2
From iris.prelude Require Export prelude.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.prelude Require Import options.
Amin Timany's avatar
Amin Timany committed
4

5
6
7
Record loc := Loc { loc_car : Z }.

Add Printing Constructor loc.
Amin Timany's avatar
Amin Timany committed
8

9
Global Instance loc_eq_decision : EqDecision loc.
10
Proof. solve_decision. Defined.
Amin Timany's avatar
Amin Timany committed
11

12
Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
Amin Timany's avatar
Amin Timany committed
13

14
Global Instance loc_countable : Countable loc.
15
Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.
Amin Timany's avatar
Amin Timany committed
16

17
18
19
Program Instance loc_infinite : Infinite loc :=
  inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
Next Obligation. done. Qed.
20

Amin Timany's avatar
Amin Timany committed
21
22
23
Definition loc_add (l : loc) (off : Z) : loc :=
  {| loc_car := loc_car l + off|}.

24
25
Notation "l +ₗ off" :=
  (loc_add l off) (at level 50, left associativity) : stdpp_scope.
Amin Timany's avatar
Amin Timany committed
26
27
28
29
30
31
32

Lemma loc_add_assoc l i j : l + i + j = l + (i + j).
Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.

Lemma loc_add_0 l : l + 0 = l.
Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.

33
Global Instance loc_add_inj l : Inj eq eq (loc_add l).
Amin Timany's avatar
Amin Timany committed
34
35
Proof. destruct l; rewrite /Inj /loc_add /=; intros; simplify_eq; lia. Qed.

36
Definition fresh_locs (ls : gset loc) : loc :=
37
  {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r)%Z 1%Z ls |}.
Amin Timany's avatar
Amin Timany committed
38

39
40
Lemma fresh_locs_fresh ls i :
  (0  i)%Z  fresh_locs ls + i  ls.
Amin Timany's avatar
Amin Timany committed
41
Proof.
42
  intros Hi. cut ( l, l  ls  loc_car l < loc_car (fresh_locs ls) + i)%Z.
43
44
45
  { 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.
Amin Timany's avatar
Amin Timany committed
46
47
48
Qed.

Global Opaque fresh_locs.