simple pattern matching with lean4

Stream: new members

[Tobias Grosser]

Hey guys (@Sebastian Ullrich?),

I am trying to get the following code to compile in lean4:

cat test.lean
import init.data.int.basic
import init.data.string.basic

def foo (ctx : String) : Int → Int
| x => if ctx == "a" then x else (foo "a" x)
$lean test.lean
/home/grosser/Projects/lean4/test.lean:4:4: error: type mismatch at application
  foo "a"
term
  "a"
has type
  String
but is expected to have type
  Int
$cat test2.lean
import init.data.int.basic
import init.data.string.basic

def foo : String → Int → Int
| "a" x => x
| _ x => foo "a" x
$lean test2.lean
/home/grosser/Projects/lean4/test2.lean:4:4: error: invalid application, function expected

The example is obviously artificial and reduced from an example that is a lot larger. What I want to do is -- in certain cases -- change the first argument and then recurse into the very same function with the updated first argument. Unfortunately, this does not seem to work. In the first test.lean file it seems ctx is already implicitly passed as the first argument to foo such that only the second argument can be passed to foo. In the second test case I get an error message which I do not fully understand. Any ideas?

[Reid Barton]

The first one is wrong in Lean 3 for the reason you say, I assume it is the same in Lean 4.
It looks like the second one needs commas in Lean 4, judging from (for example) https://github.com/leanprover/lean4/blob/master/library/init/data/list/basic.lean

[Tobias Grosser]

This seems to work. Thanks a lot. I should have looked myself a little deeper. I had the feeling I may have misunderstood sth basic, but it seems some syntax changed and the error message is not super descriptive. Thanks @Reid Barton for providing details here.

[Kevin Buzzard]

Wow, I hadn't really appreciated the following: that Lean 4 file (with all the CamelCase changes etc) still says copyright 2016 on it. Is that how it works? When mathlib gets ported we leave all the copyrights as they were -- they're not "new files"?

[Patrick Massot]

@Sebastian Ullrich will we keep that ASCII art =>? Or is it only used in core before the parser is able to handle a proper unicode arrow?

[Patrick Massot]

To all people who post Lean 4 code, do you understand correctly that there is still no VScode extension and you use Lean 4 non-interactively (or using emacs)?

[Sebastian Ullrich]

@Patrick Massot ⇒ does already work. Leo seems to prefer the ASCII arrow, but we haven't really discussed coding styles so far (which of course we should do exactly once when implementing a standard code formatter for Lean 4 and then never talk about this topic again).

[Mario Carneiro]

wait, so the preference is unicode lambda + ascii arrow?

[Sebastian Ullrich]

No, Leo's current preference is fun + =>. My preference may be fun + ⇒ but I haven't really decided yet.

[Patrick Massot]

Returning to ASCII would be really sad. Readable unicode is the first thing that attracts mathematicians to Lean after seeing Coq.

[Mario Carneiro]

have you ever read agda code?

[Mario Carneiro]

unicode can be overused

[Marc Huisinga]

is exchanging unicode for ascii the motivation for using fun instead of \lam as well?

[Marc Huisinga]

i suppose λ foo => bar would look a bit strange

[Patrick Massot]

This is no need to overuse unicode. We can keep words, but avoid ascii art.

[Mario Carneiro]

I like using ascii art for programmy stuff and unicode for math stuff

[Patrick Massot]

You can define functions in math

[Mario Carneiro]

I'm sure Scott and co will reserve all the arrows

[Mario Carneiro]

by programmy stuff I mean lean core

[matt rice]

Sometimes wish that the ascii -> unicode happened not in the editors input mechanism, but by running a pass over ASCII sources. So it would be represented as \lam foo, bar then converted to λ foo, bar for display... Not sure it'd be at all readable, but perhaps helpful if you weren't familiar with a symbol, but there are also tons of search boxes which are terrible at unicode... :shrug: