Merge branch 'robbert/infinite' into 'master'

Overhaul of the `Infinite`/`Fresh` infrastructure

See merge request iris/stdpp!58

theories/base.v

@@ -6,6 +6,7 @@ abstract interfaces for ordered structures, sets, and various other data
 structures. *)
 
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
+From Coq Require Import Permutation.
 Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
@@ -1210,17 +1211,26 @@ Class MonadSet M `{∀ A, ElemOf A (M A),
   elem_of_join {A} (X : M (M A)) (x : A) : x ∈ mjoin X ↔ ∃ Y, x ∈ Y ∧ Y ∈ X
 }.
 
-(** The function [fresh X] yields an element that is not contained in [X]. We
-will later prove that [fresh] is [Proper] with respect to the induced setoid
-equality on sets. *)
+(** The [Infinite A] class axiomatizes types [A] with infinitely many elements.
+It contains a function [fresh : list A → A] that given a list [xs] gives an
+element [fresh xs ∉ xs].
+
+We do not directly make [fresh] a field of the [Infinite] class, but use a
+separate operational type class [Fresh] for it. That way we can overload [fresh]
+to pick fresh elements from other data structure like sets. See the file
+[fin_sets], where we define [fresh : C → A] for any finite set implementation
+[FinSet C A].
+
+Note: we require [fresh] to respect permutations, which is needed to define the
+aforementioned [fresh] function on finite sets that respects set equality. *)
 Class Fresh A C := fresh: C → A.
 Hint Mode Fresh - ! : typeclass_instances.
 Instance: Params (@fresh) 3 := {}.
-Class FreshSpec A C `{ElemOf A C,
-    Empty C, Singleton A C, Union C, Fresh A C} : Prop := {
-  fresh_set_semi_set :>> SemiSet A C;
-  fresh_proper_alt X Y : (∀ x, x ∈ X ↔ x ∈ Y) → fresh X = fresh Y;
-  is_fresh (X : C) : fresh X ∉ X
+
+Class Infinite A := {
+  infinite_fresh :> Fresh A (list A);
+  infinite_is_fresh (xs : list A) : fresh xs ∉ xs;
+  infinite_fresh_Permutation :> Proper (@Permutation A ==> (=)) fresh;
 }.
 
 (** * Miscellaneous *)

theories/fin_sets.v

@@ -7,7 +7,9 @@ From stdpp Require Import relations.
 From stdpp Require Export numbers sets.
 Set Default Proof Using "Type*".
 
+(** Operations *)
 Instance set_size `{Elements A C} : Size C := length ∘ elements.
+
 Definition set_fold `{Elements A C} {B}
   (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
 
@@ -21,6 +23,28 @@ Definition set_map `{Elements A C, Singleton B D, Empty D, Union D}
   list_to_set (f <$> elements X).
 Typeclasses Opaque set_map.
 
+Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C :=
+  fresh ∘ elements.
+Typeclasses Opaque set_filter.
+
+(** We generalize the [fresh] operation on sets to generate lists of fresh
+elements w.r.t. a set [X]. *)
+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.
+Instance: Params (@fresh_list) 6 := {}.
+
+(** The following inductive predicate classifies that a list of elements is
+in fact fresh w.r.t. a set [X]. *)
+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).
+
+(** Properties **)
 Section fin_set.
 Context `{FinSet A C}.
 Implicit Types X Y : C.
@@ -342,4 +366,58 @@ Proof.
   - intros Hinf X. destruct (Hinf (elements X)). set_solver.
   - intros Hinf xs. destruct (Hinf (list_to_set xs)). set_solver.
 Qed.
+
+Section infinite.
+  Context `{Infinite A}.
+
+  (** Properties about the [fresh] operation on finite sets *)
+  Global Instance fresh_proper: Proper ((≡@{C}) ==> (=)) fresh.
+  Proof. unfold fresh, set_fresh. solve_proper. Qed.
+
+  Lemma is_fresh X : fresh X ∉ X.
+  Proof.
+    unfold fresh, set_fresh. rewrite <-elem_of_elements. apply infinite_is_fresh.
+  Qed.
+  Lemma exist_fresh X : ∃ x, x ∉ X.
+  Proof. exists (fresh X). apply is_fresh. Qed.
+
+  (** Properties about the [fresh_list] operation on finite sets *)
+  Global Instance fresh_list_proper n : Proper ((≡@{C}) ==> (=)) (fresh_list n).
+  Proof. induction n as [|n IH]; intros ?? E; by setoid_subst. 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 Forall_fresh_subseteq X Y xs :
+    Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs.
+  Proof. rewrite !Forall_fresh_alt; set_solver. 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|].
+    rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|].
+    apply IH in Hin; set_solver.
+  Qed.
+  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; set_solver.
+  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 infinite.
 End fin_set.

theories/gmap.v

@@ -264,9 +264,3 @@ Proof.
   - by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
   - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
 Qed.
-
-(** * Fresh elements *)
-Instance gset_fresh `{Countable A, Infinite A} : Fresh A (gset A) :=
-  fresh_generic.
-Instance gset_fresh_spec `{Countable A, Infinite A} : FreshSpec A (gset A) :=
-  fresh_generic_spec.

theories/nmap.v

@@ -84,20 +84,3 @@ Qed.
 Notation Nset := (mapset Nmap).
 Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
 Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
-
-(** * Fresh numbers *)
-Definition Nfresh {A} (m : Nmap A) : N :=
-  match m with NMap None _ => 0 | NMap _ m => Npos (Pfresh m) end.
-Lemma Nfresh_fresh {A} (m : Nmap A) : m !! Nfresh m = None.
-Proof. destruct m as [[]]. apply Pfresh_fresh. done. Qed. 
-
-Instance Nset_fresh : Fresh N Nset := λ X,
-  let (m) := X in Nfresh m.
-Instance Nset_fresh_spec : FreshSpec N Nset.
-Proof.
-  split.
-  - apply _.
-  - intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
-  - unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
-    by rewrite Nfresh_fresh.
-Qed.

theories/pmap.v

@@ -314,66 +314,3 @@ Qed.
 Notation Pset := (mapset Pmap).
 Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
 Instance Pmap_dom_spec : FinMapDom positive Pmap Pset := mapset_dom_spec.
-
-(** * Fresh numbers *)
-Fixpoint Pdepth {A} (m : Pmap_raw A) : nat :=
-  match m with
-  | PLeaf | PNode None _ _ => O | PNode _ l _ => S (Pdepth l)
-  end.
-Fixpoint Pfresh_at_depth {A} (m : Pmap_raw A) (d : nat) : option positive :=
-  match d, m with
-  | O, (PLeaf | PNode None _ _) => Some 1
-  | S d, PNode _ l r =>
-     match Pfresh_at_depth l d with
-     | Some i => Some (i~0) | None => (~1) <$> Pfresh_at_depth r d
-     end
-  | _, _ => None
-  end.
-Fixpoint Pfresh_go {A} (m : Pmap_raw A) (d : nat) : option positive :=
-  match d with
-  | O => None
-  | S d =>
-     match Pfresh_go m d with
-     | Some i => Some i | None => Pfresh_at_depth m d
-     end
-  end.
-Definition Pfresh {A} (m : Pmap A) : positive :=
-  let d := Pdepth (pmap_car m) in
-  match Pfresh_go (pmap_car m) d with
-  | Some i => i | None => Pos.shiftl_nat 1 d
-  end.
-
-Lemma Pfresh_at_depth_fresh {A} (m : Pmap_raw A) d i :
-  Pfresh_at_depth m d = Some i → m !! i = None.
-Proof.
-  revert i m; induction d as [|d IH].
-  { intros i [|[] l r] ?; naive_solver. }
-  intros i [|o l r] ?; simplify_eq/=.
-  destruct (Pfresh_at_depth l d) as [i'|] eqn:?,
-    (Pfresh_at_depth r d) as [i''|] eqn:?; simplify_eq/=; auto.
-Qed.
-Lemma Pfresh_go_fresh {A} (m : Pmap_raw A) d i :
-  Pfresh_go m d = Some i → m !! i = None.
-Proof.
-  induction d as [|d IH]; intros; simplify_eq/=.
-  destruct (Pfresh_go m d); eauto using Pfresh_at_depth_fresh.
-Qed.
-Lemma Pfresh_depth {A} (m : Pmap_raw A) :
-  m !! Pos.shiftl_nat 1 (Pdepth m) = None.
-Proof. induction m as [|[x|] l IHl r IHr]; auto. Qed.
-Lemma Pfresh_fresh {A} (m : Pmap A) : m !! Pfresh m = None.
-Proof.
-  destruct m as [m ?]; unfold lookup, Plookup, Pfresh; simpl.
-  destruct (Pfresh_go m _) eqn:?; eauto using Pfresh_go_fresh, Pfresh_depth.
-Qed.
-
-Instance Pset_fresh : Fresh positive Pset := λ X,
-  let (m) := X in Pfresh m.
-Instance Pset_fresh_spec : FreshSpec positive Pset.
-Proof.
-  split.
-  - apply _.
-  - intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
-  - unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
-    by rewrite Pfresh_fresh.
-Qed.

theories/sets.v

@@ -865,69 +865,6 @@ Section more_quantifiers.
   Proof. unfold set_Exists. naive_solver. Qed.
 End more_quantifiers.
 
-(** * Fresh elements *)
-(** We collect some properties on the [fresh] operation. In particular we
-generalize [fresh] to generate lists of fresh elements. *)
-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.
-Instance: Params (@fresh_list) 6 := {}.
-
-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).
-
-Section fresh.
-  Context `{FreshSpec A C}.
-  Implicit Types X Y : C.
-
-  Global Instance fresh_proper: Proper ((≡@{C}) ==> (=)) fresh.
-  Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
-  Global Instance fresh_list_proper n : Proper ((≡@{C}) ==> (=)) (fresh_list n).
-  Proof. induction n as [|n IH]; intros ?? E; by setoid_subst. Qed.
-
-  Lemma exist_fresh X : ∃ x, x ∉ X.
-  Proof. exists (fresh X). apply is_fresh. 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 Forall_fresh_subseteq X Y xs :
-    Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs.
-  Proof. rewrite !Forall_fresh_alt; set_solver. 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|].
-    rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|].
-    apply IH in Hin; set_solver.
-  Qed.
-  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; set_solver.
-  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.
-
 (** * Properties of implementations of sets that form a monad *)
 Section set_monad.
   Context `{MonadSet M}.
@@ -1003,6 +940,11 @@ Section pred_finite_infinite.
   Lemma pred_not_infinite_finite {A} (P : A → Prop) :
     pred_infinite P → pred_finite P → False.
   Proof. intros Hinf [xs ?]. destruct (Hinf xs). set_solver. Qed.
+
+  Lemma pred_infinite_True `{Infinite A} : pred_infinite (λ _: A, True).
+  Proof.
+    intros xs. exists (fresh xs). split; [done|]. apply infinite_is_fresh.
+  Qed.
 End pred_finite_infinite.
 
 Section set_finite_infinite.