Assignment 05 Status
jeehoonkang opened this issue · 21 comments
Hi all,
-
Assignment 05 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 05. - Do your homework by editing
sf/Assignment05_??.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.
- You have to run
-
Stay tuned for README.md and this issue on the assignment.
-
You are NOT allowed to use the
admit
tactic
becauseadmit
simply admits any goal
regardless 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
Note that I will grade each file on its own; for example, to grade Assignment05_10.v
,
- I will copy the skeleton files;
- I will copy your
Assignment05_10.v
ONLY. - I will compile and grade in this setting.
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
axiom (i.e. an instance of excluded middle) for any particular Prop [P].
Why? Because we cannot prove the negation of such an axiom; if we could,
we would have both [~ (P / P)] and [ ~ (P / ~P)], a contradiction.
In the first line, What is a decidability axiom? And does axiom means theorem that doesn't need proving?
The "decidability" for a proposition P
is: P \/ ~ P
.
On the Consistency of the Decidability
As 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 False
out of the decidability). It implies that it is safe to admit the decidability as an additional axiom in Coq.
The exercise asks you to prove this safety: Theorem excluded_middle_irrefutable: forall (P:Prop), ~ ~ (P \/ ~ P).
Jeehoon
@KyeongmoonKim The law of excluded middle
is something like this.
Can you decide whether the following equation has a natural number solution (x,y,z) or not?
More precisely, can you prove the proposition P
?
P: Yes, the equation has at least one natural number solution.
Maybe not. Then how about ~P
?
~P: No, there is no natural number solution for the equation.
I guess that nobody can prove either P
or ~P
, because the given equation is too difficult to analyze.
However, the interesting thing is, even though you cannot construct the proof of P
or ~P
, you really want to believe that at least one of P
or ~P
should be true, because it seems very natural that there are only two cases, that the equation has at least one solution, or not at all. And the reason for that you think so is because you already Admitted
the law of excluded middle
(배중률, in Korean), which says P \/ ~P
is always true for every P
.
But there is a group of mathematicians who deny to accept the law of excluded middle
, they are called Constructivists, and it is totally nonsense for them to believe such law, P \/ ~P
is true, while you cannot construct the proof of either of P
or ~P
. Surprisingly, Coq is one of them, so you cannot use that law by default in Coq, but if you really want to use it, you must manually import excluded_middle
from library.
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 ~ ~ (P \/ ~ P)
logically equal to (P \/ ~P)
?
If this is so, when we prove excluded_middle_irrefutable
, aren't we proving that the law of excluded middle always holds and that the Constructivists are wrong?
@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 excluded_middle -> classic_double_neg
and classic_double_neg -> excluded_middle
. Thus, constructivists, who deny to accept excluded_middle
, must deny to accept classic_double_neg
as well. So, if you try to prove classic_double_neg
in Coq, you will find that it is not provable, soon.
In constructive logic, you have only one direction. You can prove P -> ~~P
, which is our Assignment05_08.v
, but you cannot prove the opposite, ~~P -> P
.
Thus, an interesting thing happens. If you believe excluded_middle
, excluded_middle_irrefutable
implies excluded_middle
itself, so you can believe excluded_middle
. Otherwise, if you don't believe excluded_middle
, excluded_middle_irrefutable
does not implies excluded_middle
, so you don't have to believe excluded_middle
. You may easily find that there is nothing to obtain in both cases.
Also, constructivists didn't claim that excluded_middle
is False
, that is unreasonable, because of excluded_middle_irrefutable
. However, they're just saying "We don't know" about excluded_middle
. Thus, there is no problem actually.
The fact that we cannot use double negation seems contradictory to the theorem we proved in Basics.v
Theorem negb_involutive : forall b : bool, negb (negb b) = b.
However, it is another big difference between bool
and Prop
. You can easily prove negb_involutive
with destruct b
, but you cannot use destruct P
to prove classic_double_neg
.
Everything that you can represent with bool
type should be decidable, that is, you can compute the value of it with terminating Turing machine in finite time, so there are only two values, true
and false
in bool
type. However, Prop
type doesn't follow Boolean algebra, but follow Heyting algebra. You can intuitively think that there are three values for P
, True
(You can prove P
), False
(You can prove ~P
), and Undecidable (You cannot prove both of P
and ~P
). And the existence of that middle state is the reason for being unable to use double negation. Of course, if you assume excluded_middle
or the decidability axiom, there is no such middle state, and you can use double negation then.
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.
Gödel's first incompleteness theorem (1931): Every proof system which has enough power to define
nat
should contain UndecidableProp
in itself.
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
- You have to use it with
bash
, andsed
should be installed in your machine. You can use these programs in themartini.snucse.org
andmidori.snucse.org
servers. - Place your
Assignment05_??.v
files insubmission
folder. NOTE:original
folder should be intact. - Run by
./grader.sh
. - If your submission has a compilation error, then an error message will be present.
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
what should I do?
On Sun, Apr 19, 2015 at 6:14 PM, Jeehoon Kang notifications@github.com
wrote:
I made an automatic grader:
http://sf.snu.ac.kr/jeehoon.kang/pl2015/Assignment05_grader.tar.gz
- You have to use it with bash, and sed should be installed in your
machine. You can use these programs in the martini.snucse.org and
midori.snucse.org servers.- Place your Assignment05_??.v files in submission folder. NOTE:
original folder should be intact.- Run by ./grader.sh.
- If your submission has a compilation error, then an error message
will be present.Hope this grader will help you prepare a good submission.
Jeehoon
—
Reply to this email directly or view it on GitHub
#60 (comment).
Hi @alkaza
I think Windows's seq
does not work here. Instead, replace:
for i in $(seq -f "%02g" 1 ${NPROBS}); do
with:
for i in "01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39"; do
and I think the script will work.
Jeehoon
I believe there is no way all of them were wrong.
This is the error message I got after changing the script.
I don't understand how to resolve compilation error.
On Tue, Apr 21, 2015 at 2:06 PM, Jeehoon Kang notifications@github.com
wrote:
Hi @alkaza https://github.com/alkaza
I think Windows's seq does not work here. Instead, replace:
for i in$(seq -f "%02g" 1 $ {NPROBS}); do
with:
for i in "01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39"; doand I think the script will work.
Jeehoon
—
Reply to this email directly or view it on GitHub
#60 (comment).
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...