Fixpoint theorems in finset

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.