Lean Prover

마지막 수정 시각: 2020-10-26 22:03:12

lean prover를 공부해보자

https://leanprover.github.io/theorem_proving_in_lean/index.html 읽고 정리한 것.

* 그냥 읽으면서 생각나는 것들 주저리주저리 쓴 거라 제 3자가 봤을 때 별로 도움이 될 정리본은 아닙니다

Dependent Type Theory

Dependent type theory는 아주 강력하고 표현력이 뛰어난 언어다. 복잡한 수학적 assertion, 하드웨어 / 소프트웨어 명세, 그리고 이 두가지 모두에 대한 자연스럽고 일관된 방법의 추론을 가능하게 해준다. Lean은 Calculus of Constructions라고 알려진 dependent type theory에 기반하고 있다.

Simple Type Theory

'Type Theory'에서는 모든 표현식이 타입을 가진다. Lean에서 object를 선언하고 타입을 어떻게 확인하는지 몇 가지 예시를 통해 알아보자.

/- declare some constants -/

constant m : nat        -- m is a natural number
constant n : nat
constants b1 b2 : bool  -- declare two constants at once

/- check their types -/

#check m            -- output: nat
#check n
#check n + 0        -- nat
#check m * (n + 0)  -- nat
#check b1           -- bool
#check b1 && b2     -- "&&" is boolean and
#check b1 || b2     -- boolean or
#check tt           -- boolean "true"

tt가 true고 ff가 false다. 이건 또 처음 보는 스타일. /- -/ 가 주석. -- 가 한줄 주석.

constant 커맨드는 새로운 심볼을 정의한다. : 뒤에 타입을 명시. nat는 정수 타입. #check 커맨드를 통해 lean에 해당 표현식의 타입이 뭔지 물어볼 수 있다. lean에서 시스템에 뭔가 정보를얻어오기 위한 목적의 커맨드는 대개 #으로 시작한다.

새로운 object를 이런 식으로 정의하는 건 뭔가 시험해보기 위한 목적으로는 좋은데, 궁극적으로는 불필요한 작업이다. lean은 foundational system이기 때문에 필요한 모든 수학적인 object를 정의하는 강력한 방법을 제공해준다. 그래서 foundational system이 무엇인가?? 검색해봐도 딱히 안 나오는데 아무튼 저거보다 좋은 방법이 있다 정도로 생각하면 될 것 같다. 나중에 자세히 설명해준다고 한다.

Simple type theory는 하나의 타입으로부터 새로운 타입을 만들어낼 수 있다는 점으로부터 강력한 파워를 얻게 된다. 예를 들어, a와 b가 타입이면 a→b 는 a에서 b로 가는 함수를, a x b는 둘의 cartesian product(a의 모든 원소와 b의 모든 원소에 대해 그 둘의 ordered pair로 구성된 타입)를 나타낸다.

constants m n : nat

constant f : nat → nat           -- type the arrow as "\to" or "\r"
constant f' : nat -> nat         -- alternative ASCII notation
constant f'' : ℕ → ℕ             -- alternative notation for nat
constant p : nat × nat           -- type the product as "\times"
constant q : prod nat nat        -- alternative notation
constant g : nat → nat → nat
constant g' : nat → (nat → nat)  -- has the same type as g!
constant h : nat × nat → nat

constant F : (nat → nat) → nat   -- a "functional"

#check f               -- ℕ → ℕ
#check f n             -- ℕ
#check g m n           -- ℕ
#check g m             -- ℕ → ℕ
#check (m, n)          -- ℕ × ℕ
#check p.1             -- ℕ
#check p.2             -- ℕ
#check (m, n).1        -- ℕ
#check (p.1, n)        -- ℕ × ℕ
#check F f             -- ℕ

예시들. 함수의 경우 하스켈이랑 비슷해서 이해하기 어렵지 않다. F f 같은 거 재밌다. 하스켈에서 고차함수의 부분 적용을 생각해보면 되는 듯. 화살표 같은 기호 표시가 latex처럼 \to 같은 형태로 쓰는 방법이 있고 ascii 문자로 → 로 하는 방법이 있고 다양하다. 몇 번 써보면서 손에 익어야 할 것 같다

pair가 곧 cartesian product고 p.1 , p.2 같은 형태로 각 요소에 대응되는 타입을 갖고 올 수 있다. 맨날 값으로만 생각해서 몰랐는데 생각해보니 pair가 그 타입에 속하는 모든 원소를 갖고 생각하면 두 타입의 cartesian product랑 같다. 그랬군

Types as Objects

simple type theory를 확장한 dependent type theory에서는 nat, bool 과 같은 타입 그 자체에 대해서도 타입을 붙인다. 아래 예시를 보자

#check nat               -- Type
#check bool              -- Type
#check nat → bool        -- Type
#check nat × bool        -- Type
#check nat → nat         -- ...
#check nat × nat → nat
#check nat → nat → nat
#check nat → (nat → nat)
#check nat → nat → bool
#check (nat → nat) → nat

모든 표현식이 다 Type 타입을 가지는 것으로 나온다. 아래와 같이 타입에 대한 표현식을 선언해서 쓰는 경우도 보자.

constants α β : Type
constant F : Type → Type
constant G : Type → Type → Type

#check α        -- Type
#check F α      -- Type
#check F nat    -- Type
#check G α      -- Type → Type
#check G α β    -- Type
#check G α nat  -- Type

타입에 대한 함수라는 점을 제외하고 보면 별로 다를 바는 없다. 타입을 받아 다른 타입을 만들어내는 함수? 타입간의 사상? 그런 느낌으로 이해하면 위의 예시들이랑 거의 같은 느낌. 위에서 이미 prod 라는 예시(두 type의 cartesian product)가 나왔었다,

constants α β : Type

#check prod α β       -- Type
#check prod nat nat   -- Type

두 타입의 cartesian product는 새로운 타입을 만들어내니까 위의 정의에 딱 맞다. Type -> Type -> Type 인거지

또 다른 예시로는 list가 있다.

constant α : Type

#check list α    -- Type
#check list nat  -- Type

이것도 "어떤 타입의 리스트" 가 Type이니까 리스트는 Type -> Type 이 된다. (어떤 타입)을 받아서 → (그 타입의 리스트) 를 만들어내는 함수인 것

그렇다면 Type 은 또 무슨 타입을 가지는가?

#check Type     -- Type 1
#check Type 1   -- Type 2
#check Type 2   -- Type 3
#check Type 3   -- Type 4
#check Type 4   -- Type 5

그렇다고 한다. Type은 무한한 단계가 있다. 하스켈에서 kind 같은 느낌인 것 같다. 그냥 Type은 Type 0 이랑 같은데, 작은 / 평범한 타입 같은 느낌. Type 1은 타입의 타입으로 구성된 타입, Type 2는 다시 그 타입의 타입들로 구성된 타입... 뭐 그런 느낌의 위계질서가 있다

또다른 타입으로 Prop가 있다.

#check Prop -- Type

근데 다음 챕터에 설명할거래

몇몇 연산들은 타입에 대해 다형적이길 원할 수 있다. list a 가 모든 타입 a 에 대해 동작하는게 낫잖아. Type 0 에서만 동작하는 거 말고

그래서 list는 다음과 같은 타입을 가진다

#check list    -- Type u_1 → Type u_1

u_1이 타입 레벨에 대한 변수인 것.

#check prod    -- Type u_1 → Type u_2 → Type (max u_1 u_2)

prod는 이렇다. 이 경우 둘 중 큰 타입을 따라 간다. 이건 왤까? 흠..

universe u
constant α : Type u
#check α

다형적인 constant나 variable을 정의하기 위해선 위와 같은 노테이션을 쓰면 된다. universe 라는 커맨드로 타입 계층을 표현.

