feat(finfun.v): Add tuple_of_finfun, finfun_of_tuple & cancel lemmas

2 files changed, 23 insertions, 0 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 26a214d..3777a83 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -13,6 +13,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Added fixpoint and cofixpoint constructions to `finset`: `fixset`,
   `cofixset` and `fix_order`, with a few theorems about them
 
+- Added functions `tuple_of_finfun`, `finfun_of_tuple`, and their
+  "cancellation" lemmas.
+
 ### Changed
 
 - `eqVneq` lemma is changed from `{x = y} + {x != y}` to
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index 075ebfa..749f5e2 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -270,6 +270,26 @@ Canonical dfinfun_finType rT :=
 
 End InheritedStructures.
 
+Section FinFunTuple.
+
+Context {T : Type} {n : nat}.
+
+Definition tuple_of_finfun (f : T ^ n) : n.-tuple T := [tuple f i | i < n].
+
+Definition finfun_of_tuple (t : n.-tuple T) : (T ^ n) := [ffun i => tnth t i].
+
+Lemma finfun_of_tupleK : cancel finfun_of_tuple tuple_of_finfun.
+Proof.
+by move=> t; apply: eq_from_tnth => i; rewrite tnth_map ffunE tnth_ord_tuple.
+Qed.
+
+Lemma tuple_of_finfunK : cancel tuple_of_finfun finfun_of_tuple.
+Proof.
+by move=> f; apply/ffunP => i; rewrite ffunE tnth_map tnth_ord_tuple.
+Qed.
+
+End FinFunTuple.
+
 Section FunPlainTheory.
 
 Variables (aT : finType) (rT : Type).