-
Notifications
You must be signed in to change notification settings - Fork 6
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Assignment 05 Status #60
Comments
Note that I will grade each file on its own; for example, to grade
Jeehoon |
혹시 파일을 별도로 분리하신 이유가 있나요??? |
@KyeongmoonKim I think this topic is unrelated to the assignment 5. Please open a new issue :-) |
@qkr0990 Mainly for the ease of grading. |
Furthermore, since there are students who do not speak Korean, please try to ask in English in this tracker. It would help everyone to understand what's going on in the discussion. Jeehoon |
In comment of Assignment05_11.v, This theorem implies that it is always safe to add a decidability In the first line, What is a decidability axiom? And does axiom means theorem that doesn't need proving? |
The "decidability" for a proposition On the Consistency of the DecidabilityAs everything else, in the deep deep bottom of the world of mathematics, there are some things you have to believe. Those things we have to believe are called "axioms". Since we "believe", it does not need proving. There are just believed. However, historically there are arguments on what is worth believing. Decidability is one of such things. Most mathematicians believe the decidability of arbitrary propositions. However, in Coq the decidability is not automatically believed (or, admitted as an axiom). However, the decidability is known to be consistent in Coq: believing it is not harmful (i.e., you cannot prove The exercise asks you to prove this safety: Jeehoon |
@KyeongmoonKim The law of Can you decide whether the following equation has a natural number solution (x,y,z) or not? More precisely, can you prove the proposition Maybe not. Then how about I guess that nobody can prove either However, the interesting thing is, even though you cannot construct the proof of But there is a group of mathematicians who deny to accept the law of And then what this exercise asks you for proving is that, even if you are a constructivist, so you deny to accept that law, you cannot disprove (refute) the law of excluded middle. Please let me know if there is any error in my writing. |
@jaewooklee93 I'm just curious: isn't |
@minitu That is another interesting point. Definition classic_double_neg := forall P : Prop, ~~P -> P. Double negation is logically equivalent to the law of excluded middle, that is, you can prove both of In constructive logic, you have only one direction. You can prove Thus, an interesting thing happens. If you believe Also, constructivists didn't claim that The fact that we cannot use double negation seems contradictory to the theorem we proved in Theorem negb_involutive : forall b : bool, negb (negb b) = b. However, it is another big difference between Everything that you can represent with The existence of Undecidable is not the flaw of Coq itself, but it is a natural and universal thing in all fields of mathematics, because of the following monumental theorem.
Again, please let me know if there is any error inside. I'm also confused because it is not my specialty as well. |
@jaewooklee93 Thank you for your useful and easy-to-read summary. I personally learned about the Heyting algebra! I would like to merely note that: while Coq's logic is constructive, I personally believe the law of excluded middle and I am not a constructivist. If the law of excluded middle simplifies my Coq scripts, I am happy to admit it. This is because I think almost all models we can find around the world admits the law of excluded middle. Jeehoon |
Thank you. I hope that everyone gets better understanding of this exercise. |
Submissions are collected. As Gil said, I collected submissions slightly later than the schedule. |
I made an automatic grader: http://sf.snu.ac.kr/jeehoon.kang/pl2015/Assignment05_grader.tar.gz
Hope this grader will help you prepare a good submission. Jeehoon |
In the middle of the process seq.exe stops working. What does it mean and On Sun, Apr 19, 2015 at 6:14 PM, Jeehoon Kang notifications@github.com
|
Hi @alkaza I think Windows's and I think the script will work. Jeehoon |
I believe there is no way all of them were wrong. I don't understand how to resolve compilation error. On Tue, Apr 21, 2015 at 2:06 PM, Jeehoon Kang notifications@github.com
|
Delay submissions are collected. |
NAVER - http://www.naver.com/qkr0990@naver.com 님께 보내신 메일 <Re: [pl2015] Assignment 05 Status (#60)> 이 다음과 같은 이유로 전송 실패했습니다. 받는 사람이 회원님의 메일을 수신차단 하였습니다. |
@qkr0990 I sincerely hope you do not block me... |
Hi all,
Assignment 05 is issued.
Please read Homework.md to know how to fetch homework and submit your answer.
./fetch-homework.sh
to get assignment 05.sf/Assignment05_??.v
.make
works without errors.https://github.com/$YOURID/pl2015
contains the change you made.Stay tuned for README.md and this issue on the assignment.
You are NOT allowed to use the
admit
tacticbecause
admit
simply admits any goalregardless of whether it is provable or not.
But, you can leave
admit
for problems that you cannot prove.Then you will get zero points for those problems.
You are NOT allowed to use the following tactics.
tauto
,intuition
,firstorder
,omega
.Do NOT add any additional
Require Import/Export
.Sincerely,
Jeehoon
The text was updated successfully, but these errors were encountered: