When to apply hoare_if

[AdamBJ]

In text, the authors apply hoare_if directly as the first step of this proof:

   {{fun st => True}} 
  IFB (BEq (AId X) (ANum 0)) 
    THEN (Y ::= (ANum 2)) 
    ELSE (Y ::= APlus (AId X) (ANum 1)) 
  FI
    {{fun st => st X <= st Y}}.

Yet in question 5 of this week's homework, where we are asked to prove this:

  {{fun st => True}}
  IFB (BLe (AId X) (AId Y))
    THEN (Z ::= AMinus (AId Y) (AId X))
    ELSE (Y ::= APlus (AId X) (AId Z))
  FI
  {{fun st => st Y = st X + st Z}}. 

We can't apply hoare_if right away. I managed to solve the assignment question anyway, so I'm not looking for help with it specifically. I just want to know why can't we use hoare_if directly in the second problem like we could in the first.

[jeehoonkang]

The goal's precondition of hoare_if is: {{fun st => (beval st b = true -> Q1 st) /\ (beval st b = false -> Q2 st) }}. On the other hand, the precondition of question 5 is: {{fun st => True}}. Since these are not compatible, you cannot hoare_if right away.

[jaewooklee93]

Due to the difference between author's hoare_if and our professor's hoare_if, you cannot refer to the proof of if_example in the textbook directly, and slight modification is needed.

Example if_example :
    {{fun st => True}}
  IFB (BEq (AId X) (ANum 0))
    THEN (Y ::= (ANum 2))
    ELSE (Y ::= APlus (AId X) (ANum 1))
  FI
    {{fun st => st X <= st Y}}.
Proof.
  eapply hoare_consequence_pre.
  - apply hoare_if; apply hoare_asgn.
  - unfold assn_sub, assert_implies, update; simpl.
    intros; split; intros.
    + apply beq_nat_true in H0; omega.
    + omega.
Qed.

[gilhur]

As Jaewook showed, you need to apply the hoare_consequence_pre rule first.