search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Assignment 05 Status #60

Open jeehoonkang opened 9 years ago

jeehoonkang commented 9 years ago

Hi all,

Sincerely, Jeehoon

jeehoonkang commented 9 years ago

Note that I will grade each file on its own; for example, to grade Assignment05_10.v,

Jeehoon

qkr0990 commented 9 years ago

혹시 파일을 별도로 분리하신 이유가 있나요???

jeehoonkang commented 9 years ago

@KyeongmoonKim I think this topic is unrelated to the assignment 5. Please open a new issue :-)

jeehoonkang commented 9 years ago

@qkr0990 Mainly for the ease of grading.

jeehoonkang commented 9 years ago

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

KyeongmoonKim commented 9 years ago

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?

jeehoonkang commented 9 years ago

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

jaewooklee93 commented 9 years ago

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

image

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.

minitu commented 9 years ago

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

jaewooklee93 commented 9 years ago

@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 Undecidable Prop 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.

jeehoonkang commented 9 years ago

@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

jaewooklee93 commented 9 years ago

Thank you. I hope that everyone gets better understanding of this exercise.

jeehoonkang commented 9 years ago

Submissions are collected. As Gil said, I collected submissions slightly later than the schedule.

jeehoonkang commented 9 years ago

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

alkaza commented 9 years ago

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 https://github.com/snu-sf/pl2015/issues/60#issuecomment-94254930.

jeehoonkang commented 9 years ago

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

alkaza commented 9 years ago

I believe there is no way all of them were wrong. This is the error message I got after changing the script.

error

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"; do

and I think the script will work.

Jeehoon

— Reply to this email directly or view it on GitHub https://github.com/snu-sf/pl2015/issues/60#issuecomment-94639772.

jeehoonkang commented 9 years ago

Delay submissions are collected.

jeehoonkang commented 9 years ago

Submissions are graded: https://docs.google.com/spreadsheets/d/1LzOLx22lF3N31D9RDS20Ec8ub_Rq6IA3utD8CNMk9CQ/edit#gid=199588201

qkr0990 commented 9 years ago

NAVER - http://www.naver.com/

qkr0990@naver.com 님께 보내신 메일 <Re: [pl2015] Assignment 05 Status (#60)> 이 다음과 같은 이유로 전송 실패했습니다.

받는 사람이 회원님의 메일을 수신차단 하였습니다.

jeehoonkang commented 9 years ago

@qkr0990 I sincerely hope you do not block me...