Function Abstraction and Evaluation

a 타입의 변수 x : a 가 있다고 하자. 그리고 이 변수를 이용한 표현식 t : b 가 있다고 하자. fun x : a, t 는 a -> b 타입의 object를 만들어낸다. 임의의 x 를 x에 의존적인 표현식 t 에 대응시키는 함수처럼 생각하면 됨. 아래 예시를 보자.

#check fun x : nat, x + 5
#check λ x : nat, x + 5

x를 받아 x + 5 를 리턴하는 함수처럼 생각할 수 있다. 이 함수의 타입은 nat -> nat 로 생각할 수 있겠지

constants α β  : Type
constants a1 a2 : α
constants b1 b2 : β

constant f : α → α
constant g : α → β
constant h : α → β → α
constant p : α → α → bool

#check fun x : α, f x                      -- α → α
#check λ x : α, f x                        -- α → α
#check λ x : α, f (f x)                    -- α → α
#check λ x : α, h x b1                     -- α → α
#check λ y : β, h a1 y                     -- β → α
#check λ x : α, p (f (f x)) (h (f a1) b2)  -- α → bool
#check λ x : α, λ y : β, h (f x) y         -- α → β → α
#check λ (x : α) (y : β), h (f x) y        -- α → β → α
#check λ x y, h (f x) y                    -- α → β → α

좀 더 다양한 예시들. 뭐 차근차근 읽어보면 다 그냥 위에서 적은 규칙이랑 같다. 두 개의 인자를 쓰는 경우 fun x : α, fun y : β, h (f x) y 뭐 이런 식으로 , 로 연속한다는 점. 생각해보면 당연한데 , 기준으로 짤라서 오른쪽부터 보면 그냥 함수 타입의 연쇄라서(currying) 그냥 그렇게 된다. 우측 결합이니깐. 근데 그렇게 안쓰고 그냥 두개 써줘도 잘 동작하게 되어 있는 듯. 타입 추론도 잘 된다 ( 마지막 예제에서 x y는 타입 없이 선언하고 h (f x) y 표현식을 썼지만 h와 f로부터 x , y의 타입이 잘 추론되어 나옴)

constants α β γ : Type
constant f : α → β
constant g : β → γ
constant b : β

#check λ x : α, x        -- α → α
#check λ x : α, b        -- α → β
#check λ x : α, g (f x)  -- α → γ
#check λ x, g (f x)

또 다른 예시. 타입 추론 잘 해주기 때문에 굳이 안 적어도 잘 동작한다(마지막 거).

#check λ (α β : Type) (b : β) (x : α), x
#check λ (α β γ : Type) (g : β → γ) (f : α → β) (x : α), g (f x)

타입에 대한 abstract도 가능하다. 마지막 예시에서 (x : α) 의 x 는 'bound variable'인데, 이건 단순한 placeholder의 역할만 한다. 즉, 이 타입의 스코프는 표현식 t 의 범위를 벗어나지 않는다. 만약 λ (b : β) (x : α), x 이런 표현식이 있다면 여기서 constant b는 아무런 역할도 하지 않는다. 이 표현식은 bound variable만 다른 이름으로 바꾼 λ (u : β) (z : α), z 이랑 alpha equivalent하다고 말한다(같다고 취급함). lean은 이런 equivalence를 알아낸다.

constants α β γ : Type
constant f : α → β
constant g : β → γ
constant h : α → α
constants (a : α) (b : β)

#reduce (λ x : α, x) a                -- a
#reduce (λ x : α, b) a                -- b
#reduce (λ x : α, b) (h a)            -- b
#reduce (λ x : α, g (f x)) a          -- g (f a)

#reduce (λ (v : β → γ) (u : α → β) x, v (u x)) g f a   -- g (f a)

#reduce (λ (Q R S : Type) (v : R → S) (u : Q → R) (x : Q),
       v (u x)) α β γ g f a        -- g (f a)

