Lean as a programming language

Stream: new members

[Ocschwar]

Hi, all. I'm trying to write some inane functions in lean so that I can prove theorems about their properties, and I'm having trouble because the introductory material is concentrated on the prover and tactics. Is there a reference on the language syntax, so I can make some progress here? (I'm hoping to do an Advent of Lean, where first I write code to answer the challenge of the day, and then prove as much as I can about the functions written.)

[Ocschwar]

Current pitfall:

  match z with
  | z > 1 := 0
  | z = 0 := 1
  end

[Ocschwar]

[Ocschwar]

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)

[Ocschwar]

Answering my own question partially:
set_option should go after the imports at which point VS Code shows this "
invalid pattern, must be an application, constant, variable, type ascription, aliasing pattern or inaccessible term"

[Kyle Miller]

match is for pattern matching (deconstructing inductive types by patterns). You seem to be looking for if ... then ... else ...

[Kyle Miller]

There's also cmp, which you can pattern match:

def testf (z : ℤ) : string  :=
  match cmp z 0 with
  | ordering.gt := "greater than 0"
  | ordering.eq := "equal to 0"
  | ordering.lt := "less than 0"
  end

#eval testf 1

[Kyle Miller]

Learning resources: https://leanprover-community.github.io/learn.html

Reference manual: https://leanprover.github.io/reference/

[Reid Barton]

You might also be interested in https://github.com/digama0/advent-of-code or https://github.com/rwbarton/advent-of-lean-4, although neither of these contains proofs

[Kevin Buzzard]

There's also theorem proving in lean 4

[Johan Commelin]

And @James King just posted https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lean.204.20hackers/near/261451747 with a link to https://agentultra.github.io/lean-4-hackers/

[Ocschwar]

Okay, this makes much more sense now. Thanks, everyone!

[Ocschwar]

And, from the Hitchiker's guid. an example of a lemma proved for a function in page 90:

{ red   := rgb.green c,
  green := rgb.blue c,
  blue  := rgb.red c }
The definition relies on the generated selectors rgb.red, rgb. green, and rgb.blue. Instead of rgb.red c, we could also write c.red, and similarly for the other fields. Sometimes we will see these forms in Lean’s output, even if we do not use them ourselves.
Applying shuffle three times in a row is the same as not apply- ing it at all:
lemma shuffle_shuffle_shuffle (c : rgb) :
  shuffle (shuffle (shuffle c)) = c :=
begin
cases’ c,
refl
end