diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 138 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 3 |
3 files changed, 146 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2826491..26a214d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -8,6 +8,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ## [Unreleased] +### Added + +- Added fixpoint and cofixpoint constructions to `finset`: `fixset`, + `cofixset` and `fix_order`, with a few theorems about them + ### Changed - `eqVneq` lemma is changed from `{x = y} + {x != y}` to diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index c01fb39..beac009 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -72,6 +72,16 @@ From mathcomp Require Import choice fintype finfun bigop. (* comprehension as Coq parsing confuses [x | P] and [E | x]. *) (* minset p A == A is a minimal set satisfying p. *) (* maxset p A == A is a maximal set satisfying p. *) +(* Provided a monotonous function F : {set T} -> {set T}, we get fixpoints *) +(* fixset F := iter #|T| F set0 *) +(* == the least fixpoint of F *) +(* == the minimal set such that F X == X *) +(* fix_order F x == the minimum number of iterations so that *) +(* x is in iter (fix_order F x) F set0 *) +(* funsetC F := fun X => ~: F (~: X) *) +(* cofixset F == the greatest fixpoint of F *) +(* == the maximal set such that F X == X *) +(* := ~: fixset (funsetC F) *) (* We also provide notations A :=: B, A :<>: B, A :==: B, A :!=: B, A :=P: B *) (* that specialize A = B, A <> B, A == B, etc., to {set _}. This is useful *) (* for subtypes of {set T}, such as {group T}, that coerce to {set T}. *) @@ -2213,3 +2223,131 @@ Arguments setCK {T}. Arguments minsetP {T P A}. Arguments maxsetP {T P A}. Prenex Implicits minset maxset. + +Section SetFixpoint. + +Section Least. +Variables (T : finType) (F : {set T} -> {set T}). +Hypothesis (F_mono : {homo F : X Y / X \subset Y}). + +Let n := #|T|. +Let iterF i := iter i F set0. + +Lemma subset_iterS i : iterF i \subset iterF i.+1. +Proof. by elim: i => [| i IHi]; rewrite /= ?sub0set ?F_mono. Qed. + +Lemma subset_iter : {homo iterF : i j / i <= j >-> i \subset j}. +Proof. +by apply: homo_leq => //[? ? ?|]; [apply: subset_trans|apply: subset_iterS]. +Qed. + +Definition fixset := iterF n. + +Lemma fixsetK : F fixset = fixset. +Proof. +suff /'exists_eqP[x /= e]: [exists k : 'I_n.+1, iterF k == iterF k.+1]. + by rewrite /fixset -(subnK (leq_ord x)) /iterF iter_add iter_fix. +apply: contraT; rewrite negb_exists => /forallP /(_ (Ordinal _)) /= neq_iter. +suff iter_big k : k <= n.+1 -> k <= #|iter k F set0|. + by have := iter_big _ (leqnn _); rewrite ltnNge max_card. +elim: k => [|k IHk] k_lt //=; apply: (leq_ltn_trans (IHk (ltnW k_lt))). +by rewrite proper_card// properEneq// subset_iterS neq_iter. +Qed. +Hint Resolve fixsetK. + +Lemma minset_fix : minset [pred X | F X == X] fixset. +Proof. +apply/minsetP; rewrite inE fixsetK eqxx; split=> // X /eqP FXeqX Xsubfix. +apply/eqP; rewrite eqEsubset Xsubfix/=. +suff: fixset \subset iter n F X by rewrite iter_fix. +by rewrite /fixset; elim: n => //= [|m IHm]; rewrite ?sub0set ?F_mono. +Qed. + +Lemma fixsetKn k : iter k F fixset = fixset. +Proof. by rewrite iter_fix. Qed. + +Lemma iter_sub_fix k : iterF k \subset fixset. +Proof. +have [/subset_iter //|/ltnW/subnK<-] := leqP k n; +by rewrite /iterF iter_add fixsetKn. +Qed. + +Lemma fix_order_proof x : x \in fixset -> exists n, x \in iterF n. +Proof. by move=> x_fix; exists n. Qed. + +Definition fix_order (x : T) := + if (x \in fixset) =P true isn't ReflectT x_fix then 0 + else (ex_minn (fix_order_proof x_fix)). + +Lemma fix_order_le_max (x : T) : fix_order x <= n. +Proof. +rewrite /fix_order; case: eqP => //= x_in. +by case: ex_minnP => //= ? ?; apply. +Qed. + +Lemma in_iter_fix_orderE (x : T) : + (x \in iterF (fix_order x)) = (x \in fixset). +Proof. +rewrite /fix_order; case: eqP; last by move=>/negP/negPf->; rewrite inE. +by move=> x_in; case: ex_minnP => m ->; rewrite x_in. +Qed. + +Lemma fix_order_gt0 (x : T) : (fix_order x > 0) = (x \in fixset). +Proof. +rewrite /fix_order; case: eqP => [x_in|/negP/negPf->//]. +by rewrite x_in; case: ex_minnP => -[|m]; rewrite ?inE//= => _; apply. +Qed. + +Lemma fix_order_eq0 (x : T) : (fix_order x == 0) = (x \notin fixset). +Proof. by rewrite -fix_order_gt0 -ltnNge ltnS leqn0. Qed. + +Lemma in_iter_fixE (x : T) k : (x \in iterF k) = (0 < fix_order x <= k). +Proof. +rewrite /fix_order; case: eqP => //= [x_in|/negP xNin]; last first. + by apply: contraNF xNin; apply/subsetP/iter_sub_fix. +case: ex_minnP => -[|m]; rewrite ?inE// => xm mP. +by apply/idP/idP=> [/mP//|lt_mk]; apply: subsetP xm; apply: subset_iter. +Qed. + +Lemma in_iter (x : T) k : x \in fixset -> fix_order x <= k -> x \in iterF k. +Proof. by move=> x_in xk; rewrite in_iter_fixE fix_order_gt0 x_in xk. Qed. + +Lemma notin_iter (x : T) k : k < fix_order x -> x \notin iterF k. +Proof. by move=> k_le; rewrite in_iter_fixE negb_and orbC -ltnNge k_le. Qed. + +Lemma fix_order_small x k : x \in iterF k -> fix_order x <= k. +Proof. by rewrite in_iter_fixE => /andP[]. Qed. + +Lemma fix_order_big x k : x \in fixset -> x \notin iterF k -> fix_order x > k. +Proof. by move=> x_in; rewrite in_iter_fixE fix_order_gt0 x_in /= -ltnNge. Qed. + +Lemma le_fix_order (x y : T) : y \in iterF (fix_order x) -> + fix_order y <= fix_order x. +Proof. exact: fix_order_small. Qed. + +End Least. + +Section Greatest. +Variables (T : finType) (F : {set T} -> {set T}). +Hypothesis (F_mono : {homo F : X Y / X \subset Y}). + +Definition funsetC X := ~: (F (~: X)). +Lemma funsetC_mono : {homo funsetC : X Y / X \subset Y}. +Proof. by move=> *; rewrite subCset setCK F_mono// subCset setCK. Qed. +Hint Resolve funsetC_mono. + +Definition cofixset := ~: fixset funsetC. + +Lemma cofixsetK : F cofixset = cofixset. +Proof. by rewrite /cofixset -[in RHS]fixsetK ?setCK. Qed. + +Lemma maxset_cofix : maxset [pred X | F X == X] cofixset. +Proof. +rewrite maxminset setCK. +rewrite (@minset_eq _ _ [pred X | funsetC X == X]) ?minset_fix//. +by move=> X /=; rewrite (can2_eq setCK setCK). +Qed. + +End Greatest. + +End SetFixpoint. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index ad44d3b..5b667f0 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -826,6 +826,9 @@ Proof. by elim: n => //= n ->. Qed. Lemma eq_iter f f' : f =1 f' -> forall n, iter n f =1 iter n f'. Proof. by move=> eq_f n x; elim: n => //= n ->; rewrite eq_f. Qed. +Lemma iter_fix n f x : f x = x -> iter n f x = x. +Proof. by move=> fixf; elim: n => //= n ->. Qed. + Lemma eq_iteri f f' : f =2 f' -> forall n, iteri n f =1 iteri n f'. Proof. by move=> eq_f n x; elim: n => //= n ->; rewrite eq_f. Qed. |