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.