shortening and refactoring

1 files changed, 50 insertions, 98 deletions

diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index f0f331e..dfba3c7 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -464,157 +464,110 @@ Qed.
 
 End Loop.
 
-Section subset_orbit.
+Section orbit_in.
 
 Variable S : pred_sort (predPredType T).
 
-Hypothesis stable : {in S, forall x, f x \in S}.
+Hypothesis f_in : {in S, forall x, f x \in S}.
 Hypothesis injf : {in S &, injective f}.
 
-Lemma stable_in_iter : {in S, forall x i, iter i f x \in S}.
-Proof. by move => x sx; elim =>[ | i] //; rewrite iterS; apply/stable. Qed.
+Lemma iter_in : {in S, forall x i, iter i f x \in S}.
+Proof. by move=> x xS; elim=> [|i /f_in]. Qed.
+
+Lemma finv_in : {in S, forall x, finv x \in S}.
+Proof. by move=> ??; rewrite iter_in. Qed.
 
 Lemma f_finv_in : {in S, cancel finv f}.
 Proof.
-move => x sx.
-move: (looping_order x) (orbit_uniq x).
+move=> x xS; move: (looping_order x) (orbit_uniq x).
 rewrite /looping /orbit -orderSpred looping_uniq /= /looping; set n := _.-1.
-case/predU1P=> // /trajectP[i lt_i_n]; rewrite -iterSr => /=.
-have [itnS  itiS] : iter n f x \in S /\ iter i f x \in S.
-  by split; apply/stable_in_iter.
-move/injf => /(_ itnS) /(_ itiS) ->.
-by case/trajectP; exists i.
+case/predU1P=> // /trajectP[i lt_i_n]; rewrite -iterSr.
+by move=> /injf ->; rewrite ?iter_in //; case/trajectP; exists i.
 Qed.
 
 Lemma finv_f_in : {in S, cancel f finv}.
-Proof.
-move => x sx; apply/injf=> //;[apply/stable_in_iter/stable => // | ].
-by rewrite f_finv_in ?stable.
-Qed.
-
-(* There is no pre-defined concept equivalent to bijective on a
-  subset, regardless of what happens outside the subset. *)
+Proof. by move=> x xS; apply/injf; rewrite ?iter_in ?f_finv_in ?f_in. Qed.
 
 Lemma finv_inj_in : {in S &, injective finv}.
-Proof.
-by move => x y sx sy q; rewrite -(f_finv_in sx) q (f_finv_in sy).
-Qed.
+Proof. by move=> x y xS yS q; rewrite -(f_finv_in xS) q f_finv_in. Qed.
 
-Lemma fconnect_sym_in :
-  {in S &, forall x y, fconnect f x y = fconnect f y x}.
+Lemma fconnect_sym_in : {in S &, forall x y, fconnect f x y = fconnect f y x}.
 Proof.
-suff Sf x y (sx : x \in S) (sy : y \in S): fconnect f x y -> fconnect f y x.
-  by move => x y sx xy; apply/idP/idP; apply:Sf.
-case/connectP=> p f_p -> {y sy}; elim: p x sx f_p => //= y p IHp x.
-move => sx /andP [/eqP fxy].
-have ys : y \in S by rewrite -fxy stable.
-move/IHp => /(_ ys)/connect_trans; apply.
-by rewrite -fxy -{2}(finv_f_in sx) fconnect_finv.
+suff Sf : {in S &, forall x y, fconnect f x y -> fconnect f y x}.
+  by move=> *; apply/idP/idP=> /Sf->.
+move=> x _ xS _ /connectP [p f_p ->]; elim: p => //= y p IHp in x xS f_p *.
+move: f_p; rewrite -{2}(finv_f_in xS) => /andP[/eqP <- /(IHp _ (f_in xS))].
+by move=> /connect_trans -> //; apply: fconnect_finv.
 Qed.
 
 Lemma iter_order_in : {in S, forall x, iter (order x) f x = x}.
