snu-sf-class/pl2015spring

Assignment 04 Status

Opened this issue · 22 comments

jeehoonkang commented

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 commented

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

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

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

jaewooklee93 commented

@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 commented

@jaewooklee93 Thank you!!

PakHyungHoon commented

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

jeehoonkang commented

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

Jeehoon

LeeGyeongGeon commented

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

jeehoonkang commented

@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 commented

Submissions are collected.

jeehoonkang commented

Delay submissions are collected.

jaewooklee93 commented

@jeehoonkang I sent you an e-mail.

jeehoonkang commented

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

Jeehoon

jaewooklee93 commented

Thank you. I checked it.

qkr0990 commented

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 commented

@qkr0990 5pts for compilation error.

Jeehoon

jeehoonkang commented

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 commented

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

rhs0266 commented

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

jeehoonkang commented

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

jeehoonkang commented

@HexagonalED the same for you, too :-)

rhs0266 commented

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 commented

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