From 2a0a00630785c616899abaa6fccb95ee76f751bf Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 26 Jun 2019 00:27:04 +0200
Subject: feat(finfun.v): Add tuple_of_finfun, finfun_of_tuple & cancel lemmas

---
 mathcomp/ssreflect/finfun.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'mathcomp')

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).
-- 
cgit v1.2.3