search

snu-sf-class / pl201602

SNU 2016 Fall 4190.310 Programming Language
22 stars 10 forks source link

Assignment 09 P01.v 질문 있습니다! #57

Closed Holim0711 closed 7 years ago

Holim0711 commented 7 years ago

Factorial을 구하는 프로그램이 옳게 되는지 증명하는 문제인데 중간에 while문이 있어 hoare_while을 써야 합니다. 시작조건이 P, 나중 조건이 P /\ ~b가 되는데 b가 not(X = 0) 이어서 나중 조건이 not(not(X = 0))이 됩니다. 이 경우 이중 negation을 풀려면 excluded_middle이 필요할 것 같은데, 혹시 없이도 풀 수 있는 문제인가요?

minsuu commented 7 years ago

Prop이 아니라 bool type이기 때문에 없어도 가능합니다. 제 경우엔 eq_true_negb_classical를 적용하여 풀었습니다.

Holim0711 commented 7 years ago

아! 감사합니다!