diff --git a/theories/collections.v b/theories/collections.v index 953b12cfb05d5d64b914672036016e3b566c52f4..c7b1e426a3d9fd91f352ac6f0a29f5aa3c54c5ab 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -430,16 +430,19 @@ End more_quantifiers. (** * Fresh elements *) (** We collect some properties on the [fresh] operation. In particular we generalize [fresh] to generate lists of fresh elements. *) -Section fresh. - Context `{FreshSpec A C} . +Fixpoint fresh_list `{Fresh A C, Union C, Singleton A C} + (n : nat) (X : C) : list A := + match n with + | 0 => [] + | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X) + end. +Inductive Forall_fresh `{ElemOf A C} (X : C) : list A → Prop := + | Forall_fresh_nil : Forall_fresh X [] + | Forall_fresh_cons x xs : + x ∉ xs → x ∉ X → Forall_fresh X xs → Forall_fresh X (x :: xs). - Definition fresh_sig (X : C) : { x : A | x ∉ X } := - exist (∉ X) (fresh X) (is_fresh X). - Fixpoint fresh_list (n : nat) (X : C) : list A := - match n with - | 0 => [] - | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X) - end. +Section fresh. + Context `{FreshSpec A C}. Global Instance fresh_proper: Proper ((≡) ==> (=)) fresh. Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed. @@ -448,18 +451,38 @@ Section fresh. intros ? n ->. induction n as [|n IH]; intros ?? E; f_equal'; [by rewrite E|]. apply IH. by rewrite E. Qed. + + Lemma Forall_fresh_NoDup X xs : Forall_fresh X xs → NoDup xs. + Proof. induction 1; by constructor. Qed. + Lemma Forall_fresh_elem_of X xs x : Forall_fresh X xs → x ∈ xs → x ∉ X. + Proof. + intros HX; revert x; rewrite <-Forall_forall. + by induction HX; constructor. + Qed. + Lemma Forall_fresh_alt X xs : + Forall_fresh X xs ↔ NoDup xs ∧ ∀ x, x ∈ xs → x ∉ X. + Proof. + split; eauto using Forall_fresh_NoDup, Forall_fresh_elem_of. + rewrite <-Forall_forall. + intros [Hxs Hxs']. induction Hxs; decompose_Forall_hyps; constructor; auto. + Qed. + Lemma fresh_list_length n X : length (fresh_list n X) = n. Proof. revert X. induction n; simpl; auto. Qed. Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X. Proof. - revert X. induction n as [|n IH]; intros X; simpl; [by rewrite elem_of_nil|]. + revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|]. rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|]. apply IH in Hin; solve_elem_of. Qed. - Lemma fresh_list_nodup n X : NoDup (fresh_list n X). + Lemma NoDup_fresh_list n X : NoDup (fresh_list n X). Proof. revert X. induction n; simpl; constructor; auto. - intros Hin. apply fresh_list_is_fresh in Hin. solve_elem_of. + intros Hin; apply fresh_list_is_fresh in Hin; solve_elem_of. + Qed. + Lemma Forall_fresh_list X n : Forall_fresh X (fresh_list n X). + Proof. + rewrite Forall_fresh_alt; eauto using NoDup_fresh_list, fresh_list_is_fresh. Qed. End fresh. diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v index ae01fcf4742de84a49ce4033fee49db46b6a6289..fbdd637861adca1721a8d74d8385b6be72e73480 100644 --- a/theories/fin_map_dom.v +++ b/theories/fin_map_dom.v @@ -44,6 +44,12 @@ Proof. intros E. apply map_empty. intros. apply not_elem_of_dom. rewrite E. solve_elem_of. Qed. +Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m) ≡ dom D m. +Proof. + apply elem_of_equiv; intros j; rewrite !elem_of_dom; unfold is_Some. + destruct (decide (i = j)); simplify_map_equality'; eauto. + destruct (m !! j); naive_solver. +Qed. Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m. Proof. apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom.