`unsafe`나 `partial` 없이 Lean에서 무한 리스트를 구현하는 방법
unsafe나 partial 없이 Lean에서 무한 리스트를 구현하는 방법
7분 읽기 | 2026년 3월 20일
작년에 제가 Lean을 쓸 줄 모르던 시절에 썼던 Lean의 지연 무한 리스트 글을 기억하실지도 모르겠습니다. 저는 아직도 Lean을 쓸 줄 모르지만, 오늘은 다시 무한 리스트를 구현해 보겠습니다. 이번에는 unsafe나 partial로 속이지 않고 말이죠.
사람들은 종종 Lean이 무한 재귀를 하지 못하게 막는다고 말합니다. 그건 정확히는 사실이 아닙니다. Lean이 정말로 막고 싶어 하는 것은 이런 것입니다:
theorem bad : 2 + 2 = 5 := by
exact bad기본적으로 거짓을 증명하는 데 사용할 수 있는 위험한 무한 재귀는 금지됩니다. 하지만 위험하지 않은 형태의 무한 재귀도 있습니다. 예를 들면 do 블록 안의 while 루프가 그렇고, 이것은 내부적으로 partial을 사용해 구현됩니다. 무한 재귀를 하는 또 다른 방법은 partial_fixpoint를 사용하는 것입니다.
최근에 저는 Michael Sammler의 라이브러리 Coinductive와, partial_fixpoint를 훨씬 더 쓰기 편하게 만들어 주는 계산 가능하게 만든 Alex Keizer의 포크를 알게 되었습니다. 먼저 몇 가지를 import하고 다항 함수자 마법을 조금 부려 보겠습니다. (저는 Willem Vanhulle의 Lean formatter를 쓰고 있어서 코드 스타일이 약간 이상해 보일 수도 있습니다.)
import Batteries.Data.Rat.Float
import Coinductive
namespace Stream
open Coinductive Lean.Order
inductive StreamF (α : Type u) (Stream : Type u) : Type u where
| snil
| scons (x : α) (tl : Thunk Stream)
inductive StreamF.In (α : Type u) : Type u where
| snil
| scons (x : α)
@[simp, grind =]
theorem Thunk.get_mk (fn : Unit → α) : Thunk.get ⟨fn⟩ = fn () := by rfl
@[simp]
theorem Thunk.mk_get (x : Thunk α) : Thunk.mk (fun _ ↦ x.get) = x := by simp [Thunk.ext_iff]
instance (α : Type u) : PF (StreamF α)
where
P :=
⟨StreamF.In α, fun
| .snil => PEmpty
| .scons _ => PUnit⟩
unpack
| .snil => .obj (.snil) nofun
| .scons hd tl => .obj (.scons hd) fun _ ↦ tl.get
pack
| .obj (.snil) _ => .snil
| .obj (.scons hd) tl => .scons hd (tl ⟨⟩)
unpack_pack := by rintro _ (_ | _) <;> simp
pack_unpack := by rintro _ (⟨⟨⟩, _⟩ | ⟨⟨⟩⟩) <;> simp <;> funext x <;> cases x
abbrev Stream (α : Type u) : Type u :=
CoInd (StreamF α)
def Stream.fold (t : StreamF α (Stream α)) : Stream α :=
CoInd.fold _ t
def Stream.snil : Stream α :=
.fold .snil
def Stream.scons (hd : α) (tl : Thunk (Stream α)) : Stream α :=
.fold <| .scons hd tl
instance : Inhabited (StreamF α PUnit) where default := .snil좋습니다. 이제 Stream.map 함수를 쓸 수 있을까요?
def Stream.map (f : α → β) (s : Stream α) : Stream β :=
match s.unfold with
| .snil => .snil
| .scons hd tl => .scons (f hd) (Stream.map f tl.get)
partial_fixpoint그렇게 빠르진 않습니다! Lean은 오류를 던집니다:
Could not prove 'Stream.Stream.map' to be monotone in its recursive calls:
Cannot eliminate recursive call `Stream.map f tl.get` enclosed in
scons (f hd✝) { fn := fun x => map f tl✝.get }여기서 이론까지 깊게 들어가지는 않겠지만, 기본적으로 Lean은 Stream.map의 이 정의가 Stream 타입의 부분 순서를 보존한다는 것을 보여 주어야만 받아들입니다. 아래가 전체 증명입니다.
@[simp]
theorem unfold_snil : CoInd.unfold _ Stream.snil = StreamF.snil (α := α) := by simp [Stream.snil, Stream.fold]
@[simp]
theorem unfold_scons : CoInd.unfold _ (Stream.scons i s) = StreamF.scons i s := by simp [Stream.scons, Stream.fold]
@[simp]
theorem Stream.bot_eq : CoInd.bot (StreamF α) = Stream.snil :=
by
rw [CoInd.bot_eq]
simp [PF.map, PF.pack, Stream.snil, Stream.fold]
theorem Stream.le_unfold (s1 s2 : Stream α) :
(s1 ⊑ s2) = (s1 = .snil ∨ ∃ i s1' s2', s1 = .scons i s1' ∧ s2 = .scons i s2' ∧ s1'.get ⊑ s2'.get) :=
by
ext
constructor
· intro h
rw [CoInd.le_unfold] at h
rcases h with (rfl | ⟨i, _, _, _, _, h1, h2⟩); simp
rw [← unfold_fold _ s1, ← unfold_fold _ s2]
rw [← PF.unpack_pack s1.unfold, ← PF.unpack_pack s2.unfold]
simp only [h1, h2]
cases i <;> simp [PF.pack, snil, scons, fold]
right
exists ?_, ?_; rotate_left 1
constructor; rfl
apply Exists.intro
constructor; rfl
simp_all
· rintro (rfl | ⟨_, _, _, rfl, rfl, _⟩)
· simp [CoInd.le_unfold]
· simp [CoInd.le_unfold]
right
simp [PF.unpack]
constructor <;> try rfl
grind
theorem scons_monoN α i (s1 s2 : Thunk (Stream α)) n :
CoIndN.le _ (s1.get.approx n) (s2.get.approx n) →
CoIndN.le _ ((Stream.scons i s1).approx (n + 1)) ((Stream.scons i s2).approx (n + 1)) :=
by
intro hs
simp [CoIndN.le, PF.unpack]
right
constructor <;> try rfl
grind [coherent1]
@[partial_fixpoint_monotone]
theorem scons_mono [PartialOrder β] i (f : β → Stream α) : monotone f → monotone fun x ↦ Stream.scons i ⟨fun _ ↦ f x⟩ :=
by
intro hf t1 t2 hle
apply CoInd.le_leN
rintro ⟨n⟩; simp [CoIndN.le]
apply scons_monoN
grind [CoInd.leN_le, monotone]
def Stream.map (f : α → β) (s : Stream α) : Stream β :=
match s.unfold with
| .snil => .snil
| .scons hd tl => .scons (f hd) (Stream.map f tl.get)
partial_fixpoint
@[partial_fixpoint_monotone]
theorem map_mono [PartialOrder γ] (f : α → β) (g : γ → Stream α) : monotone g → monotone fun x ↦ Stream.map f (g x) :=
by
intro hf t1 t2 hle
apply CoInd.le_leN
intro n
dsimp only
have hs : (g t1) ⊑ (g t2) := by grind [monotone]
generalize g t1 = s1, g t2 = s2 at hs
induction n generalizing s1 s2 with
| zero => simp [CoIndN.le]
| succ n ih =>
unfold Stream.map
rw [Stream.le_unfold] at hs
rcases hs with rfl | ⟨hd, tl1, tl2, rfl, rfl, htl⟩
· simp [CoIndN.le, CoIndN.bot]
· simp_all
simp [CoIndN.le, PF.unpack]
right
constructor <;> try rfl
intro x
exact ih _ _ htl이제 코사인을 정의할 때 쓰던 우리가 가장 좋아하는 트릭을 사용할 수 있습니다. (간결함을 위해 단조성 정리 몇 개는 생략했습니다.)
def Stream.take (s : Stream α) : Nat → List (Option α)
| 0 => []
| n + 1 => s.shead :: s.stail.take n
def pos :=
Stream.scons (1 : Rat) <| pos.map (· + 1)
partial_fixpoint
#eval pos.take 10
notation s "integrate" c => Stream.scons c <| Stream.zipWith (· / ·) s pos
#eval (1 : Rat) / 3
def expSeries :=
expSeries integrate 1
partial_fixpoint
#eval expSeries.take 10
def evalAt n (s : Stream Rat) (x : Rat) :=
s.take n |>.foldr
(fun a acc ↦
match a with
| none => acc * x
| some a => a + acc * x)
0
#eval (evalAt 10 expSeries 2 : Float)
#eval Float.exp 2
mutual
def sinSeries :=
cosSeries integrate (0 : Rat)
partial_fixpoint
def cosSeries :=
(sinSeries integrate (-1)).map (-·)
partial_fixpoint
end
#eval (evalAt 10 sinSeries 2 : Float)
#eval Float.sin 2좋습니다, 이제 더 이상 unsafe나 partial이 필요 없습니다! 하지만 이 접근법에는 큰 문제가 하나 있는데, 엄청나게 느리다는 점입니다. 단순한 pos.take 25조차도 이미 30초가 걸리고, 그 수를 늘릴수록 지수적으로 커지는 것처럼 보입니다. 반면 같은 코드를 Haskell에서 실행하면 선형 시간이 걸립니다:
pos = 1 : map (1+) pos
take 2500 pos혹시 무한할 수도 있는 리스트의 타입 대신, 오직 무한 리스트만의 타입을 쓴다면 어떨까요? 그러면 이 타입의 부분 순서에는 바닥 원소가 없기 때문에, 이 타입에 대한 재귀 함수를 정의할 때 partial_fixpoint를 직접 사용할 수는 없을 것입니다. 다행히 Lean에서 F91을 정의할 때 사용한 트릭과 비슷한 우회 방법이 있습니다. Stream.map이 무한성을 보존한다는 것을 증명하고, Stream.map의 입력과 출력 타입을 오직 무한 리스트로만 제한하는 것입니다. 다만 저는 아직 이 아이디어를 어떻게 구현해야 할지 알아내지 못했으니, 아마 미래의 블로그 글에서 다루게 될지도 모르겠습니다.
2026년 1월 11일
“오이엠이 채워 넣을 예정”
CC BY-SA 4.0