different definitions of hoare_if

[AdamBJ]

Assignment09_00 defines hoare_if as:

Theorem hoare_if : forall Q1 Q2 Q b c1 c2,
  {{Q1}} c1 {{Q}} ->
  {{Q2}} c2 {{Q}} ->
  {{fun st => (beval st b = true -> Q1 st) /\ (beval st b = false -> Q2 st) }} 
    (IFB b THEN c1 ELSE c2 FI) 
  {{Q}}.

But the textbook defines it as:

Theorem hoare_if : ∀P Q b c1 c2,
  {{fun st ⇒ P st ∧ bassn b st}} c1 {{Q}} →
  {{fun st ⇒ P st ∧ ~(bassn b st)}} c2 {{Q}} →
  {{P}} (IFB b THEN c1 ELSE c2 FI) {{Q}}.

I think I can see why these are equivalent, but why was the definition changed for the homework? The other hoare rules are more or less the same as the versions presented in the text.

[jeehoonkang]

I redirected your question to professor Hur.

[jaewooklee93]

I guess that professor intentionally changed the definition. With this new definition, I've got no problem in solving all questions in Assignment 09. Also, I prefer professor's version because it reduces one eapply hoare_consequence_pre and we don't need to unfold bassn.

[gilhur]

I prefer the version in the assignment because it gives you the weakest precondition. Anyway, the two versions are equivalent in the presence of the consequence rule.