diff --git a/theories/collections.v b/theories/collections.v index 36304e9bd02003a759e420b4b583aec91c1fe01e..ba3a1fd43f47f2a892eb430514a386f42c1a9dad 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 fb950ab963aae17f9e6127968061b9b3819f2f55..c31d73ac0fc41d24117f31e533d8b13f5573a6f0 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 [case|case]; 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.