diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 3 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finfun.v | 20 |
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). |