[HW0-4] Verified Algorithms

[duncan020313]

안녕하세요. 프로그램 논증 조교 이동재입니다.
이번 과제에서는 증명 보조기 Lean을 사용하여 여러분들이 평소에 즐겨 사용하던 알고리즘의 올바름을 증명할 것입니다.

아래 링크를 통해 저장소를 생성하고 과제를 시작해 주세요.
https://classroom.github.com/a/l2Xgy9pb

과제를 완료하시면 마지막 커밋을 리포지토리에 푸시해 주시고, Gradescope 에 제출해주세요.

과제를 시작하기 전 리닝크루 가입 절차를 진행할 것을 강력히 권장합니다.

본 과제는 도전 과제로서 성실히 수행하는 학생에게는 Grade Up (예: A- -> A0) 혜택이 주어질 예정입니다.

• 1-17번 문제를 완료한 학생에게 1단계의 Grade Up 혜택이 주어집니다.
• 18-20번 문제를 완료한 학생에게 1단계의 Grade Up 혜택이 주어집니다.

과제의 마감 기한은 11월 30일 23시 59분입니다.

감사합니다.

---

Hello, this is an announcement for the homework0-4

In this assignment, you will prove the correctness of the algorithms you frequently use by using the theorem prover Lean.

Please create a repository and start the assignment through the link below.
https://classroom.github.com/a/l2Xgy9pb

Once you have completed the assignment, please push your final commit to the repository and submit it on [Gradescope](https://www.gradescope.com/courses/1099689).

We strongly recommend following the Leaning Crew sign-up process before starting the assignment.

While this assignment is optional, students who complete it will receive a Grade Up (e.g., A- -> A0) benefit.

• Students who complete problems 1-17 will receive a one-level Grade Up.
• Students who complete problems 18-20 will receive a one-level Grade Up.

The deadline for the assignment is November 30th at 11:59 PM.

Thank you.

[KihongHeo]

성적 상승 여부에 상관 없이 Gradescope 점수로 1등을 한 학생에게는 제가 특별한 선물을 드립니다.

---

Regardless of whether their grade improves or not, I will give a special gift to the student who earns the top score on Gradescope.

[chwons]

I think the theorem gcd_correct is impossible to prove because it is false when a = b = 0

[duncan020313]

Thank you for the report. We'll add precondition a ≠ 0 ∨ b ≠ 0 to the gcd_correct

theorem gcd_correct (a b : Nat) (h : a ≠ 0 ∨ b ≠ 0) :
    greatest_common_divisor (gcd_algorithm a b) a b := sorry

We will push the changes to the repository today. Until then, please manually make the changes and test them.

Thank you

[6eps]

I think theorem tail_fibonacci_correct in Test/fibonacci.lean should be theorem fibonacci_correct, as defined in VeriAlgorithm/Fibonacci.lean

[duncan020313]

Thank you for the report. We'll update it soon

[jDerp]

I think the Fibonacci.lean in test and VeriAlgorithm have mismatch theorem names. Could you please check on that?

[duncan020313]

We send a patch PR to each repository. Please check it.

[6eps]

I think in BinarySearch.lean, if low = 0 and high = 0, then algorithm can stuck by setting mid = 0 , and mid -1 = 0

[duncan020313]

Thank you for the report. We'll update the algorithm.

[duncan020313]

It has been updated. Please check it.

[6eps]

Thank you. Could you please check if the changes have been applied to the grading system?

[duncan020313]

We've updated it. Please check Gradescope.

[duncan020313]

모든 제출물이 재채점 되었습니다.
현재 과제의 일부 theorem이 변경된 상태이고, 이를 반영하지 않을 경우 빌드 오류로 0점 처리 될 수 있습니다.
제출 전 템플릿 코드와 동기화 되었는지 확인하세요

---

All submissions for the current assignment have been regraded.
Some assignment theorems have been modified; not reflecting these changes may result in a score of zero.
Before submitting, check that all synchronization with the template is complete.

[jqpz]

Running lake exe grader in my docker container gives me a "command not found" response.
I wasn't able to find an easy fix. What steps do i have to take to get lake exe grader to run?

[duncan020313]

Did you install the Lean extension? Please check the setup guide