-Proof.
-by move => x xs; rewrite -orderSpred iterS; apply (f_finv_in xs).
-Qed.
+Proof. by move=> x xS; rewrite -orderSpred iterS; apply: f_finv_in. Qed.
 
 Lemma iter_finv_in n :
   {in S, forall x, n <= order x -> iter n finv x = iter (order x - n) f x}.
 Proof.
-move => x xs.
-rewrite -{2}[x]iter_order_in => // /subnKC {1}<-; move: (_ - n) => m.
-rewrite iter_add; elim: n => // n {2}<-; rewrite iterSr /= finv_f_in //.
-by rewrite -iter_add stable_in_iter.
+move=> x xS; rewrite -{2}[x]iter_order_in => // /subnKC {1}<-; move: (_ - n).
+move=> m; rewrite iter_add; elim: n => // n {2}<-.
+by rewrite iterSr /= finv_f_in // -iter_add iter_in.
 Qed.
 
 Lemma cycle_orbit_in : {in S, forall x, (fcycle f) (orbit x)}.
 Proof.
-move => x sx.
-rewrite /orbit -orderSpred (cycle_path x) /= last_traject -/(finv x).
-by rewrite fpath_traject f_finv_in ?andbT.
+move=> x xS; rewrite /orbit -orderSpred (cycle_path x) /= last_traject.
+by rewrite -/(finv x) fpath_traject f_finv_in ?eqxx.
 Qed.
 
-(* There seems to be no simple equivalent of fpath_finv for subsets *)
-
-Lemma fpath_finv_f_in p :
-   {in S, forall x, fpath finv x p -> fpath f (last x p) (rev (belast x p))}.
+Lemma fpath_finv_in p x : (x \in S) && (fpath finv x p) =
+                          (last x p \in S) && (fpath f (last x p) (rev (belast x p))).
 Proof.
-elim: p => //= y p IHp x xs /andP [/eqP vy py]; rewrite rev_cons rcons_path.
-have ys : y \in S by rewrite -vy; apply: stable_in_iter.
-by rewrite (IHp _ ys py); case: p {IHp py} => //= [ | a l];
-   rewrite ?rev_cons ?path_rcons ?last_rcons /= -vy f_finv_in.
+elim: p x => //= y p IHp x; rewrite rev_cons rcons_path.
+transitivity [&& y \in S, f y == x & fpath finv y p].
+  apply/and3P/and3P => -[xS /eqP<- fxp]; split;
+  by rewrite ?f_finv_in ?finv_f_in ?finv_in ?f_in.
+rewrite andbCA {}IHp !andbA [RHS]andbC -andbA; congr [&& _, _ & _].
+by case: p => //= z p; rewrite rev_cons last_rcons.
 Qed.
 
