From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.ssreflect.tuple.html | 222 +++++++++++++++--------------
1 file changed, 117 insertions(+), 105 deletions(-)
(limited to 'docs/htmldoc/mathcomp.ssreflect.tuple.html')
diff --git a/docs/htmldoc/mathcomp.ssreflect.tuple.html b/docs/htmldoc/mathcomp.ssreflect.tuple.html
index 1dd43d4..4a62053 100644
--- a/docs/htmldoc/mathcomp.ssreflect.tuple.html
+++ b/docs/htmldoc/mathcomp.ssreflect.tuple.html
@@ -21,7 +21,6 @@
-
Require Import mathcomp.ssreflect.ssreflect.
Set Implicit Arguments.
@@ -64,13 +63,13 @@
Section Def.
-
Variables (
n :
nat) (
T :
Type).
+
Variables (
n :
nat) (
T :
Type).
-
Structure tuple_of :
Type :=
Tuple {
tval :>
seq T;
_ :
size tval == n}.
+
Structure tuple_of :
Type :=
Tuple {
tval :>
seq T;
_ :
size tval == n}.
-
Canonical tuple_subType :=
Eval hnf in [subType for tval].
+
Canonical tuple_subType :=
Eval hnf in [subType for tval].
Implicit Type t :
tuple_of.
@@ -79,61 +78,61 @@
Definition tsize of tuple_of :=
n.
-
Lemma size_tuple t :
size t = n.
+
Lemma size_tuple t :
size t = n.
-
Lemma tnth_default t :
'I_n → T.
+
Lemma tnth_default t :
'I_n → T.
Definition tnth t i :=
nth (
tnth_default t i)
t i.
-
Lemma tnth_nth x t i :
tnth t i = nth x t i.
+
Lemma tnth_nth x t i :
tnth t i = nth x t i.
-
Lemma map_tnth_enum t :
map (
tnth t) (
enum 'I_n)
= t.
+
Lemma map_tnth_enum t :
map (
tnth t) (
enum 'I_n)
= t.
-
Lemma eq_from_tnth t1 t2 :
tnth t1 =1 tnth t2 → t1 = t2.
+
Lemma eq_from_tnth t1 t2 :
tnth t1 =1 tnth t2 → t1 = t2.
Definition tuple t mkT :
tuple_of :=
-
mkT (
let:
Tuple _ tP :=
t return size t == n in tP).
+
mkT (
let:
Tuple _ tP :=
t return size t == n in tP).
-
Lemma tupleE t :
tuple (
fun sP ⇒ @
Tuple t sP)
= t.
+
Lemma tupleE t :
tuple (
fun sP ⇒ @
Tuple t sP)
= t.
End Def.
-
Notation "n .-tuple" := (
tuple_of n)
+
Notation "n .-tuple" := (
tuple_of n)
(
at level 2,
format "n .-tuple") :
type_scope.
-
Notation "{ 'tuple' n 'of' T }" := (
n.-tuple T : predArgType)
+
Notation "{ 'tuple' n 'of' T }" := (
n.-tuple T : predArgType)
(
at level 0,
only parsing) :
form_scope.
-
Notation "[ 'tuple' 'of' s ]" := (
tuple (
fun sP ⇒ @
Tuple _ _ s sP))
+
Notation "[ 'tuple' 'of' s ]" := (
tuple (
fun sP ⇒ @
Tuple _ _ s sP))
(
at level 0,
format "[ 'tuple' 'of' s ]") :
form_scope.
-
Notation "[ 'tnth' t i ]" := (
tnth t (@
Ordinal (
tsize t)
i (
erefl true)))
+
Notation "[ 'tnth' t i ]" := (
tnth t (@
Ordinal (
tsize t)
i (
erefl true)))
(
at level 0,
t,
i at level 8,
format "[ 'tnth' t i ]") :
form_scope.
-
Canonical nil_tuple T :=
Tuple (
isT : @
size T [::] == 0).
-
Canonical cons_tuple n T x (
t :
n.-tuple T) :=
-
Tuple (
valP t : size (
x :: t)
== n.+1).
+
Canonical nil_tuple T :=
Tuple (
isT : @
size T [::] == 0).
+
Canonical cons_tuple n T x (
t :
n.-tuple T) :=
+
Tuple (
valP t : size (
x :: t)
== n.+1).
-
Notation "[ 'tuple' x1 ; .. ; xn ]" :=
[tuple of x1 :: ..
[:: xn] ..
]
+
Notation "[ 'tuple' x1 ; .. ; xn ]" :=
[tuple of x1 :: ..
[:: xn] ..
]
(
at level 0,
format "[ 'tuple' '[' x1 ; '/' .. ; '/' xn ']' ]")
:
form_scope.
-
Notation "[ 'tuple' ]" :=
[tuple of [::]]
+
Notation "[ 'tuple' ]" :=
[tuple of [::]]
(
at level 0,
format "[ 'tuple' ]") :
form_scope.
@@ -146,31 +145,31 @@
Definition in_tuple (
s :
seq T) :=
Tuple (
eqxx (
size s)).
-
Definition tcast m n (
eq_mn :
m = n)
t :=
-
let:
erefl in _ = n :=
eq_mn return n.-tuple T in t.
+
Definition tcast m n (
eq_mn :
m = n)
t :=
+
let:
erefl in _ = n :=
eq_mn return n.-tuple T in t.
-
Lemma tcastE m n (
eq_mn :
m = n)
t i :
-
tnth (
tcast eq_mn t)
i = tnth t (
cast_ord (
esym eq_mn)
i).
+
Lemma tcastE m n (
eq_mn :
m = n)
t i :
+
tnth (
tcast eq_mn t)
i = tnth t (
cast_ord (
esym eq_mn)
i).
-
Lemma tcast_id n (
eq_nn :
n = n)
t :
tcast eq_nn t = t.
+
Lemma tcast_id n (
eq_nn :
n = n)
t :
tcast eq_nn t = t.
-
Lemma tcastK m n (
eq_mn :
m = n) :
cancel (
tcast eq_mn) (
tcast (
esym eq_mn)).
+
Lemma tcastK m n (
eq_mn :
m = n) :
cancel (
tcast eq_mn) (
tcast (
esym eq_mn)).
-
Lemma tcastKV m n (
eq_mn :
m = n) :
cancel (
tcast (
esym eq_mn)) (
tcast eq_mn).
+
Lemma tcastKV m n (
eq_mn :
m = n) :
cancel (
tcast (
esym eq_mn)) (
tcast eq_mn).
-
Lemma tcast_trans m n p (
eq_mn :
m = n) (
eq_np :
n = p)
t:
-
tcast (
etrans eq_mn eq_np)
t = tcast eq_np (
tcast eq_mn t).
+
Lemma tcast_trans m n p (
eq_mn :
m = n) (
eq_np :
n = p)
t:
+
tcast (
etrans eq_mn eq_np)
t = tcast eq_np (
tcast eq_mn t).
-
Lemma tvalK n (
t :
n.-tuple T) :
in_tuple t = tcast (
esym (
size_tuple t))
t.
+
Lemma tvalK n (
t :
n.-tuple T) :
in_tuple t = tcast (
esym (
size_tuple t))
t.
-
Lemma in_tupleE s :
in_tuple s = s :> seq T.
+
Lemma in_tupleE s :
in_tuple s = s :> seq T.
End CastTuple.
@@ -179,123 +178,123 @@
Section SeqTuple.
-
Variables (
n m :
nat) (
T U rT :
Type).
-
Implicit Type t :
n.-tuple T.
+
Variables (
n m :
nat) (
T U rT :
Type).
+
Implicit Type t :
n.-tuple T.
-
Lemma rcons_tupleP t x :
size (
rcons t x)
== n.+1.
+
Lemma rcons_tupleP t x :
size (
rcons t x)
== n.+1.
Canonical rcons_tuple t x :=
Tuple (
rcons_tupleP t x).
-
Lemma nseq_tupleP x : @
size T (
nseq n x)
== n.
+
Lemma nseq_tupleP x : @
size T (
nseq n x)
== n.
Canonical nseq_tuple x :=
Tuple (
nseq_tupleP x).
-
Lemma iota_tupleP :
size (
iota m n)
== n.
+
Lemma iota_tupleP :
size (
iota m n)
== n.
Canonical iota_tuple :=
Tuple iota_tupleP.
-
Lemma behead_tupleP t :
size (
behead t)
== n.-1.
+
Lemma behead_tupleP t :
size (
behead t)
== n.-1.
Canonical behead_tuple t :=
Tuple (
behead_tupleP t).
-
Lemma belast_tupleP x t :
size (
belast x t)
== n.
+
Lemma belast_tupleP x t :
size (
belast x t)
== n.
Canonical belast_tuple x t :=
Tuple (
belast_tupleP x t).
-
Lemma cat_tupleP t (
u :
m.-tuple T) :
size (
t ++ u)
== n + m.
+
Lemma cat_tupleP t (
u :
m.-tuple T) :
size (
t ++ u)
== n + m.
Canonical cat_tuple t u :=
Tuple (
cat_tupleP t u).
-
Lemma take_tupleP t :
size (
take m t)
== minn m n.
+
Lemma take_tupleP t :
size (
take m t)
== minn m n.
Canonical take_tuple t :=
Tuple (
take_tupleP t).
-
Lemma drop_tupleP t :
size (
drop m t)
== n - m.
+
Lemma drop_tupleP t :
size (
drop m t)
== n - m.
Canonical drop_tuple t :=
Tuple (
drop_tupleP t).
-
Lemma rev_tupleP t :
size (
rev t)
== n.
+
Lemma rev_tupleP t :
size (
rev t)
== n.
Canonical rev_tuple t :=
Tuple (
rev_tupleP t).
-
Lemma rot_tupleP t :
size (
rot m t)
== n.
+
Lemma rot_tupleP t :
size (
rot m t)
== n.
Canonical rot_tuple t :=
Tuple (
rot_tupleP t).
-
Lemma rotr_tupleP t :
size (
rotr m t)
== n.
+
Lemma rotr_tupleP t :
size (
rotr m t)
== n.
Canonical rotr_tuple t :=
Tuple (
rotr_tupleP t).
-
Lemma map_tupleP f t : @
size rT (
map f t)
== n.
+
Lemma map_tupleP f t : @
size rT (
map f t)
== n.
Canonical map_tuple f t :=
Tuple (
map_tupleP f t).
-
Lemma scanl_tupleP f x t : @
size rT (
scanl f x t)
== n.
+
Lemma scanl_tupleP f x t : @
size rT (
scanl f x t)
== n.
Canonical scanl_tuple f x t :=
Tuple (
scanl_tupleP f x t).
-
Lemma pairmap_tupleP f x t : @
size rT (
pairmap f x t)
== n.
+
Lemma pairmap_tupleP f x t : @
size rT (
pairmap f x t)
== n.
Canonical pairmap_tuple f x t :=
Tuple (
pairmap_tupleP f x t).
-
Lemma zip_tupleP t (
u :
n.-tuple U) :
size (
zip t u)
== n.
+
Lemma zip_tupleP t (
u :
n.-tuple U) :
size (
zip t u)
== n.
Canonical zip_tuple t u :=
Tuple (
zip_tupleP t u).
-
Lemma allpairs_tupleP f t (
u :
m.-tuple U) : @
size rT (
allpairs f t u)
== n × m.
+
Lemma allpairs_tupleP f t (
u :
m.-tuple U) : @
size rT (
allpairs f t u)
== n × m.
Canonical allpairs_tuple f t u :=
Tuple (
allpairs_tupleP f t u).
-
Definition thead (
u :
n.+1.-tuple T) :=
tnth u ord0.
+
Definition thead (
u :
n.+1.-tuple T) :=
tnth u ord0.
-
Lemma tnth0 x t :
tnth [tuple of x :: t] ord0 = x.
+
Lemma tnth0 x t :
tnth [tuple of x :: t] ord0 = x.
-
Lemma theadE x t :
thead [tuple of x :: t] = x.
+
Lemma theadE x t :
thead [tuple of x :: t] = x.
-
Lemma tuple0 :
all_equal_to (
[tuple] : 0
.-tuple T).
+
Lemma tuple0 :
all_equal_to (
[tuple] : 0
.-tuple T).
-
CoInductive tuple1_spec :
n.+1.-tuple T → Type :=
-
Tuple1spec x t :
tuple1_spec [tuple of x :: t].
+
Variant tuple1_spec :
n.+1.-tuple T → Type :=
+
Tuple1spec x t :
tuple1_spec [tuple of x :: t].
Lemma tupleP u :
tuple1_spec u.
-
Lemma tnth_map f t i :
tnth [tuple of map f t] i = f (
tnth t i)
:> rT.
+
Lemma tnth_map f t i :
tnth [tuple of map f t] i = f (
tnth t i)
:> rT.
End SeqTuple.
-
Lemma tnth_behead n T (
t :
n.+1.-tuple T)
i :
-
tnth [tuple of behead t] i = tnth t (
inord i.+1).
+
Lemma tnth_behead n T (
t :
n.+1.-tuple T)
i :
+
tnth [tuple of behead t] i = tnth t (
inord i.+1).
-
Lemma tuple_eta n T (
t :
n.+1.-tuple T) :
t = [tuple of thead t :: behead t].
+
Lemma tuple_eta n T (
t :
n.+1.-tuple T) :
t = [tuple of thead t :: behead t].
Section TupleQuantifiers.
-
Variables (
n :
nat) (
T :
Type).
-
Implicit Types (
a :
pred T) (
t :
n.-tuple T).
+
Variables (
n :
nat) (
T :
Type).
+
Implicit Types (
a :
pred T) (
t :
n.-tuple T).
-
Lemma forallb_tnth a t :
[∀ i, a (
tnth t i)
] = all a t.
+
Lemma forallb_tnth a t :
[∀ i, a (
tnth t i)
] = all a t.
-
Lemma existsb_tnth a t :
[∃ i, a (
tnth t i)
] = has a t.
+
Lemma existsb_tnth a t :
[∃ i, a (
tnth t i)
] = has a t.
-
Lemma all_tnthP a t :
reflect (
∀ i,
a (
tnth t i)) (
all a t).
+
Lemma all_tnthP a t :
reflect (
∀ i,
a (
tnth t i)) (
all a t).
-
Lemma has_tnthP a t :
reflect (
∃ i, a (
tnth t i)) (
has a t).
+
Lemma has_tnthP a t :
reflect (
∃ i, a (
tnth t i)) (
has a t).
End TupleQuantifiers.
@@ -306,79 +305,78 @@
Section EqTuple.
-
Variables (
n :
nat) (
T :
eqType).
+
Variables (
n :
nat) (
T :
eqType).
-
Definition tuple_eqMixin :=
Eval hnf in [eqMixin of n.-tuple T by <:].
-
Canonical tuple_eqType :=
Eval hnf in EqType (
n.-tuple T)
tuple_eqMixin.
+
Definition tuple_eqMixin :=
Eval hnf in [eqMixin of n.-tuple T by <:].
+
Canonical tuple_eqType :=
Eval hnf in EqType (
n.-tuple T)
tuple_eqMixin.
-
Canonical tuple_predType :=
-
Eval hnf in mkPredType (
fun t :
n.-tuple T ⇒
mem_seq t).
+
Canonical tuple_predType :=
PredType (
pred_of_seq : n.-tuple T → pred T).
-
Lemma memtE (
t :
n.-tuple T) :
mem t = mem (
tval t).
+
Lemma memtE (
t :
n.-tuple T) :
mem t = mem (
tval t).
-
Lemma mem_tnth i (
t :
n.-tuple T) :
tnth t i \in t.
+
Lemma mem_tnth i (
t :
n.-tuple T) :
tnth t i \in t.
-
Lemma memt_nth x0 (
t :
n.-tuple T)
i :
i < n → nth x0 t i \in t.
+
Lemma memt_nth x0 (
t :
n.-tuple T)
i :
i < n → nth x0 t i \in t.
-
Lemma tnthP (
t :
n.-tuple T)
x :
reflect (
∃ i, x = tnth t i) (
x \in t).
+
Lemma tnthP (
t :
n.-tuple T)
x :
reflect (
∃ i, x = tnth t i) (
x \in t).
-
Lemma seq_tnthP (
s :
seq T)
x :
x \in s → {i | x = tnth (
in_tuple s)
i}.
+
Lemma seq_tnthP (
s :
seq T)
x :
x \in s → {i | x = tnth (
in_tuple s)
i}.
End EqTuple.
Definition tuple_choiceMixin n (
T :
choiceType) :=
-
[choiceMixin of n.-tuple T by <:].
+
[choiceMixin of n.-tuple T by <:].
Canonical tuple_choiceType n (
T :
choiceType) :=
-
Eval hnf in ChoiceType (
n.-tuple T) (
tuple_choiceMixin n T).
+
Eval hnf in ChoiceType (
n.-tuple T) (
tuple_choiceMixin n T).
Definition tuple_countMixin n (
T :
countType) :=
-
[countMixin of n.-tuple T by <:].
+
[countMixin of n.-tuple T by <:].
Canonical tuple_countType n (
T :
countType) :=
-
Eval hnf in CountType (
n.-tuple T) (
tuple_countMixin n T).
+
Eval hnf in CountType (
n.-tuple T) (
tuple_countMixin n T).
Canonical tuple_subCountType n (
T :
countType) :=
-
Eval hnf in [subCountType of n.-tuple T].
+
Eval hnf in [subCountType of n.-tuple T].
Module Type FinTupleSig.
Section FinTupleSig.
-
Variables (
n :
nat) (
T :
finType).
-
Parameter enum :
seq (
n.-tuple T).
+
Variables (
n :
nat) (
T :
finType).
+
Parameter enum :
seq (
n.-tuple T).
Axiom enumP :
Finite.axiom enum.
-
Axiom size_enum :
size enum = #|T| ^ n.
+
Axiom size_enum :
size enum = #|T| ^ n.
End FinTupleSig.
End FinTupleSig.
Module FinTuple :
FinTupleSig.
Section FinTuple.
-
Variables (
n :
nat) (
T :
finType).
+
Variables (
n :
nat) (
T :
finType).
-
Definition enum :
seq (
n.-tuple T) :=
-
let extend e :=
flatten (
codom (
fun x ⇒
map (
cons x)
e))
in
-
pmap insub (
iter n extend [::[::]]).
+
Definition enum :
seq (
n.-tuple T) :=
+
let extend e :=
flatten (
codom (
fun x ⇒
map (
cons x)
e))
in
+
pmap insub (
iter n extend [::[::]]).
Lemma enumP :
Finite.axiom enum.
-
Lemma size_enum :
size enum = #|T| ^ n.
+
Lemma size_enum :
size enum = #|T| ^ n.
End FinTuple.
@@ -388,39 +386,49 @@
Section UseFinTuple.
-
Variables (
n :
nat) (
T :
finType).
+
Variables (
n :
nat) (
T :
finType).
-
Canonical tuple_finMixin :=
Eval hnf in FinMixin (@
FinTuple.enumP n T).
-
Canonical tuple_finType :=
Eval hnf in FinType (
n.-tuple T)
tuple_finMixin.
-
Canonical tuple_subFinType :=
Eval hnf in [subFinType of n.-tuple T].
+
+
+
+ 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.
+
+