From 034bdcadbd79d3e62b40924852ec9bc3152b118c Mon Sep 17 00:00:00 2001
From: Johannes Kloos
Date: Thu, 9 Nov 2017 22:16:13 +0100
Subject: [PATCH] Renamed subset_difference_in and moved to collection

theories/collections.v  3 +++
theories/infinite.v  7 ++
2 files changed, 5 insertions(+), 5 deletions()
diff git a/theories/collections.v b/theories/collections.v
index 36304e9..ba3a1fd 100644
 a/theories/collections.v
+++ b/theories/collections.v
@@ 620,6 +620,9 @@ Section collection.
Proof. set_solver. Qed.
Lemma difference_disjoint X Y : X ## Y → X ∖ Y ≡ X.
Proof. set_solver. Qed.
+ Lemma subset_difference_elem_of {x: A} {s: C} (inx: x ∈ s): s ∖ {[ x ]} ⊂ s.
+ Proof. set_solver. Qed.
+
Lemma difference_mono X1 X2 Y1 Y2 :
X1 ⊆ X2 → Y2 ⊆ Y1 → X1 ∖ Y1 ⊆ X2 ∖ Y2.
diff git a/theories/infinite.v b/theories/infinite.v
index fb950ab..c31d73a 100644
 a/theories/infinite.v
+++ b/theories/infinite.v
@@ 27,13 +27,10 @@ Qed.
Section Fresh.
Context `{FinCollection A C} `{Infinite A, !RelDecision (@elem_of A C _)}.
 Lemma subset_difference_in {x: A} {s: C} (inx: x ∈ s): s ∖ {[ x ]} ⊂ s.
 Proof. set_solver. Qed.

Definition fresh_generic_body (s: C) (rec: ∀ s', s' ⊂ s → nat → A) (n: nat) :=
let cand := inject n in
match decide (cand ∈ s) with
  left H => rec _ (subset_difference_in H) (S n)
+  left H => rec _ (subset_difference_elem_of H) (S n)
 right _ => cand
end.
Lemma fresh_generic_body_proper s (f g: ∀ y, y ⊂ s → nat → A):
@@ 64,7 +61,7 @@ Section Fresh.
induction s as [s IH] using (well_founded_ind collection_wf); intro.
setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body.
destruct decide as [casecase]; eauto with omega.
 destruct (IH _ (subset_difference_in case) (S n)) as [m [mbound [eqfix [notin inbelow]]]].
+ destruct (IH _ (subset_difference_elem_of case) (S n)) as [m [mbound [eqfix [notin inbelow]]]].
exists m; repeat split; auto with omega.
 rewrite not_elem_of_difference, elem_of_singleton in notin.
destruct notin as [??%inject_injective]; auto with omega.

2.26.2