(* Copyright (c) 2012, 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 . *) Require Import Permutation ars. Require Export collections numbers listset. 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}. Global Instance elements_proper: Proper ((≡) ==> Permutation) elements. Proof. intros ?? E. apply NoDup_Permutation. * apply elements_nodup. * apply elements_nodup. * intros. by rewrite <-!elements_spec, E. Qed. Global Instance collection_size_proper: Proper ((≡) ==> (=)) size. Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed. Lemma size_empty : size (∅ : C) = 0. Proof. unfold size, collection_size. simpl. rewrite (elem_of_nil_inv (elements ∅)). * done. * intro. rewrite <-elements_spec. solve_elem_of. Qed. Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅. Proof. intros. apply equiv_empty. intro. rewrite elements_spec. rewrite (nil_length (elements X)). by rewrite elem_of_nil. done. Qed. Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅. Proof. split. apply size_empty_inv. intros E. by rewrite E, 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. change (length (elements {[ x ]}) = length [x]). apply Permutation_length, NoDup_Permutation. * apply elements_nodup. * apply NoDup_singleton. * intros. by rewrite <-elements_spec, elem_of_singleton, elem_of_list_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 !elements_spec. generalize (elements X). intros [|? l]. * done. * injection 1. intro. rewrite (nil_length l) by done. simpl. rewrite !elem_of_list_singleton. congruence. Qed. Lemma elem_of_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅. Proof. destruct (elements X) as [|x xs] eqn:E. * right. apply equiv_empty. intros x Ex. by rewrite elements_spec, E, elem_of_nil in Ex. * left. exists x. rewrite elements_spec, E. by constructor. Qed. Lemma choose X : X ≢ ∅ → ∃ x, x ∈ X. Proof. destruct (elem_of_or_empty X) as [[x ?]|?]. * by exists x. * done. Qed. Lemma size_pos_choose X : 0 < size X → ∃ x, x ∈ X. Proof. intros E1. apply choose. intros E2. rewrite E2, size_empty in E1. by apply (Lt.lt_n_0 0). Qed. Lemma size_1_choose X : size X = 1 → ∃ x, X ≡ {[ x ]}. Proof. intros E. destruct (size_pos_choose X). * rewrite E. auto with arith. * exists x. apply elem_of_equiv. split. + intro. 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 elements_nodup. * apply NoDup_app; repeat split; try apply elements_nodup. intros x. rewrite <-!elements_spec. esolve_elem_of. * intros. rewrite elem_of_app, <-!elements_spec. solve_elem_of. 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 (elements_spec _). Defined. Global Program Instance collection_subseteq_dec_slow (X Y : C) : Decision (X ⊆ Y) | 100 := match decide_rel (=) (size (X ∖ Y)) 0 with | left E1 => left _ | right E1 => right _ end. Next Obligation. intros x Ex; apply dec_stable; intro. destruct (proj1 (elem_of_empty x)). apply (size_empty_inv _ E1). by rewrite elem_of_difference. Qed. Next Obligation. intros 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 esolve_elem_of. rewrite <-union_difference, (commutative (∪)); 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 (@subset C _). Proof. apply well_founded_lt_compat with size, subset_size. 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 (elem_of_or_empty X) as [[x ?]|HX]. * rewrite (union_difference {[ x ]} X) by solve_elem_of. apply Hadd. solve_elem_of. apply IH. esolve_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 elements_nodup. apply elements_spec. } induction 1 as [|x l ?? IH]; simpl. * intros X HX. setoid_rewrite elem_of_nil in HX. rewrite equiv_empty. done. esolve_elem_of. * intros X HX. setoid_rewrite elem_of_cons in HX. rewrite (union_difference {[ x ]} X) by esolve_elem_of. apply Hadd. solve_elem_of. apply IH. esolve_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). Proof. intros ?? E. apply (foldr_permutation R f b). * auto. * by rewrite E. Qed. Global Instance cforall_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (cforall P X) | 100. Proof. refine (cast_if (decide (Forall P (elements X)))); abstract (unfold cforall; setoid_rewrite elements_spec; by rewrite <-Forall_forall). Defined. Global Instance cexists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (cexists P X) | 100. Proof. refine (cast_if (decide (Exists P (elements X)))); abstract (unfold cexists; setoid_rewrite elements_spec; 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 (cexists (R x) X). End fin_collection.