Lvc.Fresh
Require Import CSet Le Arith.Compare_dec.
Require Import Plus Util Map Var Get.
Set Implicit Arguments.
Definition fresh (s : set var) : var :=
S(fold max s 0).
Lemma fresh_spec´ (G:set var)
: ∀ (x:var), x ∈ G → x ≤ fold max G 0.
Lemma fresh_spec G : fresh G ∉ G.
Section SafeFirst.
Hypothesis P : nat → Prop.
Inductive safe : nat → Prop :=
| safe_here n : P n → safe n
| safe_after n : safe (S n) → safe n.
Lemma safe_antitone m n
: safe n
→ m < n
→ safe m.
Lemma exists_is_safe
: (∃ x, P x) → ∃ n, safe n.
Hypothesis comp : ∀ n, Computable (P n).
Fixpoint safe_first n (s:safe n) : nat.
Defined.
Fixpoint safe_first_spec n s
: P (@safe_first n s).
End SafeFirst.
Lemma safe_impl (P Q: nat → Prop) n
: safe P n → (∀ x, P x → Q x) → safe Q n.
Lemma fresh_variable_always_exists (lv:set nat) n
: safe (fun x ⇒ x ∉ lv) n.
Lemma all_in_lv_cardinal (lv:set nat) n
: (∀ m : nat, m < n → m \In lv) → cardinal lv ≥ n.
Lemma neg_pidgeon_hole (lv:set nat)
: (∀ m : nat, m ≤ cardinal lv → m \In lv) → False.
Inductive le (n : nat) : nat → Prop :=
le_n : le n n | le_S : ∀ m : nat, le (S n) m → le n m.
Lemma le_is_le n m
: le n m ↔ n ≤ m.
Lemma small_fresh_variable_exists (lv:set nat) n
: (∀ m, m < n → m ∈ lv)
→ le n (cardinal lv)
→ safe (fun x ⇒ x ∉ lv ∧ x ≤ cardinal lv) n.
Instance le_dec x y : Computable (x ≤ y).
Defined.
Definition least_fresh (lv:set var) : var.
Defined.
Lemma least_fresh_full_spec G
: least_fresh G ∉ G ∧ least_fresh G ≤ cardinal G.
Lemma least_fresh_spec G
: least_fresh G ∉ G.
Lemma least_fresh_small G
: least_fresh G ≤ cardinal G.
Definition fresh_stable (lv:set var) (x:var) : var :=
if [x ∉ lv] then x else
fresh lv.
Lemma fresh_stable_spec G x
: fresh_stable G x ∉ G.
Fixpoint vars_up_to (n:nat) :=
match n with
| S n ⇒ {n; vars_up_to n}
| 0 ⇒ ∅
end.
Lemma in_vars_up_to n m
: n < m → n ∈ vars_up_to m.
Lemma in_vars_up_to´ n m
: n ≤ m → n ∈ vars_up_to (m + 1).
Lemma vars_up_to_incl n m
: n ≤ m → vars_up_to n ⊆ vars_up_to m.
Lemma vars_up_to_max n m
: vars_up_to (max n m) [=] vars_up_to n ∪ vars_up_to m.
Section FreshList.
Variable fresh : set var → var.
Fixpoint fresh_list (G:set var) (n:nat) : list var :=
match n with
| 0 ⇒ nil
| S n ⇒ let x := fresh G in x::fresh_list (G ∪ {{x}}) n
end.
Lemma fresh_list_length (G:set var) n
: length (fresh_list G n) = n.
Hypothesis fresh_spec : ∀ G, fresh G ∉ G.
Definition fresh_set (G:set var) (n:nat) : set var :=
of_list (fresh_list G n).
Lemma fresh_list_spec : ∀ (G:set var) n, (of_list (fresh_list G n)) ∩ G [=] ∅.
Lemma fresh_set_spec
: ∀ (G:set var) n, (fresh_set G n) ∩ G [=] ∅.
Lemma fresh_list_unique (G: set var) n
: unique (fresh_list G n).
Hypothesis fresh_small : ∀ G : set var, fresh G ≤ SetInterface.cardinal G.
Lemma least_fresh_list_small G n
: ∀ i x, get (fresh_list G n) i x → x < cardinal G + n.
Lemma least_fresh_list_small_vars_up_to G n
: of_list (fresh_list G n) ⊆ vars_up_to (cardinal G + n).
End FreshList.
Lemma inverse_on_update_fresh_list (D:set var) (Z:list var) (ϱ ϱ´ : var → var)
: inverse_on (D \ of_list Z) ϱ ϱ´
→ inverse_on D (update_with_list Z (fresh_list fresh (lookup_set ϱ (D \ of_list Z)) (length Z)) ϱ)
(update_with_list (fresh_list fresh (lookup_set ϱ (D \ of_list Z)) (length Z)) Z ϱ´).
Require Import Plus Util Map Var Get.
Set Implicit Arguments.
Definition fresh (s : set var) : var :=
S(fold max s 0).
Lemma fresh_spec´ (G:set var)
: ∀ (x:var), x ∈ G → x ≤ fold max G 0.
Lemma fresh_spec G : fresh G ∉ G.
Section SafeFirst.
Hypothesis P : nat → Prop.
Inductive safe : nat → Prop :=
| safe_here n : P n → safe n
| safe_after n : safe (S n) → safe n.
Lemma safe_antitone m n
: safe n
→ m < n
→ safe m.
Lemma exists_is_safe
: (∃ x, P x) → ∃ n, safe n.
Hypothesis comp : ∀ n, Computable (P n).
Fixpoint safe_first n (s:safe n) : nat.
Defined.
Fixpoint safe_first_spec n s
: P (@safe_first n s).
End SafeFirst.
Lemma safe_impl (P Q: nat → Prop) n
: safe P n → (∀ x, P x → Q x) → safe Q n.
Lemma fresh_variable_always_exists (lv:set nat) n
: safe (fun x ⇒ x ∉ lv) n.
Lemma all_in_lv_cardinal (lv:set nat) n
: (∀ m : nat, m < n → m \In lv) → cardinal lv ≥ n.
Lemma neg_pidgeon_hole (lv:set nat)
: (∀ m : nat, m ≤ cardinal lv → m \In lv) → False.
Inductive le (n : nat) : nat → Prop :=
le_n : le n n | le_S : ∀ m : nat, le (S n) m → le n m.
Lemma le_is_le n m
: le n m ↔ n ≤ m.
Lemma small_fresh_variable_exists (lv:set nat) n
: (∀ m, m < n → m ∈ lv)
→ le n (cardinal lv)
→ safe (fun x ⇒ x ∉ lv ∧ x ≤ cardinal lv) n.
Instance le_dec x y : Computable (x ≤ y).
Defined.
Definition least_fresh (lv:set var) : var.
Defined.
Lemma least_fresh_full_spec G
: least_fresh G ∉ G ∧ least_fresh G ≤ cardinal G.
Lemma least_fresh_spec G
: least_fresh G ∉ G.
Lemma least_fresh_small G
: least_fresh G ≤ cardinal G.
Definition fresh_stable (lv:set var) (x:var) : var :=
if [x ∉ lv] then x else
fresh lv.
Lemma fresh_stable_spec G x
: fresh_stable G x ∉ G.
Fixpoint vars_up_to (n:nat) :=
match n with
| S n ⇒ {n; vars_up_to n}
| 0 ⇒ ∅
end.
Lemma in_vars_up_to n m
: n < m → n ∈ vars_up_to m.
Lemma in_vars_up_to´ n m
: n ≤ m → n ∈ vars_up_to (m + 1).
Lemma vars_up_to_incl n m
: n ≤ m → vars_up_to n ⊆ vars_up_to m.
Lemma vars_up_to_max n m
: vars_up_to (max n m) [=] vars_up_to n ∪ vars_up_to m.
Section FreshList.
Variable fresh : set var → var.
Fixpoint fresh_list (G:set var) (n:nat) : list var :=
match n with
| 0 ⇒ nil
| S n ⇒ let x := fresh G in x::fresh_list (G ∪ {{x}}) n
end.
Lemma fresh_list_length (G:set var) n
: length (fresh_list G n) = n.
Hypothesis fresh_spec : ∀ G, fresh G ∉ G.
Definition fresh_set (G:set var) (n:nat) : set var :=
of_list (fresh_list G n).
Lemma fresh_list_spec : ∀ (G:set var) n, (of_list (fresh_list G n)) ∩ G [=] ∅.
Lemma fresh_set_spec
: ∀ (G:set var) n, (fresh_set G n) ∩ G [=] ∅.
Lemma fresh_list_unique (G: set var) n
: unique (fresh_list G n).
Hypothesis fresh_small : ∀ G : set var, fresh G ≤ SetInterface.cardinal G.
Lemma least_fresh_list_small G n
: ∀ i x, get (fresh_list G n) i x → x < cardinal G + n.
Lemma least_fresh_list_small_vars_up_to G n
: of_list (fresh_list G n) ⊆ vars_up_to (cardinal G + n).
End FreshList.
Lemma inverse_on_update_fresh_list (D:set var) (Z:list var) (ϱ ϱ´ : var → var)
: inverse_on (D \ of_list Z) ϱ ϱ´
→ inverse_on D (update_with_list Z (fresh_list fresh (lookup_set ϱ (D \ of_list Z)) (length Z)) ϱ)
(update_with_list (fresh_list fresh (lookup_set ϱ (D \ of_list Z)) (length Z)) Z ϱ´).