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 --- mathcomp/ssreflect/tuple.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'mathcomp/ssreflect') 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