Assignment 04 Status

[jeehoonkang]

Hi all,

• Assignment 04 is issued.
• Please read Homework.md to know how to fetch homework and submit your answer.
  • You have to run ./fetch-homework.sh to get assignment 04.
  • Do your homework by editing sf/Assignment04.v.
  • Make sure make works without errors.
  • Commit and push to your GitHub repository.
  • Make sure https://github.com/$YOURID/pl2015 contains the change you made.
• Stay tuned for README.md and this issue on the assignment.

Sincerely, Jeehoon

[rhs0266]

여기에 질문드려도 되나요?

1 subgoals m : nat H : 0 + 0 = S m + S m __(1/1) 0 = S m

이런 상황에서 inversion H.를 하면 어떤 경로를 통해서 goal을 만족하게 되는 것인가요? S m 일 경우와 그냥 m일 경우의 차이점을 모르겠습니다.

[jaewooklee93]

@rhs0266 The left-hand side of H is 0, whereas the right-hand side is S(m+S m) due to the definition of plus. (You may be able to check it directly with simpl in H.) Then what H said is 0 is equal to S of something, which is impossible. Whenever you have any contradictory assumption H, the tactic inversion H. can clear your goal, no matter what your goal is. Because if you have assumed any false sentence, you can prove all the ridiculous lies then. (ex falso quodlibet)

The case is different from H:0+0=m+m. In this case, we cannot argue that 'H said that 0 is equal to S of something, so H is a lie!', because we don't have any evidence for that here.

[rhs0266]

@jaewooklee93 Thank you!!

[PakHyungHoon]

직접 방문해서 질문해도 되나요?

[jeehoonkang]

Today I will be slightly busy; instead TA Yoonseung will be at the office. Contact pl2015@sf.snu.ac.kr

Jeehoon

[LeeGyeongGeon]

이번 숙제에서 apply를 사용하지 않고 rewrite만 사용해서 풀어내면 안 되는 것인가요??

[jeehoonkang]

@LeeGyeongGeon You are allowed to use rewrite only, but I am not sure why you want to; use apply if you think it is appropriate.

[jeehoonkang]

Submissions are collected.

[jeehoonkang]

Delay submissions are collected.

[jeehoonkang]

Submissions for assignment 04 are graded: https://docs.google.com/a/sf.snu.ac.kr/spreadsheets/d/1LzOLx22lF3N31D9RDS20Ec8ub_Rq6IA3utD8CNMk9CQ/edit#gid=1422302047

[jaewooklee93]

@jeehoonkang I sent you an e-mail.

[jeehoonkang]

@jaewooklee93 Sorry; my mistake. Your score is updated.

Jeehoon

[jaewooklee93]

Thank you. I checked it.

[qkr0990]

Hi, This is ByeongJun Park and my student code is (2013-11399), My Id is qkr0990. I want to know the reason why my grade for Assignment 4 has been downgraded as 5 points I reopened the Assignment 4 File and I got to know that there is no problem of which grade is 5 pts. So i think that there is special reason for downgrading as 5 pts. Thank You. Sincerely,

[jeehoonkang]

@qkr0990 5pts for compilation error.

Jeehoon

[jeehoonkang]

Note that from assignment 5 and on, each problem will be graded separately, and compilation error will give you 0 points.

@qkr0990 BTW I would like you NOT to add me as a spam..........

Jeehoon

[qkr0990]

@jeehoonkang Thank you for your fast response!!! have a good weekend!

[rhs0266]

My Assignment 4 Score is 300 at morning. I checked. But now, it becomes ?. What is the meaning of this question mark?

[jeehoonkang]

@rhs0266 That means your repository is not yet private. Please make it private as soon as possible.

[jeehoonkang]

@HexagonalED the same for you, too :-)

[rhs0266]

You have submitted 3 requests: Apr 8, 2015 for @rhs0266 – Pending Mar 17, 2015 for @rhs0266 – Rejected Mar 5, 2015 for @rhs0266 – Rejected

I'm sorry about my fault that I didn't see your notification. But github's answer is so slow.... I will upgrading my repository plan and made my repository private. I'm sorry to do this so late.

[minitu]

@jeehoonkang Please check your email. There doesn't seem to be any QED missing in my submission...