# Asser assume differ

Hello once again ! I’ve created this topic to be more specific about one question in particular :
I’m trying to proof this theorem from the book software foundation hoare.v :

``````Theorem assert_assume_differ : exists P b Q,
({{P}} ASSUME b {{Q}})
/\ ~ ({{P}} ASSERT b {{Q}}).
Proof.
exists (fun st => True).
exists (BFalse).
exists (fun st => False).
``````

I don’t see how to finish the proof, would you have any idea?

I actually didn’t do this the first time through, as it’s optional, but it was fun to work through

I was going to share exactly what I came up with, but I think that is considered in poor form…as such, here is a hint: the next step should be to `unfold hoare_triple` then split. Now you have two things to prove. I actually started with slightly different exists, but was able to prove it with the ones you posted.

When you get to the ~(stuff) case, do `intros contra` and then try to find a contradiction above the line. You have a lot of flexibility in this case because it has to be true for ALL states.

Give it a try and if you’re still stuck, ask again.