From b26bff45cb80da59a5975318a9d2a7e5425a5713 Mon Sep 17 00:00:00 2001 From: jouvelot Date: Sun, 14 Mar 2021 21:42:34 +0100 Subject: Adding sorting on tuples. (#720) * Adding sorting on tuples. Co-authored-by: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 2 ++ mathcomp/ssreflect/tuple.v | 6 +++++- 2 files changed, 7 insertions(+), 1 deletion(-) 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. -- cgit v1.2.3