Lean is a programming language created in 2015 by Leonardo de Moura.
| #195on PLDB | 8Years Old | 2.9kUsers |
| 4Books | 10Papers | 2kRepos |
Try now: TIO
Lean Theorem Prover
#print "Hello World"/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.binary
Authors: Leonardo de Moura, Jeremy Avigad
General properties of binary operations.
-/
import logic.eq
open eq.ops
namespace binary
section
variable {A : Type}
variables (op₁ : A → A → A) (inv : A → A) (one : A)
local notation a * b := op₁ a b
local notation a ⁻¹ := inv a
local notation 1 := one
definition commutative := ∀a b, a * b = b * a
definition associative := ∀a b c, (a * b) * c = a * (b * c)
definition left_identity := ∀a, 1 * a = a
definition right_identity := ∀a, a * 1 = a
definition left_inverse := ∀a, a⁻¹ * a = 1
definition right_inverse := ∀a, a * a⁻¹ = 1
definition left_cancelative := ∀a b c, a * b = a * c → b = c
definition right_cancelative := ∀a b c, a * b = c * b → a = c
definition inv_op_cancel_left := ∀a b, a⁻¹ * (a * b) = b
definition op_inv_cancel_left := ∀a b, a * (a⁻¹ * b) = b
definition inv_op_cancel_right := ∀a b, a * b⁻¹ * b = a
definition op_inv_cancel_right := ∀a b, a * b * b⁻¹ = a
variable (op₂ : A → A → A)
local notation a + b := op₂ a b
definition left_distributive := ∀a b c, a * (b + c) = a * b + a * c
definition right_distributive := ∀a b c, (a + b) * c = a * c + b * c
end
context
variable {A : Type}
variable {f : A → A → A}
variable H_comm : commutative f
variable H_assoc : associative f
infixl `*` := f
theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) :=
take a b c, calc
a*(b*c) = (a*b)*c : H_assoc
... = (b*a)*c : H_comm
... = b*(a*c) : H_assoc
theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b :=
take a b c, calc
(a*b)*c = a*(b*c) : H_assoc
... = a*(c*b) : H_comm
... = (a*c)*b : H_assoc
end
context
variable {A : Type}
variable {f : A → A → A}
variable H_assoc : associative f
infixl `*` := f
theorem assoc4helper (a b c d) : (a*b)*(c*d) = a*((b*c)*d) :=
calc
(a*b)*(c*d) = a*(b*(c*d)) : H_assoc
... = a*((b*c)*d) : H_assoc
end
end binary
| Feature | Supported | Token | Example |
|---|---|---|---|
| Comments | ✓ | ||
| Line Comments | ✓ | ||
| Integers | ✓ | ||
| Strings | ✓ | " | "Hello world" |
| Print() Debugging | ✓ |
| title | authors | year | publisher |
|---|---|---|---|
| Functional Programming Patterns in Scala and Clojure: Write Lean Programs for the JVM | Bevilacqua-Linn, Michael | 2013 | Pragmatic Bookshelf |
| Measuring and Improving Performance: Information Technology Applications in Lean Systems | Martin, James William | 2009 | CRC Press |
| Lean Python: Learn Just Enough Python to Build Useful Tools | Gerrard, Paul | 2016 | Apress |
| Lean Software Systems Engineering for Developers: Managing Requirements, Complexity, Teams, and Change Like a Champ | Durham, Doug and Michel, Chad | 2021 | Apress |