Zulip Chat Archive

Stream: new members

Topic: Lean as a programming language


Ocschwar (Nov 15 2021 at 02:25):

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 (Nov 15 2021 at 02:25):

Current pitfall:

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

Ocschwar (Nov 15 2021 at 02:26):

Ocschwar (Nov 15 2021 at 02:26):

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

Ocschwar (Nov 15 2021 at 02:49):

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 (Nov 15 2021 at 02:49):

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

Kyle Miller (Nov 15 2021 at 02:52):

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 (Nov 15 2021 at 02:53):

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

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

Reid Barton (Nov 15 2021 at 04:47):

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 (Nov 15 2021 at 07:18):

There's also theorem proving in lean 4

Johan Commelin (Nov 15 2021 at 07:56):

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 (Nov 15 2021 at 13:16):

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

Ocschwar (Nov 19 2021 at 05:11):

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

Last updated: Dec 20 2023 at 11:08 UTC