search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

BEq a a0 = true or false #112

Open HyeongMee opened 9 years ago

HyeongMee commented 9 years ago

How can I express "BEq a a0 is either true or false" in Coq? There's nothing like BOr;; So I am stuck in the 4th problemTT

jaewooklee93 commented 9 years ago

Do you want to perform a case analysis on that? Then you may be able to use destruct eqn like below.

destruct (beval st (BEq a a0)) eqn:B.

Then the goal will be separated into two cases, namely (BEq a a0=true) and (BEq a a0=false). However, I definitely believe that you don't need to write code in this way to solve 4th one.

HyeongMee commented 9 years ago

@jaewooklee93 THX :D