슬슬 복잡해. t : α → β 에 term s : α 를 적용(apply)하는 걸 t s : β 와 같은 표현식으로 나타낸다. 하스켈에서 함수 호출이랑 같다. 함수 부분을 괄호로 감싸고, 뒤에 인자를 공백으로 구분해서 나열하면 됨. 위 예시를 보자

#reduce 는 주어진 표현식을 normal form으로 reducing한 결과를 보여준다. 그러니까 어떤 x 에 대한 표현식 t 와 t s 가 있을 때 여기서 변수 x를 s 로 대체(substitute)하는 과정을 통해 단순하게 만드는 과정을 반복하는 것. 이를 beta reduction 이라고 하고, beta reduction 된 결과와 원래의 표현식을 beta equivalent 하다고 한다. 그리고 #reduce 는 다른 형태의 리덕션도 수행해준다.

constants m n : nat
constant b : bool

#print "reducing pairs"
#reduce (m, n).1        -- m
#reduce (m, n).2        -- n

#print "reducing boolean expressions"
#reduce tt && ff        -- ff
#reduce ff && b         -- ff
#reduce b && ff         -- bool.rec ff ff b

#print "reducing arithmetic expressions"
#reduce n + 0           -- n
#reduce n + 2           -- nat.succ (nat.succ n)
#reduce 2 + 3           -- 5

요건 그냥 인터프리터에서 명령하듯이 동작하는데 이 리덕션이 뭔지는 더 이후 챕터에서 설명해준다고 함

dependent type theory의 아주 중요한 feature: 모든 term은 computational behaviour를 갖고 있으며, reduction 혹은 normalization의 개념을 제공한다는 것. 같은 value로 reduce 되는 두 term은 definitionally equal 하다고 부른다. 이건 내장된 논리 프레임워크 상에서 같은 것으로 취급된다.

Introducing Definitions

define을 써보자

def foo : (ℕ → ℕ) → ℕ := λ f, f 0

#check foo    -- (ℕ → ℕ) → ℕ
#print foo    -- λ (f : ℕ → ℕ), f 0

타입 추론이 충분히 가능한 경우 타입 생략 가능

def foo' := λ f : ℕ → ℕ, f 0

다른 형태로 선언도 가능하다.

def double (x : ℕ) : ℕ := x + x
#print double
#check double 3
#reduce double 3    -- 6

def square (x : ℕ) := x * x
#print square
#check square 3
#reduce square 3    -- 9

def do_twice (f : ℕ → ℕ) (x : ℕ) : ℕ := f (f x)

#reduce do_twice double 2    -- 8

-- 아래와 동치
def double : ℕ → ℕ := λ x, x + x
def square : ℕ → ℕ := λ x, x * x
def do_twice : (ℕ → ℕ) → ℕ → ℕ := λ f x, f (f x)

연습 문제 하라고 한 것 짜보기.

• do_twice와 double을 이용해 입력을 8배, 16배 하는 함수 정의하기

def triple := do_twice double
def quadruple := do_twice square

• argument를 두 번 적용하는 함수 정의하기

def Do_twice : ((ℕ -> ℕ) -> (ℕ -> ℕ)) -> (ℕ -> ℕ) -> (ℕ -> ℕ) := λ f g, f (f g)

• curry, uncurry 구현하기

def curry (α β χ : Type) (f: α × β → χ) : α → β → χ := λ x y, f (x, y)
def uncurry (α β χ : Type) (f: α → β → χ) : α × β → χ := λ x, f x.1 x.2

쉽다 쉬워~

Local Definitions

#check let y := 2 + 2 in y * y   -- ℕ
#reduce let y := 2 + 2 in y * y   -- 16

def t (x : ℕ) : ℕ :=
let y := x + x in y * y

#reduce t 2   -- 16

하스켈에서 let ~ in 이랑 별반 다를 바 없다. 전역이 아니라 내부에서만 쓰이는 지역적 정의 만들기

