Use Pattern with Vectors in Assumptions

I had a problem using Pattern with Vectors in Assumptions.

Here's how I use Pattern in Assumptions:

(* Input := *) Simplify[Element[y[i], Anything], Element[y[_], Anything]]
(* Output:= True *)


Mathematica does assume that any variable matching y[_] is an element of Anything. However, if I replace Anything by Vectors[n], Mathematica no longer assumes that:

(* Input := *) Simplify[Element[y[i], Vectors[n]], Element[y[_], Vectors[n]]]
(* Output:= Element[y[i], Vectors[n, Complexes]] *)


in which I expect to get an ouput of True. So where is the problem?

Update: The problem exists only in v9, in which Vectors is introduced as a built-in function. (Thanks Māris Ozols for clarifying it.)

Below Michael E2 gave a solution, replacing Element[y[_], Vectors[n]] by HoldPattern@Element[y[_], Vectors[n,Complexes]]. This partially solves the problem, but it is not what I want, because it does not really assume y[_] is a vector. See the following code.

(*Input := *) \$Assumptions = {HoldPattern[Element[y[_], Vectors[n, Complexes]]],
Element[x[1], Vectors[n]], Element[z[_], Vectors[n]]};
(*Input := *) Simplify[{Element[y[i], Vectors[n]], Element[x[1], Vectors[n]],
Element[z[i], Vectors[n]]}]
(*Output:= {True, True, Element[z[i], Vectors[n, Complexes]]}*)
(*Input := *) TensorRank /@ {y[i], x[1], z[i]}
(*Ouput:=  {TensorRank[y[i]], 1, TensorRank[z[i]]}*)


Above only x[1] behaves as a vector, but y[i] and z[i] not. HoldPattern only makes Element[y[i], Vectors[n]] true, but will not make y[i] a vector. I want y[i] to behave like x[1].

-
Use Refine[] instead of Simplify[] –  belisarius Oct 5 '13 at 11:41
Refine[expr,assum] gives the form of expr that would be obtained if symbols in it were replaced by explicit numerical expressions satisfying the assumptions assum. –  belisarius Oct 5 '13 at 11:41
Simplify[Element[y[i], Vectors[n]], Element[y[_], Vectors[n]]] gives True on Mathematica 8.0.4 for Windows. Looks like a bug in v.9. –  Alexey Popkov Oct 6 '13 at 1:19
The reason it gives True in Mathematica 8.0.4 is that Vectors[n] was introduced only in 9.0. Thus, in 8.0.4 it makes no difference if you write Anything or Vectors[n], since neither is defined. –  Māris Ozols Oct 6 '13 at 1:33
It also persists if Vectors is replaced by Matrices or Arrays. But it does not appear when other domains are used, such as Integers. Thus, it seems that it is specific only to the new Symbolic Tensors domains. –  Māris Ozols Oct 6 '13 at 2:17
show 1 more comment

I don't know why your code does not work. But here's a workaround:

Simplify[Element[y[i], Vectors[n]], hyp_ /; MatchQ[hyp, Element[y[_], Vectors[n]]]]
(* True *)


Update

I can add a little bit more:

Vectors is a defined system symbol in V9 but not in V8 or earlier. The command

Simplify[Element[y[i], Foo[n]], Element[y[_], Foo[n]]]


returns True in V9, just as the command

Simplify[Element[y[i], Vectors[n]], Element[y[_], Vectors[n]]]


returns True in V8, as Alexey Popkov commented. The problems seems to have to do with the pattern Vectors[n] being evaluated, for the pattern works when it is held:

Simplify[Element[y[i], Vectors[n]], HoldPattern @ Element[y[_], Vectors[n, Complexes]]]
(* True *)


Note: Because the pattern is held and Vectors[n] automatically expands to Vectors[n, Complexes] (when not held), I needed to substitute the correct pattern.

-
Could you please explain how it works? I cannot find an example of Assumption of such form in the Documentation and confused. What does really mean such an Assumption? –  Alexey Popkov Oct 6 '13 at 1:25
@AlexeyPopkov I'm not exactly sure - that is to say, I can guess. Assumptions somehow have to be matched with (sub)expressions in order to apply them. I had (thoughtlessly) assumed that they would be literal matches, but the OP's question showed general patterns might work. I got a few things to be successful, and the one posted seemed simplest. I'll try to think of a more complete explanation, if I can find one. –  Michael E2 Oct 6 '13 at 1:32
I don't get True when using HoldPattern in Mathematica 9.0.1. –  Māris Ozols Oct 6 '13 at 2:09
@MārisOzols Oops, I accidentally removed Complexes where it was needed. Thanks! –  Michael E2 Oct 6 '13 at 2:39