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