search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Meaning of (((fun st0 : state => st0 X = 1 /\ st0 Y = 2) [Y |-> ANum 2]) [X |-> ANum 1]) st #121

Closed AdamBJ closed 9 years ago

AdamBJ commented 9 years ago

What is the goal (((fun st0 : state => st0 X = 1 /\ st0 Y = 2) [Y |-> ANum 2]) [X |-> ANum 1]) st asking us to prove exactly? Is it: if in st0 st0 X = 1 /\ st0 Y = 2, by replacing all references to X with 1 and all references to Y by 2 then we move to a new state, st, where 1 = 1 and 2 = 2?

jaewooklee93 commented 9 years ago

If you are not sure about that, just try unfold assn_sub; simpl.

AdamBJ commented 9 years ago

Oh, that's just what I was looking for! Thanks! Jaewook, are you an honorary TA or something? Your knowledge of this stuff is really exceptional.

jaewooklee93 commented 9 years ago

No, I am an ordinary undergraduate student and a newcomer to Coq like other students. But since I'm majoring in both of mathematics and computer science, I'm really enjoying Coq and its underlying Logical system. Answering others' questions here is just my voluntary work :)

AdamBJ commented 9 years ago

I see. Well, I think the students in this class are really lucky to be taking it with you then!

jeehoonkang commented 9 years ago

@jaewooklee93 Always thank you for your contribution.

Jeehoon