From 8a43c1bb12e1fa3ff407f0e80061325290996a3d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Mon, 2 Mar 2015 18:42:09 +0100
Subject: [PATCH] Remove duplicate mem_allocable notion.
---
theories/collections.v | 47 +++++++++++++++++++++++++++++++-----------
theories/fin_map_dom.v | 6 ++++++
2 files changed, 41 insertions(+), 12 deletions(-)
diff --git a/theories/collections.v b/theories/collections.v
index 953b12c..c7b1e42 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 ae01fcf..fbdd637 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.
--
GitLab