def foo := let a := nat  in λ x : a, x + 2

/-
def bar := (λ a, λ x : a, x + 2) nat
-/

위는 되는데 아래는 왜 안되는가? 위는 a가 그냥 nat인데 아래는 임의의 어떤 a 타입에 대한 함수(제네릭)이 되어야하기 때문에 +2가 항상 가능하리란 보장이 없다. 그래서 let ~ in 표현식이 항상 아래 표현식이랑 동등한 건 아님. let ~ in 은 특정 대상의 축약어라는 느낌이 더 강함

Variables and Sections

variables를 이용해서 중복을 피할 수 있다

variables (α β γ : Type)
variables (g : β → γ) (f : α → β) (h : α → α)
variable x : α

def compose := g (f x)
def do_twice := h (h x)
def do_thrice := h (h (h x))

#print compose
#print do_twice
#print do_thrice

범위 한정을 위해 section을 사용 가능

section useful
  variables (α β γ : Type)
  variables (g : β → γ) (f : α → β) (h : α → α)
  variable x : α

  def compose := g (f x)
  def do_twice := h (h x)
  def do_thrice := h (h (h x))
end useful

Namespaces

namespace foo
  def a : ℕ := 5
  def f (x : ℕ) : ℕ := x + 7

  def fa : ℕ := f a
  def ffa : ℕ := f (f a)

  #print "inside foo"

  #check a
  #check f
  #check fa
  #check ffa
  #check foo.fa
end foo

#print "outside the namespace"

-- #check a  -- error
-- #check f  -- error
#check foo.a
#check foo.f
#check foo.fa
#check foo.ffa

open foo

#print "opened foo"

#check a
#check f
#check fa
#check foo.fa

다른 언어의 namespace랑 별반 다를 바 없다. open은 using 같은거. nested도 된다. 한번 닫고 다시 열어서 덧붙이는것도 가능

namespace foo
  def a : ℕ := 5
  def f (x : ℕ) : ℕ := x + 7

  def fa : ℕ := f a
end foo

#check foo.a
#check foo.f

namespace foo
  def ffa : ℕ := f (f a)
end foo

Dependent Types

타입이 그 인자에 의존적이어서 Dependent Type. list라거나 길이가 N인 타입 a의 벡터라거나.

리스트의 맨 앞에 원소를 추가하는 cons 함수를 생각해보자. 이 함수의 타입은 뭐가 되어야 할까? 얘는 list a에서 a에 dependent하다. 즉, a 타입을 assuming해야할 필요가 있다. 이런걸 pi type 혹은 dependent function type이라고 부름. a : Type이 주어지고 b : a → Type이 주어지면 b를 a에 대한 타입의 집합으로 생각할 수 있다. 이런 경우, Π x : α, β x 는 임의의 a 에 대해 a : α, f a 가 β 의 원소가 되는 성질을 가진 함수의 타입을 나타낸다.

namespace hidden

universe u

constant list   : Type u → Type u

constant cons   : Π α : Type u, α → list α → list α
constant nil    : Π α : Type u, list α
constant head   : Π α : Type u, list α → α
constant tail   : Π α : Type u, list α → list α
constant append : Π α : Type u, list α → list α → list α

end hidden

이건 그냥 설명용이고 이미 이건 lean 라이브러리에 있다

open list

#check list     -- Type u_1 → Type u_1

#check @cons    -- Π {α : Type u_1}, α → list α → list α
#check @nil     -- Π {α : Type u_1}, list α
#check @head    -- Π {α : Type u_1} [_inst_1 : inhabited α], list α → α
#check @tail    -- Π {α : Type u_1}, list α → list α
#check @append  -- Π {α : Type u_1}, list α → list α → list α

@는 뭐고 {} 랑 []는 또 무엇인가? 좀 이따 설명한다고 함. head의 경우 반드시 원소가 하나 이상 있어야 하며 / 그게 아닐 경우 기본 원소를 준다. 이거 관련은 챕터 10에서 설명

