Zulip Chat Archive

Stream: general

Topic: Use list as an argument


view this post on Zulip Blair Shi (Jul 11 2018 at 08:36):

I define a function which takes a list as a argument but I do not know why it always break when I use it in my other theorem or function.
my function no error:

def f_span (l : list V) : set V :=
span {vc : V | vc ∈ l}

use it later in

def are_basis_equal (l₀ : list V) (l₁ : list V) : Prop :=
∀vc : V, vc ∈ (f_span l₀) ∧ vc ∈ (f_span l₁)

it reports error :

[Lean]
type mismatch at application
  f_span l₀
term
  l₀
has type
  list V : Type v
but is expected to have type
  Type ? : Type (?+1)

view this post on Zulip Kevin Buzzard (Jul 11 2018 at 08:46):

You have some variable V somewhere, I guess?

view this post on Zulip Kevin Buzzard (Jul 11 2018 at 08:46):

If you look at what you wrote as the definition of f_span then it looks like it is expecting one input, namely l of type list V

view this post on Zulip Kevin Buzzard (Jul 11 2018 at 08:47):

But after the definition of f_span, if you write #check f_span you will probably see a different story!

view this post on Zulip Kevin Buzzard (Jul 11 2018 at 08:47):

Probably f_span is also expecting you to input V itself. So that's my guess as to what your error is caused by -- you need f_span V l_0

view this post on Zulip Kevin Buzzard (Jul 11 2018 at 08:48):

The trick is to make V a {} variable; then f_span won't ask for it. I've got to run but that's the idea

view this post on Zulip Sean Leather (Jul 11 2018 at 08:59):

But after the definition of f_span, if you write #check f_span you will probably see a different story!

Even better would be to write #check @f_span. That fills in those pesky metavariables with something readable.

view this post on Zulip Blair Shi (Jul 11 2018 at 09:17):

I added more argument using [] and it works now. thank you !

view this post on Zulip Sean Leather (Jul 11 2018 at 09:21):

@Blair Shi Can you show us what it looks like now?

view this post on Zulip Blair Shi (Jul 11 2018 at 09:39):

def f_span (l : list V) : set V :=
span {vc : V | vc ∈ l}
def are_basis_equal (l₀ : list V) (l₁ : list V) : Prop :=
∀vc : V, vc ∈ (f_span k V l₀) ∧ vc ∈ (f_span k V l₁)

I just added k V everywhere when I using the function f_span without any change of f_span

Because if you check my f_span, the type is

f_span :
  Π (k : Type u_1) (V : Type u_2) [_inst_1 : field k] [_inst_2 : ring k] [_inst_3 : module k V], list V → set V

I also tried like added (k : Type u_1) (V : Type u_2) [_inst_1 : field k] [_inst_2 : ring k] [_inst_3 : module k V] all of them as arguments to my f_span but I realized I don't need to do so. But adding arguments also works for me.

view this post on Zulip Patrick Massot (Jul 11 2018 at 09:43):

Are you sure you're not duplicating stuff around https://github.com/leanprover/mathlib/blob/master/linear_algebra/basic.lean#L122?

view this post on Zulip Blair Shi (Jul 11 2018 at 09:52):

@Patrick Massot because the vector space in mathlib does not support finite dimensional vector space. I am currently working on finite dimensional vector space and in the definition of finite dimensional vector space, the basis is a list.

view this post on Zulip Blair Shi (Jul 11 2018 at 09:57):

@Sean Leather
I realized I have wrote the global variables and if I delete them the code does not work

variables (k : Type u) (V : Type v)
variable [field k]
variables [ring k] [module k V]
variables (a : k) (b : V)
include k

view this post on Zulip Patrick Massot (Jul 11 2018 at 10:00):

Ok. I remember we had this discussion about ordering basis elements here.

view this post on Zulip Mario Carneiro (Jul 11 2018 at 10:10):

You want variables {k : Type u} {V : Type v} in the first line

view this post on Zulip Blair Shi (Jul 11 2018 at 10:23):

I change it to be {k : Type u} {V : Type v}as you said. Now I delete all k V when I use the function:)

view this post on Zulip Kevin Buzzard (Jul 11 2018 at 10:24):

ordering basis elements -- it's a funny situation! In the general case you seem to want a basis to be a set. But to prove the standard undergraduate theorems about linear maps = matrices you seem to want the basis to be a finite totally ordered set.

view this post on Zulip Kevin Buzzard (Jul 11 2018 at 10:26):

@Blair Shi yes -- if you are doing vector spaces over a field field k then you don't want to have to keep mentioning k. If you're doing k-linear maps between vector spaces V and W then you probably want to mention V but if you're doing things with a fixed V like showing that sets of size less than dim(V) can't span then you might not even want to mention V. This is how those {} and () brackets that I talked about in my lecture on Monday work in practice. There are tricks to change the variable from () to {}and back in the middle of a file which I can tell you about later if you need them.


Last updated: May 13 2021 at 06:15 UTC