diff options
| author | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
| commit | 6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch) | |
| tree | 1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/mathcomp.ssreflect.tuple.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.tuple.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.tuple.html | 477 |
1 files changed, 0 insertions, 477 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.tuple.html b/docs/htmldoc/mathcomp.ssreflect.tuple.html deleted file mode 100644 index 4a62053..0000000 --- a/docs/htmldoc/mathcomp.ssreflect.tuple.html +++ /dev/null @@ -1,477 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.ssreflect.tuple</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.ssreflect.tuple</h1> - -<div class="code"> -<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><br/> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -</div> - -<div class="doc"> - Tuples, i.e., sequences with a fixed (known) length. We define: - n.-tuple T == the type of n-tuples of elements of type T. - [tuple of s] == the tuple whose underlying sequence (value) is s. - The size of s must be known: specifically, Coq must - be able to infer a Canonical tuple projecting on s. - in_tuple s == the (size s)-tuple with value s. - [tuple] == the empty tuple. - [tuple x1; ..; xn] == the explicit n.-tuple <x1; ..; xn>. - [tuple E | i < n] == the n.-tuple with general term E (i : 'I_n is bound - in E). - tcast Emn t == the m-tuple t cast as an n-tuple using Emn : m = n. - As n.-tuple T coerces to seq t, all seq operations (size, nth, ...) can be - applied to t : n.-tuple T; we provide a few specialized instances when - avoids the need for a default value. - tsize t == the size of t (the n in n.-tuple T) - tnth t i == the i'th component of t, where i : 'I_n. - [tnth t i] == the i'th component of t, where i : nat and i < n - is convertible to true. - thead t == the first element of t, when n is m.+1 for some m. - Most seq constructors (cons, behead, cat, rcons, belast, take, drop, rot, - map, ...) can be used to build tuples via the [tuple of s] construct. - Tuples are actually a subType of seq, and inherit all combinatorial - structures, including the finType structure. - Some useful lemmas and definitions: - tuple0 : [tuple] is the only 0.-tuple - tupleP : elimination view for n.+1.-tuple - ord_tuple n : the n.-tuple of all i : 'I_n -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Def"><span class="id" title="section">Def</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="Def.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="Def.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>).<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="tuple_of"><span class="id" title="record">tuple_of</span></a> : <span class="id" title="keyword">Type</span> := <a name="Tuple"><span class="id" title="constructor">Tuple</span></a> {<a name="tval"><span class="id" title="projection">tval</span></a> :> <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#Def.T"><span class="id" title="variable">T</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tval"><span class="id" title="method">tval</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#Def.n"><span class="id" title="variable">n</span></a>}.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tval"><span class="id" title="projection">tval</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_of"><span class="id" title="record">tuple_of</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tsize"><span class="id" title="definition">tsize</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_of"><span class="id" title="record">tuple_of</span></a> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Def.n"><span class="id" title="variable">n</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="size_tuple"><span class="id" title="lemma">size_tuple</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#Def.n"><span class="id" title="variable">n</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tnth_default"><span class="id" title="lemma">tnth_default</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#Def.T"><span class="id" title="variable">T</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tnth"><span class="id" title="definition">tnth</span></a> <span class="id" title="var">t</span> <span class="id" title="var">i</span> := <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth_default"><span class="id" title="lemma">tnth_default</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tnth_nth"><span class="id" title="lemma">tnth_nth</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="map_tnth_enum"><span class="id" title="lemma">map_tnth_enum</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum"><span class="id" title="abbreviation">enum</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eq_from_tnth"><span class="id" title="lemma">eq_from_tnth</span></a> <span class="id" title="var">t1</span> <span class="id" title="var">t2</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t1"><span class="id" title="variable">t1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t2"><span class="id" title="variable">t2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t1"><span class="id" title="variable">t1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t2"><span class="id" title="variable">t2</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tuple"><span class="id" title="definition">tuple</span></a> <span class="id" title="var">t</span> <span class="id" title="var">mkT</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_of"><span class="id" title="record">tuple_of</span></a> :=<br/> - <a class="idref" href="mathcomp.ssreflect.tuple.html#mkT"><span class="id" title="variable">mkT</span></a> (<span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> <span class="id" title="var">_</span> <span class="id" title="var">tP</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#Def.n"><span class="id" title="variable">n</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">tP</span>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tupleE"><span class="id" title="lemma">tupleE</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple"><span class="id" title="definition">tuple</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">sP</span> ⇒ @<a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#sP"><span class="id" title="variable">sP</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#Def"><span class="id" title="section">Def</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">"</span></a>n .-tuple" := (<a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_of"><span class="id" title="record">tuple_of</span></a> <span class="id" title="var">n</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "n .-tuple") : <span class="id" title="var">type_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="e6755b713866d9cfa46c6af439dadcc7"><span class="id" title="notation">"</span></a>{ 'tuple' n 'of' T }" := (<span class="id" title="var">n</span><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <span class="id" title="var">T</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#predArgType"><span class="id" title="definition">predArgType</span></a>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">"</span></a>[ 'tuple' 'of' s ]" := (<a class="idref" href="mathcomp.ssreflect.tuple.html#tuple"><span class="id" title="definition">tuple</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">sP</span> ⇒ @<a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">s</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#sP"><span class="id" title="variable">sP</span></a>))<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'tuple' 'of' s ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="1e7a8c2b96d06dcd9add7e63bc21c575"><span class="id" title="notation">"</span></a>[ 'tnth' t i ]" := (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <span class="id" title="var">t</span> (@<a class="idref" href="mathcomp.ssreflect.fintype.html#Ordinal"><span class="id" title="constructor">Ordinal</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tsize"><span class="id" title="definition">tsize</span></a> <span class="id" title="var">t</span>) <span class="id" title="var">i</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#erefl"><span class="id" title="abbreviation">erefl</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>)))<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">t</span>, <span class="id" title="var">i</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">format</span> "[ 'tnth' t i ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">nil_tuple</span> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#isT"><span class="id" title="definition">isT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> @<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::]</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">cons_tuple</span> <span class="id" title="var">n</span> <span class="id" title="var">T</span> <span class="id" title="var">x</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>) :=<br/> - <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#valP"><span class="id" title="lemma">valP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="44d42eed9f717544480811f482f3c650"><span class="id" title="notation">"</span></a>[ 'tuple' x1 ; .. ; xn ]" := <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <span class="id" title="var">x1</span> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> .. <a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">[::</span></a> <span class="id" title="var">xn</span><a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">]</span></a> ..<a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a><br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'tuple' '[' x1 ; '/' .. ; '/' xn ']' ]")<br/> - : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="40a2c8face21f18a7058a916d5f839b8"><span class="id" title="notation">"</span></a>[ 'tuple' ]" := <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a><br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'tuple' ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="CastTuple"><span class="id" title="section">CastTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="CastTuple.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="in_tuple"><span class="id" title="definition">in_tuple</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#CastTuple.T"><span class="id" title="variable">T</span></a>) := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#eqxx"><span class="id" title="abbreviation">eqxx</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#s"><span class="id" title="variable">s</span></a>)).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tcast"><span class="id" title="definition">tcast</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> (<span class="id" title="var">eq_mn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a>) <span class="id" title="var">t</span> :=<br/> - <span class="id" title="keyword">let</span>: <span class="id" title="var">erefl</span> <span class="id" title="tactic">in</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#CastTuple.T"><span class="id" title="variable">T</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tcastE"><span class="id" title="lemma">tcastE</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> (<span class="id" title="var">eq_mn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a>) <span class="id" title="var">t</span> <span class="id" title="var">i</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#cast_ord"><span class="id" title="definition">cast_ord</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#esym"><span class="id" title="definition">esym</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tcast_id"><span class="id" title="lemma">tcast_id</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">eq_nn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a>) <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_nn"><span class="id" title="variable">eq_nn</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tcastK"><span class="id" title="lemma">tcastK</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> (<span class="id" title="var">eq_mn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a>) (<a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#esym"><span class="id" title="definition">esym</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a>)).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tcastKV"><span class="id" title="lemma">tcastKV</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> (<span class="id" title="var">eq_mn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#esym"><span class="id" title="definition">esym</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a>)) (<a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tcast_trans"><span class="id" title="lemma">tcast_trans</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> <span class="id" title="var">p</span> (<span class="id" title="var">eq_mn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a>) (<span class="id" title="var">eq_np</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#p"><span class="id" title="variable">p</span></a>) <span class="id" title="var">t</span>:<br/> - <a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#etrans"><span class="id" title="definition">etrans</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_np"><span class="id" title="variable">eq_np</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_np"><span class="id" title="variable">eq_np</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tvalK"><span class="id" title="lemma">tvalK</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#CastTuple.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.tuple.html#in_tuple"><span class="id" title="definition">in_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#esym"><span class="id" title="definition">esym</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#size_tuple"><span class="id" title="lemma">size_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>)) <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="in_tupleE"><span class="id" title="lemma">in_tupleE</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#in_tuple"><span class="id" title="definition">in_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#CastTuple.T"><span class="id" title="variable">T</span></a>. <br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#CastTuple"><span class="id" title="section">CastTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="SeqTuple"><span class="id" title="section">SeqTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="SeqTuple.n"><span class="id" title="variable">n</span></a> <a name="SeqTuple.m"><span class="id" title="variable">m</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="SeqTuple.T"><span class="id" title="variable">T</span></a> <a name="SeqTuple.U"><span class="id" title="variable">U</span></a> <a name="SeqTuple.rT"><span class="id" title="variable">rT</span></a> : <span class="id" title="keyword">Type</span>).<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.T"><span class="id" title="variable">T</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="rcons_tupleP"><span class="id" title="lemma">rcons_tupleP</span></a> <span class="id" title="var">t</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rcons"><span class="id" title="definition">rcons</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">rcons_tuple</span> <span class="id" title="var">t</span> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#rcons_tupleP"><span class="id" title="lemma">rcons_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="nseq_tupleP"><span class="id" title="lemma">nseq_tupleP</span></a> <span class="id" title="var">x</span> : @<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.T"><span class="id" title="variable">T</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#nseq"><span class="id" title="definition">nseq</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">nseq_tuple</span> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#nseq_tupleP"><span class="id" title="lemma">nseq_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="iota_tupleP"><span class="id" title="lemma">iota_tupleP</span></a> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#iota"><span class="id" title="definition">iota</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">iota_tuple</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#iota_tupleP"><span class="id" title="lemma">iota_tupleP</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="behead_tupleP"><span class="id" title="lemma">behead_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#behead"><span class="id" title="definition">behead</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">behead_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#behead_tupleP"><span class="id" title="lemma">behead_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="belast_tupleP"><span class="id" title="lemma">belast_tupleP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#belast"><span class="id" title="definition">belast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">belast_tuple</span> <span class="id" title="var">x</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#belast_tupleP"><span class="id" title="lemma">belast_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="cat_tupleP"><span class="id" title="lemma">cat_tupleP</span></a> <span class="id" title="var">t</span> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#93e0a78b945d3f9f22195c004c67aa36"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">cat_tuple</span> <span class="id" title="var">t</span> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#cat_tupleP"><span class="id" title="lemma">cat_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="take_tupleP"><span class="id" title="lemma">take_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#take"><span class="id" title="definition">take</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#minn"><span class="id" title="definition">minn</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">take_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#take_tupleP"><span class="id" title="lemma">take_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="drop_tupleP"><span class="id" title="lemma">drop_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#drop"><span class="id" title="definition">drop</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7825ccc99f23b0d30c9d40c317ba7af0"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">drop_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#drop_tupleP"><span class="id" title="lemma">drop_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="rev_tupleP"><span class="id" title="lemma">rev_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">rev_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#rev_tupleP"><span class="id" title="lemma">rev_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="rot_tupleP"><span class="id" title="lemma">rot_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rot"><span class="id" title="definition">rot</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">rot_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#rot_tupleP"><span class="id" title="lemma">rot_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="rotr_tupleP"><span class="id" title="lemma">rotr_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rotr"><span class="id" title="definition">rotr</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">rotr_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#rotr_tupleP"><span class="id" title="lemma">rotr_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="map_tupleP"><span class="id" title="lemma">map_tupleP</span></a> <span class="id" title="var">f</span> <span class="id" title="var">t</span> : @<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">map_tuple</span> <span class="id" title="var">f</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#map_tupleP"><span class="id" title="lemma">map_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="scanl_tupleP"><span class="id" title="lemma">scanl_tupleP</span></a> <span class="id" title="var">f</span> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : @<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#scanl"><span class="id" title="definition">scanl</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">scanl_tuple</span> <span class="id" title="var">f</span> <span class="id" title="var">x</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#scanl_tupleP"><span class="id" title="lemma">scanl_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="pairmap_tupleP"><span class="id" title="lemma">pairmap_tupleP</span></a> <span class="id" title="var">f</span> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : @<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#pairmap"><span class="id" title="definition">pairmap</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">pairmap_tuple</span> <span class="id" title="var">f</span> <span class="id" title="var">x</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#pairmap_tupleP"><span class="id" title="lemma">pairmap_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="zip_tupleP"><span class="id" title="lemma">zip_tupleP</span></a> <span class="id" title="var">t</span> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.U"><span class="id" title="variable">U</span></a>) : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#zip"><span class="id" title="definition">zip</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">zip_tuple</span> <span class="id" title="var">t</span> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#zip_tupleP"><span class="id" title="lemma">zip_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="allpairs_tupleP"><span class="id" title="lemma">allpairs_tupleP</span></a> <span class="id" title="var">f</span> <span class="id" title="var">t</span> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.U"><span class="id" title="variable">U</span></a>) : @<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#allpairs"><span class="id" title="definition">allpairs</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">allpairs_tuple</span> <span class="id" title="var">f</span> <span class="id" title="var">t</span> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#allpairs_tupleP"><span class="id" title="lemma">allpairs_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="thead"><span class="id" title="definition">thead</span></a> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.T"><span class="id" title="variable">T</span></a>) := <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#ord0"><span class="id" title="definition">ord0</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tnth0"><span class="id" title="lemma">tnth0</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#ord0"><span class="id" title="definition">ord0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="theadE"><span class="id" title="lemma">theadE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#thead"><span class="id" title="definition">thead</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tuple0"><span class="id" title="lemma">tuple0</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#all_equal_to"><span class="id" title="definition">all_equal_to</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#40a2c8face21f18a7058a916d5f839b8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#40a2c8face21f18a7058a916d5f839b8"><span class="id" title="notation">tuple</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#40a2c8face21f18a7058a916d5f839b8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> 0<a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Variant</span> <a name="tuple1_spec"><span class="id" title="inductive">tuple1_spec</span></a> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span> :=<br/> - <a name="Tuple1spec"><span class="id" title="constructor">Tuple1spec</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple1_spec"><span class="id" title="inductive">tuple1_spec</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tupleP"><span class="id" title="lemma">tupleP</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple1_spec"><span class="id" title="inductive">tuple1_spec</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tnth_map"><span class="id" title="lemma">tnth_map</span></a> <span class="id" title="var">f</span> <span class="id" title="var">t</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.rT"><span class="id" title="variable">rT</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple"><span class="id" title="section">SeqTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tnth_behead"><span class="id" title="lemma">tnth_behead</span></a> <span class="id" title="var">n</span> <span class="id" title="var">T</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>) <span class="id" title="var">i</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#behead"><span class="id" title="definition">behead</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#inord"><span class="id" title="definition">inord</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tuple_eta"><span class="id" title="lemma">tuple_eta</span></a> <span class="id" title="var">n</span> <span class="id" title="var">T</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#thead"><span class="id" title="definition">thead</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#behead"><span class="id" title="definition">behead</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="TupleQuantifiers"><span class="id" title="section">TupleQuantifiers</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="TupleQuantifiers.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="TupleQuantifiers.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>).<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">a</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#TupleQuantifiers.T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#TupleQuantifiers.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#TupleQuantifiers.T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="forallb_tnth"><span class="id" title="lemma">forallb_tnth</span></a> <span class="id" title="var">a</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#ce8c9a990e3e773a56ef37417d3761c6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ce8c9a990e3e773a56ef37417d3761c6"><span class="id" title="notation">∀</span></a> <span class="id" title="var">i</span><a class="idref" href="mathcomp.ssreflect.fintype.html#f3be25edeb0349b0a76405eded9d0b98"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>)<a class="idref" href="mathcomp.ssreflect.fintype.html#ce8c9a990e3e773a56ef37417d3761c6"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="existsb_tnth"><span class="id" title="lemma">existsb_tnth</span></a> <span class="id" title="var">a</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">∃</span></a> <span class="id" title="var">i</span><a class="idref" href="mathcomp.ssreflect.fintype.html#f3be25edeb0349b0a76405eded9d0b98"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>)<a class="idref" href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#has"><span class="id" title="definition">has</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="all_tnthP"><span class="id" title="lemma">all_tnthP</span></a> <span class="id" title="var">a</span> <span class="id" title="var">t</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">i</span>, <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>)) (<a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="has_tnthP"><span class="id" title="lemma">has_tnthP</span></a> <span class="id" title="var">a</span> <span class="id" title="var">t</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">i</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>)) (<a class="idref" href="mathcomp.ssreflect.seq.html#has"><span class="id" title="definition">has</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#TupleQuantifiers"><span class="id" title="section">TupleQuantifiers</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="EqTuple"><span class="id" title="section">EqTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="EqTuple.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="EqTuple.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tuple_eqMixin"><span class="id" title="definition">tuple_eqMixin</span></a> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_eqMixin"><span class="id" title="definition">tuple_eqMixin</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_predType</span> := <a class="idref" href="mathcomp.ssreflect.ssrbool.html#PredType"><span class="id" title="definition">PredType</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#pred_of_seq"><span class="id" title="definition">pred_of_seq</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="memtE"><span class="id" title="lemma">memtE</span></a> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tval"><span class="id" title="projection">tval</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="mem_tnth"><span class="id" title="lemma">mem_tnth</span></a> <span class="id" title="var">i</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="memt_nth"><span class="id" title="lemma">memt_nth</span></a> <span class="id" title="var">x0</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x0"><span class="id" title="variable">x0</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tnthP"><span class="id" title="lemma">tnthP</span></a> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">i</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>) (<a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="seq_tnthP"><span class="id" title="lemma">seq_tnthP</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#in_tuple"><span class="id" title="definition">in_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#s"><span class="id" title="variable">s</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple"><span class="id" title="section">EqTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tuple_choiceMixin"><span class="id" title="definition">tuple_choiceMixin</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) :=<br/> - <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation"><:]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_choiceType</span> <span class="id" title="var">n</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_choiceMixin"><span class="id" title="definition">tuple_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tuple_countMixin"><span class="id" title="definition">tuple_countMixin</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/> - <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation"><:]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_countType</span> <span class="id" title="var">n</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_countMixin"><span class="id" title="definition">tuple_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_subCountType</span> <span class="id" title="var">n</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Module</span> <span class="id" title="keyword">Type</span> <a name="FinTupleSig"><span class="id" title="module">FinTupleSig</span></a>.<br/> -<span class="id" title="keyword">Section</span> <a name="FinTupleSig.FinTupleSig"><span class="id" title="section">FinTupleSig</span></a>.<br/> -<span class="id" title="keyword">Variables</span> (<a name="FinTupleSig.FinTupleSig.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="FinTupleSig.FinTupleSig.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>).<br/> -<span class="id" title="keyword">Parameter</span> <a name="FinTupleSig.enum"><span class="id" title="axiom">enum</span></a> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.FinTupleSig.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.FinTupleSig.T"><span class="id" title="variable">T</span></a>).<br/> -<span class="id" title="keyword">Axiom</span> <a name="FinTupleSig.enumP"><span class="id" title="axiom">enumP</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.axiom"><span class="id" title="definition">Finite.axiom</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.enum"><span class="id" title="axiom">enum</span></a>.<br/> -<span class="id" title="keyword">Axiom</span> <a name="FinTupleSig.size_enum"><span class="id" title="axiom">size_enum</span></a> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.enum"><span class="id" title="axiom">enum</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.FinTupleSig.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.FinTupleSig.n"><span class="id" title="variable">n</span></a>.<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.FinTupleSig"><span class="id" title="section">FinTupleSig</span></a>.<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig"><span class="id" title="module">FinTupleSig</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Module</span> <a name="FinTuple"><span class="id" title="module">FinTuple</span></a> : <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig"><span class="id" title="module">FinTupleSig</span></a>.<br/> -<span class="id" title="keyword">Section</span> <a name="FinTuple.FinTuple"><span class="id" title="section">FinTuple</span></a>.<br/> -<span class="id" title="keyword">Variables</span> (<a name="FinTuple.FinTuple.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="FinTuple.FinTuple.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="FinTuple.enum"><span class="id" title="definition">enum</span></a> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.FinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.FinTuple.T"><span class="id" title="variable">T</span></a>) :=<br/> - <span class="id" title="keyword">let</span> <span class="id" title="var">extend</span> <span class="id" title="var">e</span> := <a class="idref" href="mathcomp.ssreflect.seq.html#flatten"><span class="id" title="definition">flatten</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#codom"><span class="id" title="definition">codom</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#e"><span class="id" title="variable">e</span></a>)) <span class="id" title="tactic">in</span><br/> - <a class="idref" href="mathcomp.ssreflect.seq.html#pmap"><span class="id" title="definition">pmap</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#insub"><span class="id" title="definition">insub</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.FinTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#extend"><span class="id" title="variable">extend</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::]</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">]</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="FinTuple.enumP"><span class="id" title="lemma">enumP</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.axiom"><span class="id" title="definition">Finite.axiom</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.enum"><span class="id" title="definition">enum</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="FinTuple.size_enum"><span class="id" title="lemma">size_enum</span></a> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.enum"><span class="id" title="definition">enum</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.FinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.FinTuple.n"><span class="id" title="variable">n</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.FinTuple"><span class="id" title="section">FinTuple</span></a>.<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple"><span class="id" title="module">FinTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="UseFinTuple"><span class="id" title="section">UseFinTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="UseFinTuple.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="UseFinTuple.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>).<br/> - -<br/> -</div> - -<div class="doc"> - tuple_finMixin could, in principle, be made Canonical to allow for folding - Finite.enum of a finite tuple type (see comments around eqE in eqtype.v), - but in practice it will not work because the mixin_enum projector - has been burried under an opaque alias, to avoid some performance issues - during type inference. -</div> -<div class="code"> -<span class="id" title="keyword">Definition</span> <a name="tuple_finMixin"><span class="id" title="definition">tuple_finMixin</span></a> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinMixin"><span class="id" title="abbreviation">FinMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.tuple.html#enumP"><span class="id" title="axiom">FinTuple.enumP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_finType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_finMixin"><span class="id" title="definition">tuple_finMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_subFinType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="card_tuple"><span class="id" title="lemma">card_tuple</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#fa3b33ae9d0a52de608b305a09f3b881"><span class="id" title="notation">{:</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#fa3b33ae9d0a52de608b305a09f3b881"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="enum_tupleP"><span class="id" title="lemma">enum_tupleP</span></a> (<span class="id" title="var">A</span> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum"><span class="id" title="abbreviation">enum</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#A"><span class="id" title="variable">A</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">enum_tuple</span> <span class="id" title="var">A</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#enum_tupleP"><span class="id" title="lemma">enum_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#A"><span class="id" title="variable">A</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="ord_tuple"><span class="id" title="definition">ord_tuple</span></a> : <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#introT"><span class="id" title="lemma">introT</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#eqP"><span class="id" title="lemma">eqP</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#size_enum_ord"><span class="id" title="lemma">size_enum_ord</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a>)).<br/> -<span class="id" title="keyword">Lemma</span> <a name="val_ord_tuple"><span class="id" title="lemma">val_ord_tuple</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#ord_tuple"><span class="id" title="definition">ord_tuple</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#enum"><span class="id" title="abbreviation">enum</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a>. <br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tuple_map_ord"><span class="id" title="lemma">tuple_map_ord</span></a> <span class="id" title="var">U</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#U"><span class="id" title="variable">U</span></a>) : <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#ord_tuple"><span class="id" title="definition">ord_tuple</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tnth_ord_tuple"><span class="id" title="lemma">tnth_ord_tuple</span></a> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#ord_tuple"><span class="id" title="definition">ord_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="UseFinTuple.ImageTuple"><span class="id" title="section">ImageTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="UseFinTuple.ImageTuple.T'"><span class="id" title="variable">T'</span></a> : <span class="id" title="keyword">Type</span>) (<a name="UseFinTuple.ImageTuple.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T'"><span class="id" title="variable">T'</span></a>) (<a name="UseFinTuple.ImageTuple.A"><span class="id" title="variable">A</span></a> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">image_tuple</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.T'"><span class="id" title="variable">T'</span></a> := <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#image"><span class="id" title="abbreviation">image</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">codom_tuple</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.T'"><span class="id" title="variable">T'</span></a> := <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#codom"><span class="id" title="definition">codom</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.f"><span class="id" title="variable">f</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple"><span class="id" title="section">ImageTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="UseFinTuple.MkTuple"><span class="id" title="section">MkTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="UseFinTuple.MkTuple.T'"><span class="id" title="variable">T'</span></a> : <span class="id" title="keyword">Type</span>) (<a name="UseFinTuple.MkTuple.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T'"><span class="id" title="variable">T'</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="mktuple"><span class="id" title="definition">mktuple</span></a> := <a class="idref" href="mathcomp.ssreflect.tuple.html#map_tuple"><span class="id" title="definition">map_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.MkTuple.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#ord_tuple"><span class="id" title="definition">ord_tuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tnth_mktuple"><span class="id" title="lemma">tnth_mktuple</span></a> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#mktuple"><span class="id" title="definition">mktuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.MkTuple.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="nth_mktuple"><span class="id" title="lemma">nth_mktuple</span></a> <span class="id" title="var">x0</span> (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a>) : <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x0"><span class="id" title="variable">x0</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#mktuple"><span class="id" title="definition">mktuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.MkTuple.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.MkTuple"><span class="id" title="section">MkTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eq_mktuple"><span class="id" title="lemma">eq_mktuple</span></a> <span class="id" title="var">T'</span> (<span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T'"><span class="id" title="variable">T'</span></a>) :<br/> - <a class="idref" href="mathcomp.ssreflect.tuple.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f2"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#mktuple"><span class="id" title="definition">mktuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#mktuple"><span class="id" title="definition">mktuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f2"><span class="id" title="variable">f2</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple"><span class="id" title="section">UseFinTuple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="9d5b9af75768e306a1218aacdf8c3490"><span class="id" title="notation">"</span></a>[ 'tuple' F | i < n ]" := (<a class="idref" href="mathcomp.ssreflect.tuple.html#mktuple"><span class="id" title="definition">mktuple</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a> ⇒ <span class="id" title="var">F</span>))<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">i</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/> - <span class="id" title="var">format</span> "[ '[hv' 'tuple' F '/' | i < n ] ']'") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -</div> -</div> - -<div id="footer"> -<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> -</div> - -</div> - -</body> -</html>
\ No newline at end of file |