Zulip Chat Archive

Stream: new members

Topic: lean fromList


Alok Singh (S1'17) (Jun 17 2021 at 11:32):

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 (Jun 17 2021 at 12:02):

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 (Jun 17 2021 at 12:23):

@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 (Jun 17 2021 at 12:24):

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

Yakov Pechersky (Jun 17 2021 at 12:24):

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

Alex J. Best (Jun 17 2021 at 12:41):

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 (Jun 17 2021 at 13:52):

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) (Jun 18 2021 at 01:08):

what does the triangle do?

Mario Carneiro (Jun 18 2021 at 01:20):

it's basically term mode rw


Last updated: Dec 20 2023 at 11:08 UTC