Midterm Status

[jeehoonkang]

Midterm submissions are graded. See: https://docs.google.com/spreadsheets/d/1LzOLx22lF3N31D9RDS20Ec8ub_Rq6IA3utD8CNMk9CQ/edit#gid=1440146993

• 0(COMPILE) means your proof script is not well-compiled.
• 0(ADMIT) means you have admits in your proof script.
• 0(FORBIDDEN) means you used forbidden tactics.
• 0(CHECK) means your definition/theorem is strange.

[Parkdaeyoung]

My student Id is 2010-10422 and I didn't admit all of problems. I think two or three of them was admitted in the exam. Can I fix this problem ? or Should I 'admit' my grade?

[jeehoonkang]

@Parkdaeyoung I saw two submissions from you, and both of them contain admitted proof scripts for all problems. If you want to see what I gathered, please visit my office.

Jeehoon

[hyunjinjeong]

Hello, My student id is 2013-11431. My 8th problem score is zero because of compile error and only I have compile error. Can I know what compile error occurs?

[jeehoonkang]

@Hyunjin95 Here is your submission for problem 8: https://gist.github.com/jeehoonkang/4de7367737202f2c1062

Your sorted_min_example2 is not well-closed by Qed.

[hyunjinjeong]

@jeehoonkang I made dumb mistake.. I thought it will compile well because it has no problem in CoqIDE. Thank you.

[Parkdaeyoung]

Can I visit your office at 4pm Wed?

[hyunjinjeong]

@jeehoonkang I'm sorry but may I ask one more thing? I wonder if I can get partial score or not.

[jeehoonkang]

@Parkdaeyoung Yes, please. @Hyunjin95 I will ask Gil about the issue. @sanha I saw your email, and I will ask Gil about the issue you raised.

Jeehoon

[hyunjinjeong]

@jeehoonkang I see. Thank you for reply

[jeehoonkang]

Problem 8 will be re-graded, soon.

[jeehoonkang]

Problem 8 is re-graded. In short, we additionally checked if Example sorted_min_non_example2: sorted_min 3 [4; 5; 4] -> False. is provable.

Jeehoon

[ik1ne]

After re-grading, my score of problem 8 became 0(CHECK). Does that means my definition of sorted_min failed to prove Example sorted_min_non_example2: sorted_min 3 [4; 5; 4] -> False.?

[jeehoonkang]

@ik1ne your definition:

Inductive sorted_min: nat -> list nat -> Prop :=
  | sort_min_init: forall (n:nat), True -> sorted_min n nil
  | sort_min_cons_single: forall (n m:nat), (le n m) -> sorted_min n [m]
  | sort_min_cons_double: forall (n m o:nat) (l1: list nat), (le n m) -> (le m o) -> (sorted_min n ([m;o]++l1))                                           
.

is invalid, as sorted_min 1 [2; 3; 1] is justified by sort_min_cons_double.

Jeehoon

[ik1ne]

Well, Thank you for checking that out. I should have checked not only Example sortedmin*, but my own test cases.

[ik1ne]

Another question, in the final exam should I assume that passing all Example cases doesn't assure my definition is right?

[jeehoonkang]

@ik1ne You cannot. Your submission will be graded with additional Examples and Proofs.