Home | Blog | Wiki | About

General

• Type check current file: C-c C-l
• Math library of lean: mathlib (like mathcomp of coq)

Misc

#check Nat

mathlib

• [CommRing R]: mention that R is a commutative ring

Lean3

namespace <namespace-name>
open <namespace-name>

Coq analogues

• Check: #check
• Compute: #reduce (done by trusted kernel. Less efficient.)
• Eval: #eval (computation. Non-trusted? More efficient.)
• Admitted: sorry
• Proof-Qed: begin-end

ℕ vs ℕ+

• ℕ is ℕ₀.
• ℕ+ is ℕ₁.

#check (0:ℕ)
#check (1:ℕ+)

Random snippets

• Type*: I guess it's like the Top type. Type of all types.
• fact: insert a fact. ie, info. Not factorial.

#reduce 1+2
-- 3
#check 1+2
-- 1 + 2 : ℕ

-----------------------------------

constant p: ℕ.
#check p.prime
│ nat.prime p : Prop

def x:ℕ := 5
#reduce x.prime
│ irreducible 5

-----------------------------------

#print or
│ inductive or : Prop → Prop → Prop
│ constructors:
│ or.inl : ∀ {a b : Prop}, a → a ∨ b
│ or.inr : ∀ {a b : Prop}, b → a ∨ b

#print and.elim
│ theorem and.elim : ∀ {a b c : Prop}, a ∧ b → (a → b → c) → c :=
│ λ {a b c : Prop} (h₁ : a ∧ b) (h₂ : a → b → c), and.rec h₂ h₁


theorem or_intro_l (p q: Prop) : p → p ∨ q :=
show p ∨ q, from or.inl

Commas in proof script

From https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=1&level=2

The comma tells Lean "I've finished writing this tactic now, please process it." Lean ignores newlines, but pays great attention to commas.

Comment

• Multi-line: /-- comment --/
• Single-line: -- comment

Todo

• How to search for existing lemmas? Like Coq's Search.
• Notations? And Locate equivalent?
  • Custom entries?
• Show Proof
• print proofs