Small scale tool for proving circular implications, and using any pai…

…r of equivalence

mathcomp/ssreflect/seq.v

@@ -2789,3 +2789,42 @@ by apply: inj_f => //; apply/allpairsP; [exists (x, y1) | exists (x, y2)].
 Qed.
 
 End EqAllPairs.
+
+Section AllIff.
+
+Inductive all_iff_and (P Q : Prop) := AllIffConj of P & Q.
+Definition all_iff P0 (Ps : seq Prop) : Prop :=
+  (fix aux (P : Prop) (Qs : seq Prop) : Prop :=
+      if Qs is Q :: Qs then all_iff_and (P -> Q) (aux Q Qs)
+      else P -> P0 : Prop) P0 Ps.
+
+Notation "[ '<->' x0 ; x1 ; .. ; xn ]" := (all_iff x0 (x1 :: .. [:: xn] ..))
+  (at level 0, format "[ '<->' '['  x0 ;  '/' x1 ;  '/'  .. ;  '/'  xn ']' ]")
+  : form_scope.
+
+Lemma all_iffLR P0 Ps : all_iff P0 Ps ->
+   forall m n, nth P0 (P0 :: Ps) m -> nth P0 (P0 :: Ps) n.
+Proof.
+move=> Ps_iff; have ltn_imply : {homo nth P0 Ps : m n / m < n >-> (m -> n)}.
+  apply: homo_ltn => [|i]; first tauto.
+  elim: Ps i P0 Ps_iff => [|P [|/=Q Ps] IHPs] [|i]//= P0 [P0P Ps_iff]//=;
+     do ?by [rewrite nth_nil|case: Ps_iff].
+  by case: Ps_iff => [PQ Ps_iff]; apply: IHPs; split => // /P0P.
+have {ltn_imply}leq_imply : {homo nth P0 Ps : m n / m <= n >-> (m -> n)}.
+  by move=> m n; rewrite leq_eqVlt => /predU1P[->//|/ltn_imply].
+move=> [:P0ton Pnto0] [|m] [|n]//=.
+- abstract: P0ton n.
+  suff P0to0 : P0 -> nth P0 Ps 0 by move=> /P0to0; apply: leq_imply.
+  by case: Ps Ps_iff {leq_imply} => // P Ps [].
+- abstract: Pnto0 m; move=> /(leq_imply m (maxn (size Ps) m)).
+  by rewrite leq_max leqnn orbT nth_default ?leq_max ?leqnn //; apply.
+exact: (P0ton _ \o Pnto0 _).
+Qed.
+
+Lemma all_iffP P0 Ps : all_iff P0 Ps ->
+   forall m n, nth P0 (P0 :: Ps) m <-> nth P0 (P0 :: Ps) n.
+Proof. by move=> /all_iffLR iffPs m n; split => /iffPs. Qed.
+
+End AllIff.
+Arguments all_iffLR {P0 Ps}.
+Coercion all_iffP : all_iff >-> Funclass.