I'd like to remove tcast in a "lemma" such as the following one. But this doesn't even typecheck, due to dependent-typing "constraints".
Lemma foo : forall {T} m n (tc : n = m) (f : m.-tuple T -> 'I_n -> nat) (x : n.-tuple T),
[seq f (tcast tc x) j | j <- enum 'I_n] =
[seq f x j | j <- enum 'I_n].
In fact, a more significant example for the application I have in mind, and which does typecheck, would be the following lemma:
Lemma bar n1 n2 n (tc : n1 + n2 = n) (l1 : n1.-tuple nat) (l2 : n2.-tuple nat) :
\sum_(i < n) tnth (tcast tc [tuple of (l1 ++ l2)]) i =
\sum_(i < n1) tnth l1 i + \sum_(i < n2) tnth l2 i.
This would be simple on seq, but here I cannot find how to proceed using lemmas in tuple.v or fintype.v.
So what is the proper way to address such tcast expressions when they don't seem to be amenable to treatment via val_inj and case analysis (see previous post)? Do I have, in the first example, to introduce two versions of f, later proved to be equal over sequences (and if so, what would be the best way to proceed)?
Thanks in advance for any suggestion.
Pierre
In the case you post, you can remove the casts using the standard trick:
Lemma val_tcast {T} m n (tc : n = m) (x : n.-tuple T) :
val (tcast tc x) = val x.
Proof. by case: m / tc. Qed.
Lemma sum_tuple n (t : n.-tuple nat) :
\sum_(i < n) tnth t i = \sum_(i < n) nth 0 (val t) i.
Proof. by apply: eq_bigr => ? ?; rewrite (tnth_nth 0). Qed.
Lemma bar n1 n2 n (tc : n1 + n2 = n) (l1 : n1.-tuple nat) (l2 : n2.-tuple nat) :
\sum_(i < n) tnth (tcast tc [tuple of (l1 ++ l2)]) i =
\sum_(i < n1) tnth l1 i + \sum_(i < n2) tnth l2 i.
Proof.
rewrite !sum_tuple val_tcast /=.
Tho there is a direct proof:
Lemma bar' n1 n2 n (tc : n1 + n2 = n) (l1 : n1.-tuple nat) (l2 : n2.-tuple nat) :
\sum_(i < n) tnth (tcast tc [tuple of (l1 ++ l2)]) i =
\sum_(i < n1) tnth l1 i + \sum_(i < n2) tnth l2 i.
Proof. by rewrite -!(big_tuple _ _ _ predT id) val_tcast big_cat. Qed.