From f6a6894d1f5f7f80e076489c2dbf5a6a98954181 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Oct 2014 15:10:17 -0700
Subject: [PATCH] doc(intro): basic slides

---
 doc/intro.org | 206 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 206 insertions(+)
 create mode 100644 doc/intro.org

diff --git a/doc/intro.org b/doc/intro.org
new file mode 100644
index 000000000..ba84758c2
--- /dev/null
+++ b/doc/intro.org
@@ -0,0 +1,206 @@
+* 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.
+
+#+BEGIN_SRC lean
+inductive decidable [class] (p : Prop) : Type :=
+inl : p  → decidable p,
+inr : ¬p → decidable p
+#+END_SRC
+
+- `decidable` is the _type class_ of decidable propositions.
+
+- The excluded middle is a theorem for decidable propositions.
+
+#+BEGIN_SRC lean
+theorem em (p : Prop) [H : decidable p] : p ∨ ¬p :=
+induction_on H (assume Hp, or.inl Hp) (assume Hnp, or.inr Hnp)
+#+END_SRC
+
+- 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
+#+BEGIN_SRC lean
+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))
+#+END_SRC
+
+#+BEGIN_SRC lean
+definition decidable_eq (A : Type) := Π (a b : A), decidable (a = b)
+
+protected definition nat.has_decidable_eq [instance] : decidable_eq ℕ :=
+take n m : ℕ,
+...
+#+END_SRC
+
+- We define `if-then-else` expressions as
+
+#+BEGIN_SRC lean
+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
+#+END_SRC
+
+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
+
+#+BEGIN_SRC lean
+import standard
+open nat decidable
+
+variables a b : nat
+check if a = b ∧ a > 0 then a else b
+#+END_SRC
+
+Lean automatically synthesizes the implicit argument `H : decidable c`.
+
+```
+(and_decidable (nat.has_decidable_eq a b) (ge_decidable a (succ 0)))
+```
+
+# Note: we can see this argument by setting options
+# set_option pp.notation false
+# set_option pp.implicit true
+
+- When we import the classical axioms, then we can prove that *all propositions are decidable*.
+#+BEGIN_SRC lean
+theorem prop_decidable [instance] (a : Prop) : decidable a
+#+END_SRC
+
+Moreover, we can write arbitrary `if-then-else` expressions.
+#+BEGIN_SRC lean
+if riemman_hypothesis then t else e
+#+END_SRC
+
+* Lean interfaces
+...
+
+* Future work
+
+- Definitional package: convert "recursive equations" into recursors.
+The user wants to write
+
+#+BEGIN_SRC lean
+append : list A → list A → list A
+append nil      t = t
+append (x :: l) t = x :: (append l t)
+#+END_SRC
+
+instead of
+
+#+BEGIN_SRC lean
+definition append (s t : list A) : list A :=
+rec_on s
+  t
+  (λx l u, x::u)
+#+END_SRC
+
+- 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
+#+BEGIN_SRC lean
+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
+#+END_SRC