Lean에서 무한 리스트 구현에 관한 본 글은 unsafe나 partial 키워드 없이 안전하게 무한 리스트를 다루는 방법을 소개합니다.

Coinductive 라이브러리를 활용하여 코딩하며, StreamF라는 코어 데이터 구조와 partial_fixpoint를 통해 무한 리스트를 정의하고, 이를 기반으로 Stream.map 함수 구현 시 발생하는 모노톤성(monotonicity) 증명 문제를 해결하는 과정을 상세히 다룹니다.

이 접근법은 Lean의 엄격한 재귀 제한을 우회하면서도, 안전한 무한 재귀를 가능하게 하여, 코사인과 같은 무한 급수도 표현할 수 있게 합니다. 다만, 현재 구현은 성능이 매우 느리며, Haskell과 같은 언어 대비 실행 속도가 크게 떨어지는 한계가 있습니다.

마지막으로, 무한 리스트를 다루는 더 효율적인 방법으로 오직 무한 리스트만을 타입으로 사용하는 방안을 제안하며, 이 경우에는 partial_fixpoint를 직접 쓸 수 없으나, 무한성을 보존하는 map 함수를 정의해 타입을 제한하는 방식으로 해결할 수 있음을 시사합니다.