Return of PR #226: adds relevant theorems when fcycle f (orbit f x) and the needed lemmas (#261)

* adds relevant theorems when fcycle f (orbit f x) and the needed lemmas

* Generalize f_step lemmas

* Generalizations, shorter proofs, bugfixes, CHANGELOG

- changelog, renamings and comments
- renaming `homo_cycle` to `mem_fcycle` and other small renamings
- name swap `mem_orbit` and `in_orbit`
- simplifications
- generalization following @pi8027's comment
- Getting rid of many uniquness condition in `fingraph.v`
- added cases to the equivalence `orbitPcycle`
- added `cycle_catC`

1 files changed, 47 insertions, 11 deletions

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 5566a44..0ddd382 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -180,12 +180,17 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 (*  if T : [<-> P0; P1; ..; Pn]  is such an equivalence, and i, j are in nat  *)
 (*  then T i j is a proof of the equivalence Pi <-> Pj between Pi and Pj;     *)
 (*  when i (resp. j) is out of bounds, Pi (resp. Pj) defaults to P0.          *)
+(*  The tactic tfae splits the goal into n+1 implications to prove.           *)
+(*  An example of use can be found in fingraph theorem orbitPcycle.           *)
 (******************************************************************************)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Reserved Notation "[ '<->' P0 ; P1 ; .. ; Pn ]"
+  (at level 0, format "[ '<->' '['  P0 ;  '/' P1 ;  '/'  .. ;  '/'  Pn ']' ]").
+
 Delimit Scope seq_scope with SEQ.
 Open Scope seq_scope.
 
@@ -384,6 +389,11 @@ Lemma nth_rcons s x n :
     if n < size s then nth s n else if n == size s then x else x0.
 Proof. by elim: s n => [|y s IHs] [] //=; apply: nth_nil. Qed.
 
+Lemma nth_rcons_default s i : nth (rcons s x0) i = nth s i.
+Proof.
+by rewrite nth_rcons; case: ltngtP => //[/ltnW ?|->]; rewrite nth_default.
+Qed.
+
 Lemma nth_ncons m x s n :
   nth (ncons m x s) n = if n < m then x else nth s (n - m).
 Proof. by elim: m n => [|m IHm] []. Qed.
@@ -1275,6 +1285,15 @@ Qed.
 Lemma undup_nil s : undup s = [::] -> s = [::].
 Proof. by case: s => //= x s; rewrite -mem_undup; case: ifP; case: undup. Qed.
 
+Lemma undup_cat s t :
+  undup (s ++ t) = [seq x <- undup s | x \notin t] ++ undup t.
+Proof. by elim: s => //= x s ->; rewrite mem_cat; do 2 case: in_mem => //=. Qed.
+
+Lemma undup_rcons s x : undup (rcons s x) = rcons [seq y <- undup s | y != x] x.
+Proof.
+by rewrite -!cats1 undup_cat; congr cat; apply: eq_filter => y; rewrite inE.
+Qed.
+
 (* Lookup *)
 
 Definition index x := find (pred1 x).
@@ -1336,16 +1355,24 @@ Proof. by move=> x; rewrite -{2}(cat_take_drop n0 s) !mem_cat /= orbC. Qed.
 Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2).
 Proof. by apply: inj_eq; apply: rot_inj. Qed.
 
-Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.
+End EqSeq.
 
-Lemma rot_to s x : x \in s -> rot_to_spec s x.
+Section RotIndex.
+Variables (T : eqType).
+Implicit Types x y z : T.
+
+Lemma rot_index s x (i := index x s) : x \in s ->
+  rot i s = x :: (drop i.+1 s ++ take i s).
 Proof.
-move=> s_x; pose i := index x s; exists i (drop i.+1 s ++ take i s).
-rewrite -cat_cons {}/i; congr cat; elim: s s_x => //= y s IHs.
-by rewrite in_cons; case: eqVneq => // -> _; rewrite drop0.
+by move=> x_s; rewrite /rot (drop_nth x) ?index_mem ?nth_index// cat_cons.
 Qed.
 
-End EqSeq.
+Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.
+
+Lemma rot_to s x : x \in s -> rot_to_spec s x.
+Proof. by move=> /rot_index /RotToSpec. Qed.
+
+End RotIndex.
 
 Definition inE := (mem_seq1, in_cons, inE).
 
@@ -2825,6 +2852,14 @@ Lemma flatten_map1 (S T : Type) (f : S -> T) s :
   flatten [seq [:: f x] | x <- s] = map f s.
 Proof. by elim: s => //= s0 s ->. Qed.
 
+Lemma undup_flatten_nseq n (T : eqType) (s : seq T) : 0 < n ->
+  undup (flatten (nseq n s)) = undup s.
+Proof.
+elim: n => [|[|n]/= IHn]//= _; rewrite ?cats0// undup_cat {}IHn//.
+rewrite (@eq_in_filter _ _ pred0) ?filter_pred0// => x.
+by rewrite mem_undup mem_cat => ->.
+Qed.
+
 Lemma sumn_flatten (ss : seq (seq nat)) :
   sumn (flatten ss) = sumn (map sumn ss).
 Proof. by elim: ss => // s ss /= <-; apply: sumn_cat. Qed.
@@ -3326,8 +3361,8 @@ Definition all_iff (P0 : Prop) (Ps : seq Prop) : Prop :=
     if Qs is Q :: Qs then all_iff_and (P -> Q) (loop Q Qs) else P -> P0 in
   loop P0 Ps.
 
-Lemma all_iffLR P0 Ps :
-   all_iff P0 Ps -> forall m n, nth P0 (P0 :: Ps) m -> nth P0 (P0 :: Ps) n.
+Lemma all_iffLR P0 Ps : all_iff P0 Ps ->
+  forall m n, nth P0 (P0 :: Ps) m -> nth P0 (P0 :: Ps) n.
 Proof.
 move=> iffPs; have PsS n: nth P0 Ps n -> nth P0 Ps n.+1.
   elim: n P0 Ps iffPs => [|n IHn] P0 [|P [|Q Ps]] //= [iP0P] //; first by case.
@@ -3352,9 +3387,10 @@ Arguments all_iffP {P0 Ps}.
 Coercion all_iffP : all_iff >-> Funclass.
 
 (* This means "the following are all equivalent: P0, ... Pn" *)
-Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (all_iff P0 (P1 :: .. [:: Pn] ..))
-  (at level 0, format "[ '<->' '['  P0 ;  '/' P1 ;  '/'  .. ;  '/'  Pn ']' ]")
-  : form_scope.
+Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" :=
+  (all_iff P0 (@cons Prop P1 (.. (@cons Prop Pn nil) ..))) : form_scope.
+
+Ltac tfae := do !apply: AllIffConj.
 
 (* Temporary backward compatibility. *)
 Notation perm_eqP := (deprecate perm_eqP permP) (only parsing).