Introduction to Lean

$ curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

$ lake new playground
$ cd playground

playground/
├── Playground/
│   └── Basic.lean
├── Playground.lean
├── lakefile.toml
└── lean-toolchain

$ lake build

[[require]]
name = "mathlib"
scope = "leanprover-community"

$ lake update
$ lake exe cache get
$ lake build

theorem two_plus_two : 2 + 2 = 4 := by
  rfl

α : Type u_1
x : α
xs ys : List α
ih : sum (xs ++ ys) = sum xs + sum ys
⊢ sum (x :: xs ++ ys) = sum (x :: xs) + sum ys

theorem hard : P = Q := by
  sorry

#check List.append_assoc   -- what is its statement
#print List.length         -- how is it defined
#eval sum [1, 2, 3]        -- run it

def sum : List Nat → Nat
  | [] => 0
  | x :: xs => x + sum xs

theorem sum_append (xs ys : List Nat) :
    sum (xs ++ ys) = sum xs + sum ys := by
  sorry

theorem sum_append (xs ys : List Nat) :
    sum (xs ++ ys) = sum xs + sum ys := by
  induction xs with
  | nil => sorry
  | cons x xs ih => sorry

  | nil => simp [sum]

  | cons x xs ih => simp [sum, ih, Nat.add_assoc]

theorem sum_append (xs ys : List Nat) :
    sum (xs ++ ys) = sum xs + sum ys := by
  induction xs with
  | nil => simp [sum]
  | cons x xs ih => simp [sum, ih, Nat.add_assoc]

rfl              both sides reduce to the same thing
exact h          h is precisely the goal
assumption       some hypothesis is, find it
trivial          the goal is True, rfl, or similar
decide           the proposition is decidable, so compute the answer

intro x          move a binder from the goal into context
apply f          reduce the goal to f's arguments
refine e ?_      apply, with holes you name and fill later
constructor      split a conjunction or pick a structure's constructor
exfalso          replace the goal with False

rw [Nat.add_comm]
rw [← Nat.add_assoc]
rw [h1, h2] at hyp
subst h            -- h : a = b, replace b everywhere

cases xs with
  | nil => ...
  | cons x xs => ...
 
rcases h with ⟨a, b⟩      -- destructure a conjunction or existential
obtain ⟨x, hx⟩ := h       -- the same thing, reads better forwards

simp             rewrite with the simp set until stuck
simp [f, h]      ... plus these definitions and hypotheses
simp at h        ... in a hypothesis
omega            linear arithmetic over Nat and Int
linarith         linear arithmetic over ordered fields (mathlib)
positivity       this expression is positive (mathlib)
norm_num         evaluate numeric expressions (mathlib)
aesop            general-purpose search (mathlib)

example (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by
  exact?
 
Try this: exact List.length_append xs ys

  simp?
 
Try this: simp only [List.length_append, Nat.add_comm]

apply?           library results whose conclusion matches
exact?           ... that close the goal outright
rw?              rewrites applicable here
hint             run several tactics and report which worked

example (xs ys : List α) :
    (xs ++ ys).length = xs.length + ys.length := by
  simp says simp only [List.length_append]

theorem example1 (a b : Nat) (h : a ≤ b) : a ≤ b + 1 := by
  have h2 : b ≤ b + 1 := Nat.le_succ b
  exact Nat.le_trans h h2

theorem example2 (a b c : Nat) (h1 : a = b) (h2 : b = c) : a + 0 = c := by
  calc a + 0 = a := Nat.add_zero a
    _ = b := h1
    _ = c := h2

theorem example3 (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp
  · exact hq

  show 0 + n = n
  simp

def main : IO Unit := do
  let xs := [1, 2, 3]
  IO.println s!"sum = {sum xs}"

$ lake build
$ lake exe playground

def head! (xs : List α) (h : xs ≠ []) : α :=
  match xs, h with
  | x :: _, _ => x
 
#eval head! [1, 2, 3] (by simp)

$ lake build
$ ls .lake/build/bin/