(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on finite collections. Most
importantly, it implements a fold and size function and some useful induction
principles on finite collections . *)
From Coq Require Import Permutation.
From stdpp Require Import relations listset.
From stdpp Require Export numbers collections.
Instance collection_size `{Elements A C} : Size C := length ∘ elements.
Definition collection_fold `{Elements A C} {B}
(f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
Section fin_collection.
Context `{FinCollection A C}.
Implicit Types X Y : C.
Lemma fin_collection_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)).
Proof.
intros ?? E. apply NoDup_Permutation.
- apply NoDup_elements.
- apply NoDup_elements.
- intros. by rewrite !elem_of_elements, E.
Qed.
Lemma elements_empty : elements (∅ : C) = [].
Proof.
apply elem_of_nil_inv; intros x.
rewrite elem_of_elements, elem_of_empty; tauto.
Qed.
Lemma elements_union_singleton (X : C) x :
x ∉ X → elements ({[ x ]} ∪ X) ≡ₚ x :: elements X.
Proof.
intros ?; apply NoDup_Permutation.
{ apply NoDup_elements. }
{ by constructor; rewrite ?elem_of_elements; try apply NoDup_elements. }
intros y; rewrite elem_of_elements, elem_of_union, elem_of_singleton.
by rewrite elem_of_cons, elem_of_elements.
Qed.
Lemma elements_singleton x : elements {[ x ]} = [x].
Proof.
apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}),
elements_union_singleton, elements_empty by solve_elem_of.
Qed.
Lemma elements_contains X Y : X ⊆ Y → elements X `contains` elements Y.
Proof.
intros; apply NoDup_contains; auto using NoDup_elements.
intros x. rewrite !elem_of_elements; auto.
Qed.
Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _).
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
Lemma size_empty : size (∅ : C) = 0.
Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed.
Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
Proof.
intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
Qed.
Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅.
Proof. by rewrite size_empty_iff. Qed.
Lemma size_singleton (x : A) : size {[ x ]} = 1.
Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed.
Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
Proof.
unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
generalize (elements X). intros [|? l]; intro; simplify_eq/=.
rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence.
Qed.
Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
Proof.
destruct (elements X) as [|x l] eqn:HX; [right|left].
- apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
- exists x. rewrite <-elem_of_elements, HX. by left.
Qed.
Lemma collection_choose X : X ≢ ∅ → ∃ x, x ∈ X.
Proof. intros. by destruct (collection_choose_or_empty X). Qed.
Lemma collection_choose_L `{!LeibnizEquiv C} X : X ≠ ∅ → ∃ x, x ∈ X.
Proof. unfold_leibniz. apply collection_choose. Qed.
Lemma size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X.
Proof.
intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|].
contradict Hsz. rewrite HX, size_empty; lia.
Qed.
Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}.
Proof.
intros E. destruct (size_pos_elem_of X); auto with lia.
exists x. apply elem_of_equiv. split.
- rewrite elem_of_singleton. eauto using size_singleton_inv.
- solve_elem_of.
Qed.
Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
Proof.
intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
apply Permutation_length, NoDup_Permutation.
- apply NoDup_elements.
- apply NoDup_app; repeat split; try apply NoDup_elements.
intros x; rewrite !elem_of_elements; solve_elem_of.
- intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Qed.
Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
Proof.
refine (cast_if (decide_rel (∈) x (elements X)));
by rewrite <-(elem_of_elements _).
Defined.
Global Program Instance collection_subseteq_dec_slow (X Y : C) :
Decision (X ⊆ Y) | 100 :=
match decide_rel (=) (size (X ∖ Y)) 0 return _ with
| left _ => left _ | right _ => right _
end.
Next Obligation.
intros X Y E1 x ?; apply dec_stable; intro. destruct (proj1(elem_of_empty x)).
apply (size_empty_inv _ E1). by rewrite elem_of_difference.
Qed.
Next Obligation.
intros X Y E1 E2; destruct E1. apply size_empty_iff, equiv_empty. intros x.
rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
Qed.
Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
Proof.
rewrite <-size_union by solve_elem_of.
setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by solve_elem_of.
rewrite <-union_difference, (comm (∪)); solve_elem_of.
Qed.
Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Lemma subset_size X Y : X ⊂ Y → size X < size Y.
Proof.
intros. rewrite (union_difference X Y) by solve_elem_of.
rewrite size_union_alt, difference_twice.
cut (size (Y ∖ X) ≠ 0); [lia |].
by apply size_non_empty_iff, non_empty_difference.
Qed.
Lemma collection_wf : wf (strict (@subseteq C _)).
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Lemma collection_ind (P : C → Prop) :
Proper ((≡) ==> iff) P →
P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
Proof.
intros ? Hemp Hadd. apply well_founded_induction with (⊂).
{ apply collection_wf. }
intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
- rewrite (union_difference {[ x ]} X) by solve_elem_of.
apply Hadd. solve_elem_of. apply IH; solve_elem_of.
- by rewrite HX.
Qed.
Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
Proper ((=) ==> (≡) ==> iff) P →
P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
∀ X, P (collection_fold f b X) X.
Proof.
intros ? Hemp Hadd.
cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X).
{ intros help ?. apply help; [apply NoDup_elements|].
symmetry. apply elem_of_elements. }
induction 1 as [|x l ?? IH]; simpl.
- intros X HX. setoid_rewrite elem_of_nil in HX.
rewrite equiv_empty. done. solve_elem_of.
- intros X HX. setoid_rewrite elem_of_cons in HX.
rewrite (union_difference {[ x ]} X) by solve_elem_of.
apply Hadd. solve_elem_of. apply IH. solve_elem_of.
Qed.
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
(f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
(Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
Proper ((≡) ==> R) (collection_fold f b : C → B).
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
Global Instance set_Forall_dec `(P : A → Prop)
`{∀ x, Decision (P x)} X : Decision (set_Forall P X) | 100.
Proof.
refine (cast_if (decide (Forall P (elements X))));
abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements;
by rewrite <-Forall_forall).
Defined.
Global Instance set_Exists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X :
Decision (set_Exists P X) | 100.
Proof.
refine (cast_if (decide (Exists P (elements X))));
abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements;
by rewrite <-Exists_exists).
Defined.
Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X :
Decision (elem_of_upto R x X) | 100 := decide (set_Exists (R x) X).
End fin_collection.