universe u
constant vec : Type u → ℕ → Type u

namespace vec
  constant empty : Π α : Type u, vec α 0
  constant cons :
    Π (α : Type u) (n : ℕ), α → vec α n → vec α (n + 1)
  constant append :
    Π (α : Type u) (n m : ℕ),  vec α m → vec α n → vec α (n + m)
end vec

벡터 구현. 이것도 비슷. 사이즈가 같이 붙는다는 것 외에는 별로 다른게 없음.

Sigma type이라는 것도 있다. Σ x : α, β x 라고 쓰고, dependent products라고도 알려져 있음. 이건 a : α 이고 b : β a 일 때 sigma.mk a b 페어 타입을 가리킴. 그냥 페어인데, 두 번째 원소가 첫번째 원소의 타입에 의존적인 형태의 타입을 가진 페어 말하는 것.

variable α : Type
variable β : α → Type
variable a : α
variable b : β a

#check sigma.mk a b      -- Σ (a : α), β a
#check (sigma.mk a b).1  -- α
#check (sigma.mk a b).2  -- β (sigma.fst (sigma.mk a b))

#reduce  (sigma.mk a b).1  -- a
#reduce  (sigma.mk a b).2  -- b

Implicit Arguments

위에서 정의한 list 써서 새로운 리스트들을 구성할 수 있다.

open hidden.list

variable  α : Type
variable  a : α
variables l1 l2 : list α

#check cons α a (nil α)
#check append α (cons α a (nil α)) l1
#check append α (append α (cons α a (nil α)) l1) l2

이 constructor들은 타입에 대해 다형적(polymophic)이기 때문에 타입 α 을 반복적으로 넣어줘야한다. 추론 가능해서 자동으로 넣을 수 있는 경우 underscore(_)로 쓰고 자동으로 채워넣으라고 할 수 있다. 이걸 implicit aruments라고 함

#check cons _ a (nil _)
#check append _ (cons _ a (nil _)) l1
#check append _ (append _ (cons _ a (nil _)) l1) l2

당연히 이것도 번거롭다.. 사용된 문맥으로부터 인자가 뭔지를 충분히 추론할 수 있는 경우, 그걸 아예 비워놓는것도 허용한다. 이 경우, argument를 중괄호안에 넣어줘야 한다.

namespace list
  constant cons   : Π {α : Type u}, α → list α → list α
  constant nil    : Π {α : Type u}, list α
  constant append : Π {α : Type u}, list α → list α → list α
end list

open hidden.list

variable  α : Type
variable  a : α
variables l1 l2 : list α

#check cons a nil
#check append (cons a nil) l1
#check append (append (cons a nil) l1) l2

좋다. 근데 왜 중괄호를 써야만 이런 생략이 가능하게 한걸까? 뭔가 설계상의 이유가 있을 것 같은데 잘 모르겠음

함수 정의에서도 마찬가지의 문법을 사용할 수 있다.

universe u
def ident {α : Type u} (x : α) := x

variables α β : Type u
variables (a : α) (b : β)

#check ident      -- ?M_1 → ?M_1
#check ident a    -- α
#check ident b    -- β

?M_1 이라는 타입은 무엇인가.. 모르겠다

variable 커맨드로 선언된 애들도 implicit하게 사용 가능하다.

universe u

section
  variable {α : Type u}
  variable x : α
  def ident := x
end

variables α β : Type u
variables (a : α) (b : β)

#check ident
#check ident a
#check ident b

lean은 굉장히 복잡한 과정을 통해 implicit arguments들을 구체화한다. 이러한 과정을 elaboration이라고 부름. 가끔씩 정보가 부족해서 특정 표현식의 타입을 정확히 알아낼 수 없는 경우가 있다. 리스트에서 nil같은 것. 이럴 땐 (e : T) 같은 구문을 이용해 표현식의 타입을 명시해줄 수 있다.

