defining a map out of a list

Stream: new members

[Dean Young]

How do I inductively define a map out of a list?

def sum_the_elements  : (sequence : List Int) → Int :=
  match sequence with
  | a ++ [s] => (sum_the_elements a) + s

[Dean Young]

I want to modify the example to produce a function which sums the elements.

[Henrik Böving]

is there a particular rreason you are not matching on nil and cons but instead on append?

[Kyle Miller]

docs4#List.sum will sum the elements of a list.

[Kyle Miller]

Notice that List.foldl in its definition is a way to recurse where the last element is summed last.

[Dean Young]

@Henrik Böving for my purposes I want something that appends at the end of the list and not the beginning.

[Henrik Böving]

Right but why is that relevant to yourr sum function? It is commutative anyways

[Dean Young]

I was just interested in learning how it works I think.

But I can't even seem to get this to work:

def j (l : List Int) : Int :=
  match l with
  | cons fdfd fdfd2 => (j fdfd2) + fdfd
  | nil => 0

lean seems to think that fdfd is a proposition.

[Dean Young]

def append (as bs : List α) : List α :=
  match as with
  | nil       => bs
  | cons a as => cons a (append as bs)

this example is taken from the tutorial, but my lean thinks that nil is supposed to be a proposition.

[Dean Young]

this is lean 4 by the way

[Henrik Böving]

No, the issue with your code is that cons and nil are not top leve identifiers so you have to do one of List.cons .cons (note the dot) fdfd :: fdfd2 and [] or open the List namespace which is most likely what happened in the example

[Henrik Böving]

Kind Bubble said:

this is lean 4 by the way

I know^^

[Dean Young]

Is opening the List namespace recommendable? Does that just tell Lean to use the terminology from the list section of documentation?

[Henrik Böving]

So, there are actually two ways of opening the List name space, you can open List which basically takes all identifiers frrom the List namespace and makes them directly accessible or you can use

namespace List

def function...

end List

which actually adds function to the List namespace so you can later do List.function or even use xs.function where xs is a List. The second is (obviously) interesting if you wish to extend the functions directly available on List. The first is interesting if you want to just use functionality from a namespace. However given the fact that you can even use the [] and :: syntax to match on a list I see no reason to do the open List thing. I would usually use it when for example writing a Lean metaproogramm to open Lean so you don't have to prefix literally every line with Lean.

[Dean Young]

I think it has another issue though,

inductive jkljkl (α : Type) where
| nil  : jkljkl α
| cons : α → jkljkl α → jkljkl α

gives me

Main.lean:44:9: error: type expected
failed to synthesize instance
  CoeSort (?m.6367 = ?m.6392) ?m.6398
Main.lean:45:7: error: expected command

[Eric Wieser]

You've only shown us three lines, and your error is on line 44

[Eric Wieser]

Can you make a #mwe?

[Dean Young]

oh thanks, that made me realize that I had defined

notation p "|" q => transitivity p q

which is no good!

[Eric Wieser]

If you're not familiar yet with Lean 4's regular syntax, I would strongly recommend against defining your own syntax that remotely resembles something that is builtin

[Dean Young]

Ok -- and thanks for your help.
@Henrik Böving thanks!