-Lemma fpath_f_finv_in p :
-  {in S, forall y x, y = last x p -> fpath f (last x p) (rev (belast x p))
-    -> fpath finv x p}.
-Proof.
-have inS : forall p, {in S, forall y x, y = last x p ->
-          fpath f (last x p) (rev (belast x p)) -> {subset (x::p) <= S}}.
-move => {p}.
-  elim => //= [y ys x q _ | a p IHp y ys x q].
-    by move => c; rewrite -q inE => /eqP ->.
-  rewrite rev_cons rcons_path => /andP [pa vx].
-  have := (IHp y ys _ q pa) => sap.
-  move => c; rewrite inE => /orP[/eqP -> {c}| ]; last by apply: sap.
-  rewrite -(eqP vx).
-  set v := last _ _; have -> : v = a.
-    rewrite /v; case: p {IHp q pa vx sap v} => [ | b l']//=.
-    by rewrite rev_cons last_rcons.
-  by apply/stable/sap; rewrite inE eqxx.
-elim: p => //= a p IHp y ys x q; rewrite rev_cons rcons_path /=.
-move  => /andP [pa /eqP vx].
-rewrite (IHp y ys a q pa) andbT.
-have la : last (last a p) (rev (belast a p)) = a.
-  by case: p {IHp q pa vx} => /= [ | b l']; rewrite ?rev_cons ?last_rcons.
-move : vx; rewrite la => <-.
-apply/eqP/finv_f_in.
-by apply: (inS p y ys a q pa); rewrite inE eqxx.
-Qed.
+Lemma fpath_finv_f_in p : {in S, forall x,
+  fpath finv x p -> fpath f (last x p) (rev (belast x p))}.
+Proof. by move=> x xS /(conj xS)/andP; rewrite fpath_finv_in => /andP[]. Qed.
+
+Lemma fpath_f_finv_in p x : last x p \in S ->
+  fpath f (last x p) (rev (belast x p)) -> fpath finv x p.
+Proof. by move=> lS /(conj lS)/andP; rewrite -fpath_finv_in => /andP[]. Qed.
 
-End subset_orbit.
+End orbit_in.
 
 Hypothesis injf : injective f.
 
-Lemma f_finv : cancel finv f.
-Proof. by apply: in1T; apply: f_finv_in => //; apply: in2W. Qed.
+Lemma f_finv : cancel finv f. Proof. exact: (in1T (f_finv_in _ (in2W _))). Qed.
 
-Lemma finv_f : cancel f finv.
-Proof. by apply: in1T; apply: finv_f_in => //; apply: in2W. Qed.
+Lemma finv_f : cancel f finv. Proof. exact: (in1T (finv_f_in _ (in2W _))). Qed.
 
 Lemma fin_inj_bij : bijective f.
-Proof. by exists finv; [apply finv_f | apply f_finv]. Qed.
+Proof. by exists finv; [apply: finv_f|apply: f_finv]. Qed.
 
 Lemma finv_bij : bijective finv.
-Proof. by exists f; [apply f_finv | apply finv_f]. Qed.
+Proof. by exists f; [apply: f_finv|apply: finv_f]. Qed.
 
-Lemma finv_inj : injective finv.
-Proof. exact: (can_inj f_finv). Qed.
+Lemma finv_inj : injective finv. Proof. exact: (can_inj f_finv). Qed.
 
 Lemma fconnect_sym x y : fconnect f x y = fconnect f y x.
-Proof.
-by move: x y; apply: in2T; apply: fconnect_sym_in => //; apply: in2W.
-Qed.
+Proof. exact: (in2T (fconnect_sym_in _ (in2W _))). Qed.
 
 Let symf := fconnect_sym.
 
 Lemma iter_order x : iter (order x) f x = x.
-Proof. by move: x; apply: in1T; apply: iter_order_in=> //; apply: in2W. Qed.
+Proof. exact: (in1T (iter_order_in _ (in2W _))). Qed.
 
 Lemma iter_finv n x : n <= order x -> iter n finv x = iter (order x - n) f x.
-Proof.
-by move: x; apply: in1T; apply: iter_finv_in => //; apply: in2W.
-Qed.
+Proof. exact: (in1T (@iter_finv_in _ _ (in2W _) _)). Qed.
 
 Lemma cycle_orbit x : fcycle f (orbit x).
-Proof. by move: x; apply: in1T; apply: cycle_orbit_in => //; apply: in2W. Qed.
+Proof. exact: (in1T (cycle_orbit_in _ (in2W _))). Qed.
 
 Lemma fpath_finv x p : fpath finv x p = fpath f (last x p) (rev (belast x p)).
-Proof.
-apply/idP/idP.
-  by move: x; apply: in1T; apply: fpath_finv_f_in => //; apply: in2W.
-move: (erefl (last x p)); move: (LHS) => y; move: y x.
-by apply: in1T; apply: fpath_f_finv_in => //; apply: in2W.
-Qed.
+Proof. exact: (@fpath_finv_in T _ (in2W _)). Qed.
 
 Lemma same_fconnect_finv : fconnect finv =2 fconnect f.
 Proof.
@@ -821,4 +774,3 @@ Implicit Arguments intro_adjunction [T T' h e e' a].
 Implicit Arguments adjunction_n_comp [T T' e e' a].
 
 Unset Implicit Arguments.
-