#check list.nil             -- list ?M1
#check id                   -- ?M1 → ?M1

#check (list.nil : list ℕ)  -- list ℕ
#check (id : ℕ → ℕ)         -- ℕ → ℕ

수 타입들은 overloaded되어있긴 한데, 추론 불가능한 경우에는 기본적으로 자연수로 취급한다.

#check 2            -- ℕ
#check (2 : ℕ)      -- ℕ
#check (2 : ℤ)      -- ℤ

implicit하게 만들었는데 뭔가 모종의 이유로 explicit하게 타입을 주고 싶은 경우 @를 붙여서 쓴다.

#check @id        -- Π {α : Type u_1}, α → α
#check @id α      -- α → α
#check @id β      -- β → β
#check @id α a    -- α
#check @id β b    -- β

이제 알았는데 brace는 생략 가능이 아니라 반드시 생략(무조건 infer함)을 뜻하는거였다. 그래서 brace쓰면 명시하는 것 자체가 불가능해짐. 명시하려면 명시한다고 하기 위해 @를 쓰는거고. 하긴 이게 저거 타입 인자 넘기는 건지 그냥 뒤에 다른 argument 넘기는건지 알 수가 없어서 저런 문법을 가지나 보다

Exercises

1,2는 위에서 이미 풀었다(Do_Twice랑 curry, uncurry)

• 위에서 vec a n을 길이 n인 타입 a의 vector로 썼다. 같은 길이의 두 자연수 vector를 더하는 vec_add constant를 정의하라. 그리고 argument를 거꾸로 뒤집는 vec_reverse constant도 정의하라. implicit argument를 써서 추론 가능한 건 추론할 수 있게 해라. variables을 정의하고 정의한 constant를 포함하는 표현식들을 이용해서 제대로 짰는지 확인해봐라.

namespace test
  universe u

  constant vec : Type u → ℕ → Type u

  constant empty : Π {α : Type u}, vec α 0
  constant cons : Π {α : Type u} {n : ℕ}, α → vec α n → vec α (n + 1)
  constant append : Π {α : Type u} {n m : ℕ}, vec α n → vec α m → vec α (n + m)

  constant vec_add : Π {n : ℕ}, vec ℕ n → vec ℕ n → vec ℕ n
  constant vec_reverse : Π {α : Type u} {n : ℕ}, vec α n → vec α n

  variable v1 : vec ℕ 3
  variable v2 : vec ℕ 3
  variable v3 : vec ℕ 4
  variables α β : Type
  variable va : vec α 10
  variable va2 : vec α 3
  variable vb : vec β 10

  -- OK
  #check vec_add v1 v2 -- vec ℕ 3
  #check vec_reverse v1 -- vec ℕ 3
  #check vec_reverse va -- vec α 10

  -- Error
  #check vec_add va va
  #check vec_add v1 va2
  #check vec_add v1 v3

end test

타입만 하래.. 너무 시시해서 죽고 싶어졌다

• 비슷하게, matrix constat를 정의해서 matrix a m n이 해당 타입의 m by n 크기 행렬을 표현하게 해봐라. 행렬 덧셈이나 곱셈을 정의하는 constant도 만들어봐라. vec을 써서 matrix와 vec의 곱도 구현해봐라. 그리고 잘 짰는지 확인해봐라

