search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Assignment 09_03 #132

Closed alkaza closed 9 years ago

alkaza commented 9 years ago

I don't understand how to get started on this one, since I cannot introduce a into the context. I tried to do unfold not. unfold hoare_triple. and I don't see what else could I do there, I'm left with this:

1 subgoals
______________________________________(1/1)
exists a : aexp,
  (forall st st' : state,
   (X ::= a) / st || st' -> True -> st' X = aeval st' a) -> False

Please help!

jeehoonkang commented 9 years ago

Say you know exactly which a satisfies the goal. Then exists (something_that_satisfies_as_a). will give you a manageable goal.

alkaza commented 9 years ago

Thank you!