배열 뒤집기

지침

이번 과제는 직접 만든 배열 뒤집기 함수와 내장 List.reverse가 서로 같다는 것을 증명하는 거예요.

이 연습 문제의 특성상, 전통적인 런타임 테스트에 의존하는 대신 check라는 정리로 증명을 검사해요. 이 정리가 타입 검사를 통과하면 테스트가 통과한 것으로 봐도 돼요.

로컬에서 작업하거나 Lean의 온라인 플레이그라운드에서 작업하면, 어떤 정리가 성공하는지 실패하는지, 그리고 왜 실패하는지를 Lean InfoView를 통해 즉시 확인할 수 있어요. 증명에서 사용 중인 모든 지역 값과 현재 목표를 보여줄 수 있는 아주 유용한 도구예요.

Lean에서 정리 증명하기

정리 증명은 Lean의 핵심적인 부분이에요. 정리 증명을 통해 프로그래머는 자신의 프로그램에 대한 성질을 증명하고, 프로그램의 동작을 추론하며, 제약 조건과 명세를 타입 수준에서 표현할 수 있어요.

이 장에서 Lean의 정리 증명을 잘 소개하고 있어요. 더 깊이 파고들고 싶다면, 이 책이 Lean 웹사이트에 공식 자료로 등록되어 있어요.

Lean은 증명 전체나 그 일부를 자동화할 수 있는 다양한 tactic을 제공해요. 언어 레퍼런스를 확인해 보는 것도 좋아요.

@[csimp]
theorem custom_reverse_eq_spec_reverse : @Extra.custom_reverse = @List.reverse := by
    ... -- proof here

-- now any occurrence of `Extra.custom_reverse` may now compile to `List.reverse`.