namespace test
  universe u

  constant vec : Type u -> ℕ -> Type u
  constant mat : Type u → ℕ → ℕ → Type u
  constant mat_add : Π {α : Type u} {n m : ℕ}, mat α n m → mat α n m → mat α n m
  constant mat_mul : Π {α : Type u} {n m k : ℕ}, mat α n k -> mat α k m -> mat α n m
  constant mat_vec_mul : Π {α : Type u} {n m : ℕ}, mat α n m -> vec α m -> vec α n

  variables α β: Type
  variable m1 : mat α 3 5
  variable m2 : mat α 5 2
  variable m3 : mat α 3 5
  variable m4 : mat β 5 2
  variable m5 : mat β 3 5
  variable v1 : vec α 5
  variable v2 : vec β 5

  -- OK
  #check mat_mul m1 m2

  #check mat_add m1 m3

  #check mat_vec_mul m1 v1 
  #check mat_mul m5 m4

  -- Error
  #check mat_mul m1 m4
  #check mat_mul m2 m1

  #check mat_add m1 m2
  #check mat_add m1 m5
  #check mat_add m1 m4

  #check mat_vec_mul m1 v2
  #check mat_vec_mul m2 v1

end test

Propositions and Proofs

dependent type theory에서 수학적 assertion과 증명을 어케 할 수 있는지 알아보자

Propositions as Types

Prop 타입은 명제를 나타낸다.

constant and : Prop → Prop → Prop
constant or : Prop → Prop → Prop
constant not : Prop → Prop
constant implies : Prop → Prop → Prop

variables p q r : Prop
#check and p q                      -- Prop
#check or (and p q) r               -- Prop
#check implies (and p q) (and q p)  -- Prop

p: Prop 에 대해 Proof p 타입은 p에 대한 증명을 나타내는 타입이다. axiom(공리)은 이런 타입의 상수가 된다.

constant Proof : Prop → Type

constant and_comm : Π p q : Prop,
  Proof (implies (and p q) (and q p))

variables p q : Prop
#check and_comm p q      -- Proof (implies (and p q) (and q p))

axiom에 덧붙여서, 기존의 proof에서 새로운 proof를 유도하는 규칙이 필요하다. 예를 들어, 명제 논리를 위한 많은 증명 시스템은 modus ponens 규칙을 갖고 있다.

• Proof (implies p q) 와 Proof p 가 있으면, Proof q를 얻을 수 있다. 즉 "p이면 q이다"와 "p이다"에서 "q이다"를 추론해낼 수 있다.

이 규칙은 아래와 같이 표현할 수 있다.

constant modus_ponens :
  Π p q : Prop, Proof (implies p q) →  Proof p → Proof q

명제 논리를 위한 수학적 귀납법 시스템은 보통 다음과 같은 룰에 의존한다.

• p가 참이라고 가정했을 때 q에 대한 증명을 얻을 수 있으면, p이면 q이다를 증명할 수 있다.

constant implies_intro :
  Π p q : Prop, (Proof p → Proof q) → Proof (implies p q).

이러한 접근은 assertion과 broof를 쌓아올리는 합리적인 방법을 제공해준다. 어떤 표현식 t가 assertion p에 대한 올바른 증명인지 판별하기 위해서는 그냥 t가 Proof p 타입을 가지는지만 확인해보면 된다.

그러나, 몇 가지 단순화가 가능하다. 우선 p와 p에 대한 증명(Proof p)의 혼동을 방지하기 위해 항상 Proof를 앞에 붙이는 것을 피할 수 있다. 만약 우리가 p : prop 를 가지고 있다면, 우리는 p를 그 증명에 대한 타입으로 해석할 수 있다. 이 경우 t : p 를 t가 p의 증명이라는 assertion으로 이해할 수 있다.

한 걸음 더 나아가서, 이런 구분을 하고 나면 'P이면 Q이다(implies p q)'와 p →q를 서로 자유롭게 변환할 수 있다는 것을 보일 수 있다. 즉, 'P이면 Q이다' 라는 명제는 임의의 p에 속하는 원소를 받아서 q에 속하는 원소를 반환하는 함수에 대응된다는 것이다. 따라서 굳이 implies 같은 걸 쓸 필요 없이, 평소에 쓰던 함수 생성자 p → q를 implication에 대한 표기로 쓰면 된다.

(아래쪽 설명 문단은 제대로 정리하기에 이해가 부족해서, 뒤쪽 좀 더 읽어보고 나중에 다시 정리하기)