diff options
| author | jouvelot | 2021-03-14 21:42:34 +0100 |
|---|---|---|
| committer | GitHub | 2021-03-14 21:42:34 +0100 |
| commit | b26bff45cb80da59a5975318a9d2a7e5425a5713 (patch) | |
| tree | d14ff1ba5790957be7d2857c67832dc111040644 | |
| parent | 1ec9344814bb4d8d7fa59dffdbf4f5045ca1ba86 (diff) | |
Adding sorting on tuples. (#720)
* Adding sorting on tuples.
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 6 |
2 files changed, 7 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4ea1df2..8a7a0b4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -25,6 +25,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `path.v`, new lemmas: `sorted_pairwise(_in)`, `path_pairwise(_in)`, `cycle_all2rel(_in)`, `pairwise_sort`, and `sort_pairwise_stable`. +- in `tuple.v`, added Canonical tuple for sort. + - in `interval.v`, new lemmas: `ge_pinfty`, `le_ninfty`, `gt_pinfty`, `lt_ninfty`. - in `order.v` diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index f32793f..50a4d1e 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -1,7 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. -From mathcomp Require Import seq choice fintype. +From mathcomp Require Import seq choice fintype path. Set Implicit Arguments. Unset Strict Implicit. @@ -208,6 +208,10 @@ Lemma allpairs_tupleP f t (u : m.-tuple U) : @size rT (allpairs f t u) == n * m. Proof. by rewrite size_allpairs !size_tuple. Qed. Canonical allpairs_tuple f t u := Tuple (allpairs_tupleP f t u). +Lemma sort_tupleP r t : size (sort r t) == n. +Proof. by rewrite size_sort size_tuple. Qed. +Canonical sort_tuple r t := Tuple (sort_tupleP r t). + Definition thead (u : n.+1.-tuple T) := tnth u ord0. Lemma tnth0 x t : tnth [tuple of x :: t] ord0 = x. |