"True" assertion in hoare triples

[AdamBJ]

For question 3 we're asked to find an a such that { fun st => True }} X ::= a {{ fun st => st X = aeval st a} doesn't hold. Before getting to that part of the question though I want to understand exactly what fun st => True means. I know that it represents an assertion that holds before the assignment operation is applied, but what does it tell us? I can understand assertions like fun st => X = 3: before the assignment operation the variables X has 3 stored inside it. Bur for fun st => True, what is true exactly? What does this assertion tell us about the state?

[jaewooklee93]

fun st => True is an assertion which is satisfied by every imaginable memory state. Thus, that precondition gives no restriction to state before the assignment at all.

[AdamBJ]

So question 3 is ~(given that we can start from any imaginable memory state, show that after assigning a to X that X = a). Or, to unroll the ~, "given ... find an a such that after assigning a to X, X != a.

[jaewooklee93]

The definition of Hoare Triple contains universal quantifications (forall) over states in itself. So if we negate it, they become existential quantifications (exists) over states.

Thus, exists a, ~ {{ fun st => True }} X ::= a {{ fun st => st X = aeval st a}}. will be translated into

Find an arithmetic expression a such that there exists a pair of memory states st and st', which satisfies True and (X::=a) / st || st', but also satisfies st' X <> (aeval st' a).

So it's enough that there is at least one pair of such memory state st and st'.

[AdamBJ]

I've been thinking about this question, and my idea is this: X has some state prior to the assignment, say X = 1. Then, say a involves X somehow ,eg a = X + 5. Then after the assignment X = 6. But then the post condition state would be 6 = 6 + 1 which is false.

I want to try this, but I can't figure out how to tell Coq that I want a to be X + 5 using exists. I tried exists APlus((AId X) (ANum 5)). and some other stuff but I can't get the syntax right. Can someone help me with how to use exists in this case?

[jaewooklee93]

Maybe this one works: exists (APlus (AId X) (ANum 5)).

[AdamBJ]

That one does! Thanks.

[AdamBJ]

My goal is:

~
({{fun _ : state => True}} X ::= APlus (AId X) (ANum 5)
 {{fun st : state => st X = aeval st (APlus (AId X) (ANum 5))}})

I think I should apply hoare_consequence_pre so I can apply hoare_asgn. Looking at the definition of hoare_consequenc_pre, what I would expect after applying it is something like

~
?123 X ::= APlus (AId X) (ANum 5)
 {{fun st : state => st X = aeval st (APlus (AId X) (ANum 5))}})
-----------------------------------------------------------------------------
?123 ->> ({{fun _ : state => True}})

Instead I have

{{?9}} ?10
{{fun _ : state =>
  ~
  ({{fun _ : state => True}} X ::= APlus (AId X) (ANum 5)
   {{fun st : state => st X = aeval st (APlus (AId X) (ANum 5))}})}}
______________________________________(2/4)
?8 ->> ?9
______________________________________(3/4)
?10 / ?11 || ?12
______________________________________(4/4)
?8 ?11

Where did these extra subgoals come from and what do they mean? Why is this unexpected behavior happening?

[jaewooklee93]

That's because of small ~ at the beginning of your goal. Hoare consequence rule grabbed completely different term there.

[AdamBJ]

I'm a bit confused about how to apply hoare_consequence_pre to something in the context. After unfolding not I'm left with this:

1 subgoals
H : {{fun _ : state => True}} X ::= APlus (AId X) (ANum 5)
    {{fun st : state => st X = aeval st (APlus (AId X) (ANum 5))}}
______________________________________(1/1)
False

I want to break down H like we've done in the other questions, but when I do eapply hoare_consequence_pre in H. I'm left with something I can't understand:

2 subgoal
H : {{ceval (X ::= APlus (AId X) (ANum 5)) ?8}} ?10 {{?9}}
______________________________________(1/2)
False
______________________________________(2/2)
{{fun st' : state => True -> st' X = aeval st' (APlus (AId X) (ANum 5))}} 
?10 {{?9}}

Can someone explain the behaviour of hoare_consequence_pre here, and/or give me a suggestion for how to get around this problem? Where did the ceval come from?

[jaewooklee93]

After unfolding hoare_triple, you can provide a counterexample of H with assert.

[jaewooklee93]

And the behavior of hoare_consequence_pre there seems quite undesirable and meaningless. Again, hoare consequence rule grabbed improper term and did the odd thing with it, because eapply forced it to do something, but there is no meaningful term to grab.

[AdamBJ]

Unfold hoare_triple changes what I've got in the context:

H : forall st st' : state,
    (X ::= APlus (AId X) (ANum 5)) / st || st' -> True -> st' X = st' X + 5
______________________________________(1/1)
False

But I'm not sure how to work with H. It's not inductive so eliminates a lot of possibilities... am I on the right track here?

[AdamBJ]

Or is there a way to separate out the implications in H? I'd like to apply E_Ass on the first part of H but I can't do that in the current state.

[jeehoonkang]

As you can see, the goal of H is absurd (i.e., you can derive False from it). Thus you have to find st, st', and an evidence of (X ::= APlus (AId X) (ANum 5)) / st || st'. Then you can get by: specialize (H st st' EVIDENCE).

Jeehoon

[AdamBJ]

How can I pull X ::= APlus (AId X) (ANum 5)) / st || st' out of H so I can get EVIDENCE from it though?

[jaewooklee93]

You can provide a counterexample of H with assert.

[AdamBJ]

But I already did that, didn't I? The counter example is X = X + 5

[jaewooklee93]

Yes, but that is only a half of the answer. As I mentioned before, you have to specify not only the arithmetic expression, but also two memory states st and st'.