From f0e9ca0a160fd11716cc759cab8c6cbcbf20a32d Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Mon, 17 Jun 2019 15:00:07 +0200
Subject: Fixes in naming, mixins, doc and canonical ordering

- comparer -> compare (in order.v)
- eq constructor of compare goes last
- "x < y" is matched before "x > y"
- "x <= y" is matched before "x >= y"
- adding prod and lexi ordering on tuple
- adding missing CS
- edit CHANGELOG
---
 mathcomp/ssreflect/tuple.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'mathcomp/ssreflect/tuple.v')

diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index dd73664..10d54f0 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -213,6 +213,9 @@ Definition thead (u : n.+1.-tuple T) := tnth u ord0.
 Lemma tnth0 x t : tnth [tuple of x :: t] ord0 = x.
 Proof. by []. Qed.
 
+Lemma tnthS x t i : tnth [tuple of x :: t] (lift ord0 i) = tnth t i.
+Proof. by rewrite (tnth_nth (tnth_default t i)). Qed.
+
 Lemma theadE x t : thead [tuple of x :: t] = x.
 Proof. by []. Qed.
 
@@ -231,6 +234,11 @@ Qed.
 Lemma tnth_map f t i : tnth [tuple of map f t] i = f (tnth t i) :> rT.
 Proof. by apply: nth_map; rewrite size_tuple. Qed.
 
+Lemma tnth_nseq x i : tnth [tuple of nseq n x] i = x.
+Proof.
+by rewrite !(tnth_nth (tnth_default (nseq_tuple x) i)) nth_nseq ltn_ord.
+Qed.
+
 End SeqTuple.
 
 Lemma tnth_behead n T (t : n.+1.-tuple T) i :
@@ -277,6 +285,10 @@ Canonical tuple_eqType := Eval hnf in EqType (n.-tuple T) tuple_eqMixin.
 
 Canonical tuple_predType := PredType (pred_of_seq : n.-tuple T -> pred T).
 
+Lemma eqEtuple (t1 t2 : n.-tuple T) :
+  (t1 == t2) = [forall i, tnth t1 i == tnth t2 i].
+Proof. by apply/eqP/'forall_eqP => [->|/eq_from_tnth]. Qed.
+
 Lemma memtE (t : n.-tuple T) : mem t = mem (tval t).
 Proof. by []. Qed.
 
-- 
cgit v1.2.3