lean2/doc/intro.org

• Introduction
• Big picture
• The logical framework
• Reasoning about abstractions
• Constructive and classical logic
• Lean interfaces
• Future work
• Future work (cont.)
• Example

Introduction

• Lean is a new automated/interactive theorem prover.

• It is a powerful system for

  • reasoning about complex systems
  • reasoning about mathematics
  • proving claims about both
• It aims to bring the automated and interactive theorem proving worlds together.

Big picture

• Proving should be as easy as programming.

  • We can teach logic to any kid that knows how to program.

• Lean as a new engine for software verification tools.

  • Lean offers a much richer language.
  • We offer multiple APIs (C/C++, Lua, Lean, Javascript).

• Impact on education.

  • We want to have a "live" and formalized version of Euclid's Elements (book 1).
  • Natural deduction style proofs are like flowcharts, they should be "eradicated".
• Revolutionize mathematics.

The logical framework

• Lean's default logical framework is a version of the Calculus of Constructions with:

  • an impredicative, proof irrelevant type `Prop` of propositions.
  • a non-cumulative hierarchy of universes `Type 1`, `Type 2`, … above `Prop`
  • universe polymorphism
  • inductively defined types

• Features

  • the kernel is constructive
  • smooth support for classical logic
  • support for Homotopy Type Theory (HoTT)

Reasoning about abstractions

• At CMU, Jeremy Avigad, Floris van Doorn and Jakob von Raumer are formalizing Category theory and Homotopy type theory using Lean.

• Why this relevant?

  • It is stressing all lean major components.
  • If we can do it, then we can do anything.
  • Test if we can reason about higher-level abstractions.
  • In CS, we also want to reason about higher-level abstractions.

Constructive and classical logic

• Almost everything we do is constructive, but we want to support classical users

smoothly.

inductive decidable [class] (p : Prop) : Type :=
inl : p  → decidable p,
inr : ¬p → decidable p

• `decidable` is the type class of decidable propositions.
• The excluded middle is a theorem for decidable propositions.

theorem em (p : Prop) [H : decidable p] : p ∨ ¬p :=
induction_on H (assume Hp, or.inl Hp) (assume Hnp, or.inr Hnp)

• The `[…]` instructs lean that `H : decidable p` is an implicit argument,

and it should be synthesized automatically using type-class instantiation

• We have populated the lean standard library with many decidability results.

Example: the conjunction of two decidable propositions is decidable

variables p q : Prop
definition and_decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ∧ q) :=
rec_on Hp
  (assume Hp  : p, rec_on Hq
    (assume Hq  : q,  inl (and.intro Hp Hq))
    (assume Hnq : ¬q, inr (and.not_right p Hnq)))
  (assume Hnp : ¬p, inr (and.not_left q Hnp))

definition decidable_eq (A : Type) := Π (a b : A), decidable (a = b)

protected definition nat.has_decidable_eq [instance] : decidable_eq ℕ :=
take n m : ℕ,
...

• We define `if-then-else` expressions as

definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A :=
decidable.rec_on H (assume Hc,  t) (assume Hnc, e)

notation `if` c `then` t:45 `else` e:45 := ite c t e

Lean will only allow us to use `if-then-else` for decidable propositions. By default, it will try to prove decidability using type-class resolution. If we write

import standard
open nat decidable

variables a b : nat
check if a = b ∧ a > 0 then a else b

Lean automatically synthesizes the implicit argument `H : decidable c`.

``` (and_decidable (nat.has_decidable_eq a b) (ge_decidable a (succ 0))) ```

• When we import the classical axioms, then we can prove that all propositions are decidable.

theorem prop_decidable [instance] (a : Prop) : decidable a

Moreover, we can write arbitrary `if-then-else` expressions.

if riemman_hypothesis then t else e

Lean interfaces

…

Future work

• Definitional package: convert "recursive equations" into recursors.

The user wants to write

append : list A → list A → list A
append nil      t = t
append (x :: l) t = x :: (append l t)

instead of

definition append (s t : list A) : list A :=
rec_on s
  t
  (λx l u, x::u)

• Automation

  • Simplifier
  • SMT-like engines
  • Arithmetic

Future work (cont.)

• Next semester, we will have a course on theorem proving based on Lean at CMU
• Tutorial at CADE

Example

import algebra.category
open eq.ops category functor natural_transformation

variables {ob₁ ob₂ : Type} {C : category ob₁} {D : category ob₂} {F G H : C ⇒ D}

-- infix `↣`:20 := hom

-- F G H are functors
-- η θ are natural transformations

-- A natural transformation provides a way of transforming one functor
-- into another while respecting the internal structure.
-- A natural transformation can be considered to be a "morphism of functors".

-- http://en.wikipedia.org/wiki/Natural_transformation

definition nt_compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
natural_transformation.mk
  (take a, η a ∘ θ a)
  (take a b f, calc
    H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : !assoc
                  ... = (η b ∘ G f) ∘ θ a : {naturality η f}
                  ... = η b ∘ (G f ∘ θ a) : !assoc⁻¹
                  ... = η b ∘ (θ b ∘ F f) : {naturality θ f} -- {@naturality _ _ _ _ _ _ θ _ _ f}
                  ... = (η b ∘ θ b) ∘ F f : !assoc)

-- check nt_compose
-- check @nt_compose
exit
set_option pp.implicit true
set_option pp.full_names true
set_option pp.notation false
set_option pp.coercions true
-- set_option pp.universes true
print definition nt_compose