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}}).
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 :slight_smile:

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.