lean fromList

Stream: new members

[Alok Singh (S1'17)]

Given

  | empty: Vect 0
  | cons {n:Nat} (a:Nat) (v:Vect n) : Vect (n+1)


def plus (v1:Vect n) (v2:Vect n) : Vect  n:=
  match (v1,v2) with
  | (Vect.empty, _) => Vect.empty
  | (Vect.cons a v, Vect.cons b w) => Vect.cons  (a + b) (plus v w)


def fromlist (v: List Nat): Vect (n:Nat):=
  match v with
  | [] => Vect.empty
  | List.cons x xs => Vect.cons x xs

def main : IO Unit :=
    IO.println "foo"

I get 2 errors:

./Test.lean:14:10: error: type mismatch
  Vect.empty
has type
  Vect 0 : Type ?u.1922
but is expected to have type
  Vect n : Type ?u.1922

How would I get this to work?

[Yakov Pechersky]

You're not sharing your whole code. Where do you define what n is? Is it a variable or a parameter or what? In any case, your fromlist function won't work because it's not actually recursive. And I'd suggest using the equation compiler on your variables instead of match, if you want to prove things about your definitions later on.

[Alex J. Best]

@Yakov Pechersky As this is lean4 I guess n doesn't need to be defined due to https://leanprover.github.io/lean4/doc/autobound.html

[Alex J. Best]

@Alok Singh (S1'17) the first line of your code is chopped off, you need a newline after ```

[Yakov Pechersky]

Ah yes, I should have noticed it was lean 4 from the =>, apologies

[Alex J. Best]

For plus, matching on n too works

def plus (v1 : Vect n) (v2 : Vect n) : Vect  n:=
  match n, v1, v2 with
  | 0, _, _ => Vect.empty
  | (n + 1), Vect.cons a v, Vect.cons b w => Vect.cons (a + b) (plus v w)

[Alex J. Best]

As for the fromlist function, I'm not sure really what the best way to do what you want is, but the following does typecheck at least:

def fromlist (v: List Nat) : Vect v.length :=
  match v with
  | [] => Vect.empty
  | List.cons x xs => xs.length_cons _ ▸ Vect.cons x (fromlist xs)

we have to specify in the function definition what the length of the vector is (the length of the input list).
Then we are forced to use the triangle to make the Vector length line up right.
So I'm not sure how convenient it will be to prove things about this definition tbh.

[Alok Singh (S1'17)]

what does the triangle do?

[Mario Carneiro]

it's basically term mode rw