Lean Prover Checksheet

• 定义变量

def b: Bool := true
def n: Nat := 1
def prod: Nat × Nat := (1, 2) 

• 检查变量类型

#check b  -- true : Bool
#check prod -- Nat × Nat
#check Bool -- Type
#check Type -- Type 1
#check Type 1 -- Type 2
#check Prod -- Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)

• 检查值

#eval 1 + 2 -- 3

• 定义多态常量（polymorphic constants)

universe u
def F1 (α : Type u) : Type u := Prod α α
def F2.{u} (α : Type u) : Type u := Prod α α

• 函数
  • 定义匿名函数

  #check fun (x : Nat) => x + 5 -- Nat → Nat 
  #check λ (x : Nat) => x + 5   -- λ and fun mean the same thing
  #check fun x : Nat => x + 5   -- Nat inferred 
  #check λ x : Nat => x + 5     -- Nat inferred
  #check fun (α β γ : Type) (u : β → γ) (v : α → β) (x : α) => u (v x)

  • 调用匿名函数

  #eval (λ x : Nat => x + 5) 10   -- 15

  • 定义具名函数

  def double : (Nat -> Nat) := fun x => x + x
  def double (x : Nat) := x + x

• 局部定义

def t (x: Nat) : Nat := let y := x + x; y + y

• variable 和 section

section useful 
	variable (α β γ : Type)
	variable (g : β → γ) (f : α → β) (h : α → α)
	variable (x : α) 
	def compose := g (f x) 
	def doTwice := h (h x) 
	def doThrice := h (h (h x)) 
end useful

• Namespace

namespace Foo 
	def a : Nat := 5 
	def f (x : Nat) : Nat := x + 7 
	def fa : Nat := f a 
	def ffa : Nat := f (f a) 
	#check a 
	#check f 
	#check fa
	#check ffa 
	#check Foo.fa 
end Foo 
-- #check a -- error 
-- #check f -- error 
#check Foo.a 
#check Foo.f 
#check Foo.fa 
#check Foo.ffa 
open Foo 
#check a 
#check f 
#check fa 
#check Foo.fa

• 嵌套namespace

namespace Foo 
	def a : Nat := 5
	def f (x : Nat) : Nat := x + 7 
	def fa : Nat := f a 
	namespace Bar 
		def ffa : Nat := f (f a) 
		#check fa 
		#check ffa 
	end Bar 
	#check fa 
	#check Bar.ffa 
end Foo 
#check Foo.fa 
#check Foo.Bar.ffa 
open Foo 
#check fa 
#check Bar.ffa

• namespace可多次打开

namespace Foo
  def a : Nat := 5
  def f (x : Nat) : Nat := x + 7
  def fa : Nat := f a
end Foo
 
#check Foo.a
#check Foo.f
 
namespace Foo
  def ffa : Nat := f (f a)
end Foo

• 隐式参数

def ident.{u} {α : Type u} (a : α) := a
#check ident -- ident.{u} {α : Type u} (a : α) : α
#check ident 1 -- Nat
#check @ident  -- @ident : {α : Type u_1} -> α -> α
#eval @ident Nat 1 -- 1