Hoare3

Reasoning About Imp programs

We saw that we can use the equational theory of the monad laws, along with some monad-specific properties to prove program transformations.

What if we want to prove other things about our programs?

Generalizing EqM

Recall eqM : ∀ A, M A → M A → Prop , in particular our insistance that bind be Proper.

Idea: generalize to a binary, heterogeneous relation: eqMR : ∀ A B, M A → M B → Prop

More General Typeclass

Definition relationH A B := A → B → Prop

  Class EqMR (M : Type → Type) : Type := {
      eqMR : ∀ {A B : Type} (R : relationH A B), relationH (M A) (M B)
  }.

Assuming R : A → B → Prop (i.e. R : relH A B)

Notation "t₁ ≈[ R ] t₂" := (eutt R t₁ t₂) (at level 20).

Note: we can recover the ordinary eqM by instantiating R with = :
eqM := eqMR eq

Logical relation for (itree) ret

For eqM, we didn't have to justify that ret was Proper. But for this version, we have to show that it is.
    eqMR_Ret
     : ∀ (E : Type → Type) (R₁ R₂ : Type) (RR : relH R₁ R₂) (r₁ : R₁) (r₂ : R₂),
      RR r₁ r₂ ↔ Ret r₁ ≈[ RR] Ret r₂

Logical relation for bind

The generalization of Proper for bind looks like this:
eqMR_bind
     : ∀ (E : Type → Type) (R₁ R₂ : Type) (RR : relH R₁ R₂) (U₁ U₂ : Type)
         (UU : relH U₁ U₂) (t₁ : itree E U₁) (t₂ : itree E U₂) (k₁ : U₁ → itree E R₁)
         (k₂ : U₂ → itree E R₂),
       t₁ ≈[ UU] t₂ →
       (∀ (u₁ : U₁) (u₂ : U₂), UU u₁ u₂ → k₁ u₁ ≈[ RR] k₂ u₂) →
       (x <- t₁;; k₁ x) ≈[ RR] (x <- t₂;; k₂ x)

Expected Properties Of EqMR

EqMR

If R is a an equivalence then so is ≈[RR]
Monotonicity: if R₁ ⊆ R₂ then ≈[R₁] ⊆ ≈[R₂]
General notion of the "image" of a monadic computation (useful for inversion principles).

Definition imageH m a₁ a₂ := ∀ R, PER R → m ≈[R] m → R a₁ a₂.
Definition image m a := imageH m a a.
Notation "a ∈ m" := (image m a)

Semantic Definition of Hoare Triples

Definition hoare_itree_triple (P:Assertion) (c:com) (Q:Assertion) :=
∀ σ, P σ → eutt (fun '(σ1,_) '(σ2,_) ⇒ σ1 = σ2 ∧ Q σ1) (ℑ ⟦c⟧ σ) (ℑ ⟦c⟧ σ).

Notation "⦃ P ⦄ c ⦃ Q ⦄" :=
(hoare_itree_triple P c Q) (at level 90, c custom com at level 99)
: hoare_spec_scope.

Proofs of Hoare Inference Rules

Theorem hoare_itree_skip : ∀ P,
     ⦃P⦄ skip ⦃P⦄.
Proof.
  intros P.
  unfold hoare_itree_triple.
  cbn.
  intros.
  rewrite interp_state_ret. apply eutt_Ret. intuition.
Qed.

Theorem hoare_itree_seq : ∀ P Q R c₁ c₂,
     ⦃Q⦄ c₂ ⦃R⦄ →
     ⦃P⦄ c₁ ⦃Q⦄ →
     ⦃P⦄ c₁; c₂ ⦃R⦄.
Proof.
  unfold hoare_itree_triple.
  intros P Q R c₁ c₂ H₁ H₂ st PRE.
  cbn.
  norm.
  eapply eutt_clo_bind. apply H₂; auto.
  destruct u₁, u₂. intros [MEQ QM].
  subst. simpl.
  eapply H₁; auto.
Qed.

Theorem hoare_itree_asgn : ∀ Q X a,
  ⦃Q [X ⊢> a]⦄ X := a ⦃Q⦄.
Proof.
  unfold hoare_itree_triple.
  intros Q X a σ HQ.
  cbn.
  norm. cbn.
  apply eutt_Ret. intuition.
Qed.

OPLSS - this is Adam's prefered version: Let's prove it!

Theorem hoare_itree_asgn' : ∀ P X a,
  ⦃P⦄ X := a ⦃ fun (σ:mem) ⇒ ∃ σ', σ = (X !-> (aeval σ' a) ; σ') ∧ P σ' ⦄.
Proof.
  unfold hoare_itree_triple.
  intros P X a σ H.
  cbn.
  norm.
  apply eutt_Ret. simpl.
  split. reflexivity.
  ∃ σ. split. reflexivity. assumption.
Qed.

Theorem hoare_itree_if : ∀ P Q (b:bexp) c₁ c₂,
  ⦃ P ∧ b ⦄ c₁ ⦃Q⦄ →
  ⦃ P ∧ ¬b⦄ c₂ ⦃Q⦄ →
  ⦃P⦄ if b then c₁ else c₂ end ⦃Q⦄.
Proof.
  intros P Q b c₁ c₂ H H₀.
  unfold hoare_itree_triple.
  intros σ HS.
  cbn.
  norm.
  cbn.
  destruct (beval σ b) eqn:HB.
  - apply H. intuition.
  - apply H₀. intuition. simpl in H₁. rewrite HB in H₁. inversion H₁.
Qed.

Theorem hoare_itree_while : ∀ P (b:bexp) c,
  ⦃P ∧ b⦄ c ⦃P⦄ →
  ⦃P⦄ while b do c end ⦃P ∧ ¬b⦄.
Proof.
  intros P b c H.
  unfold hoare_itree_triple.
  einit.
  ecofix CIH.
  intros σ HS.
  cbn.
  rewrite unfold_repeat.
  rewrite bind_bind.
  (* TODO SAZ: norm loops here for some reason. *)
  rewrite interp_state_bind.
  ebind.
  apply pbc_intro_h with (RU := fun '(st₁, b₁) '(st₂, b₂) ⇒ st₁ = st₂ ∧ st₁ = σ ∧ b₁ = b₂ ∧ b₁ = beval σ b).
  - norm.
    apply eqit_Ret. intuition.
  - intros.
    destruct u₁, u₂.
    destruct H₀ as [? [? [? ?]]].
    subst.
    simpl.
    destruct (beval σ b) eqn:HB.
    + norm.
      unfold hoare_itree_triple in H.
      specialize (H σ (conj HS HB)).
      ebind.
      econstructor. apply H.
      intros.
      destruct u₁, u₂.
      intuition. subst.
      norm.
      cbn. rewrite interp_state_tau. estep.
    + norm.
      estep. intuition.
      rewrite HB in H₀. inversion H₀.
Qed.

Theorem hoare_itree_consequence_pre : ∀ (P P' Q : Assertion) c,
  ⦃P'⦄ c ⦃Q⦄ →
  P ->> P' →
  ⦃P⦄ c ⦃Q⦄.
Proof.
  intros P P' Q c Htriple Hpre.
  unfold hoare_itree_triple in ×.
  intros σ H.
  apply Htriple.
  apply Hpre.
  assumption.
Qed.

Theorem hoare_itree_consequence_conj : ∀ (P Q Q' : Assertion) c,
  ⦃P⦄ c ⦃Q⦄ →
  ⦃P⦄ c ⦃Q'⦄ →
  ⦃P⦄ c ⦃Q ∧ Q'⦄.
Proof.
  intros P Q Q' c H₁ H₂.
  unfold hoare_itree_triple in ×.
  intros σ H.
  specialize (H₁ σ H).
  specialize (H₂ σ H).
  specialize (eutt_conj _ _ H₁ H₂).
  eapply eqit_mon; eauto.
  intros.
  destruct x₀, x₁. intuition.
Qed.

Theorem hoare_itree_consequence_post : ∀ (P Q Q' : Assertion) c,
  ⦃P⦄ c ⦃Q'⦄ →
  Q' ->> Q →
  ⦃P⦄ c ⦃Q⦄.
Proof.
  intros P P' Q Q' c Htriple Hpre Hpost.
  unfold hoare_itree_triple in ×.
  eapply eqit_mon with (RR := (fun '(σ1, _) '(σ2, _) ⇒ σ1 = σ2 ∧ Q σ1) ); eauto.
  intros.
  destruct x₀, x₁.
  intuition.
  apply c. assumption.
Qed.

Theorem hoare_itree_consequence : ∀ (P P' Q Q' : Assertion) c,
  ⦃P'⦄ c ⦃Q'⦄ →
  P ->> P' →
  Q' ->> Q →
  ⦃P⦄ c ⦃Q⦄.
Proof.
  intros P P' Q Q' c Htriple Hpre Hpost.
  apply hoare_itree_consequence_pre with (P' := P').
  - apply hoare_itree_consequence_post with (Q' := Q'); assumption.
  - assumption.
Qed.

Theorem hoare_itree_post_true : ∀ (P Q : Assertion) c,
  (∀ st, Q st) →
  ⦃P⦄ c ⦃Q⦄.
Proof.
  intros P Q c HQ. revert P.
  induction c.
  - intros P. eapply hoare_itree_consequence_post. apply hoare_itree_skip. red.
    intros. apply HQ.
  - intros P.
    unfold hoare_itree_triple. intros.
    cbn.
    norm.
    apply eutt_Ret. intuition.
  - intros P.
    eapply hoare_itree_seq. eapply IHc2. eapply IHc1.
  - intros P.
    eapply hoare_itree_if. apply IHc1.
    apply IHc2.
  - intros P.
    eapply hoare_itree_consequence_pre with (P' := Q).
    eapply hoare_itree_consequence_post.
    apply hoare_itree_while.
    apply IHc.
    intuition.
    intuition.
Qed.

Prove that if P holds in no state, then any triple with P as its precondition is valid.

Theorem hoare_itree_pre_false : ∀ (P Q : Assertion) c,
  (∀ st, ¬(P st)) →
  ⦃P⦄ c ⦃Q⦄.
Proof.
  intros P Q c H. unfold hoare_itree_triple.
  intros st HP.
  unfold not in H. apply H in HP.
  contradiction.
Qed.

Lemma semantic_preservation : ∀ (P Q : Assertion) (c₁ c₂ : com),
    (∀ σ, P σ → ℑ⟦c₁⟧σ ≈ ℑ⟦c₂⟧σ) →
    ⦃P⦄ c₁ ⦃Q⦄ →
    ⦃P⦄ c₂ ⦃Q⦄.
Proof.
  intros P Q c₁ c₂ EQ HC₁.
  unfold hoare_itree_triple in HC₁.
  intros σ HS.
  specialize (EQ σ HS).
  rewrite <- EQ.
  apply HC₁. assumption.
Qed.

Example hoare_itree_if_example :
  ⦃True⦄
    if X = 0
      then Y := 2
      else Y := X + 1
    end
  ⦃X ≤ Y⦄.
Proof.
  apply hoare_itree_if.
  - eapply hoare_itree_consequence_pre.
    + apply hoare_itree_asgn.
    + assertion_auto'.
  - eapply hoare_itree_consequence_pre.
    + apply hoare_itree_asgn.
    + assertion_auto'.
Qed.

Substitution

Fixpoint substitute_aexp (x:string) (ax:aexp) (a:aexp) : aexp :=
  match a with
  | ANum n ⇒ a
  | AId y ⇒ if String.eqb y x then ax else a
  | <{ a₁ + a₂ }> ⇒ <{ (substitute_aexp x ax a₁) + (substitute_aexp x ax a₂) }>
  | <{ a₁ - a₂ }> ⇒ <{ (substitute_aexp x ax a₁) - (substitute_aexp x ax a₂) }>
  | <{ a₁ × a₂ }> ⇒ <{ (substitute_aexp x ax a₁) × (substitute_aexp x ax a₂) }>
  end.

Eval compute in (substitute_aexp X (<{ Y + 2}>) (<{ X + Z }>)).

Lemma aexp_eval_semantics2 : ∀ a₁ a₂ σ,
    (aeval σ a₁ = aeval σ a₂) ↔
      ℑ ⟦ a₁ ⟧a σ ≈ ℑ ⟦ a₂ ⟧a σ.
Proof.
  intros.
  split.
  - intros H.
    norm.
    rewrite H.
    reflexivity.
  - intros H.
    unfold aexp_equiv in H.
    do 2 rewrite aexp_pure_aeval in H.
    apply eutt_Ret in H.
    inversion H.
    reflexivity.
Qed.

Lemma substitute_aexp_aeval : ∀ (x:string) ax a,
  ∀ σ (EQ : aeval σ <{ x }> = aeval σ ax),
    aeval σ a = aeval σ (substitute_aexp x ax a).
Proof.
  intros x ax a σ EQ.
  induction a; simpl; auto.
  destruct (String.eqb_spec x₀ x).
  - simpl in EQ. subst. assumption.
  - reflexivity.
Qed.

Lemma substitute_aexp_semantic : ∀ (x:string) ax a,
  ∀ σ (EQ: ℑ ⟦ <{ x }> ⟧a σ ≈ ℑ ⟦ ax ⟧a σ),
    ℑ ⟦ a ⟧a σ ≈ ℑ ⟦ substitute_aexp x ax a ⟧a σ.
Proof.
  intros x ax a σ HEQ.
  apply aexp_eval_semantics2.
  intros. apply substitute_aexp_aeval.
  apply aexp_eval_semantics2.
  assumption.
Qed.

Lemma bexp_eval_semantics : ∀ b₁ b₂ σ,
    (beval σ b₁ = beval σ b₂) ↔
      ℑ ⟦ b₁ ⟧b σ ≈ ℑ ⟦ b₂ ⟧b σ.
Proof.
  intros.
  split.
  - intros H.
    norm.
    rewrite H.
    reflexivity.
  - intros H.
    unfold bexp_equiv in H.
    do 2 rewrite bexp_pure_beval in H.
    apply eutt_Ret in H.
    inversion H.
    reflexivity.
Qed.

Fixpoint substitute_bexp (x:string) (ax:aexp) (b:bexp) : bexp :=
  match b with
  | <{true}> ⇒ b
  | <{false}> ⇒ b
  | <{a₁ = a₂}> ⇒ <{ (substitute_aexp x ax a₁) = (substitute_aexp x ax a₂) }>
  | <{a₁ ≠ a₂}> ⇒ <{ (substitute_aexp x ax a₁) ≠ (substitute_aexp x ax a₂) }>
  | <{a₁ ≤ a₂}> ⇒ <{ (substitute_aexp x ax a₁) ≤ (substitute_aexp x ax a₂) }>
  | <{a₁ > a₂}> ⇒ <{ (substitute_aexp x ax a₁) > (substitute_aexp x ax a₂) }>
  | <{~ b₁}> ⇒ <{~ (substitute_bexp x ax b₁) }>
  | <{b₁ && b₂}> ⇒ <{ (substitute_bexp x ax b₁) && (substitute_bexp x ax b₂) }>
  end.

Lemma substitute_bexp_beval : ∀ (x:string) ax b,
  ∀ σ (EQ : aeval σ <{ x }> = aeval σ ax),
    beval σ b = beval σ (substitute_bexp x ax b).
Proof.
  intros x ax b σ EQ.
  induction b; simpl; try reflexivity.
  - repeat rewrite <- (substitute_aexp_aeval x ax); auto.
  - repeat rewrite <- (substitute_aexp_aeval x ax); auto.
  - repeat rewrite <- (substitute_aexp_aeval x ax); auto.
  - repeat rewrite <- (substitute_aexp_aeval x ax); auto.
  - rewrite IHb. reflexivity.
  - rewrite IHb1, IHb2. reflexivity.
Qed.

Lemma substitute_bexp_semantic : ∀ (x:string) ax b,
  ∀ σ (EQ: ℑ ⟦ <{ x }> ⟧a σ ≈ ℑ ⟦ ax ⟧a σ),
    ℑ ⟦ b ⟧b σ ≈ ℑ ⟦ substitute_bexp x ax b ⟧b σ.
Proof.
  intros x ax a σ HEQ.
  apply bexp_eval_semantics.
  intros. apply substitute_bexp_beval.
  apply aexp_eval_semantics2.
  assumption.
Qed.

Fixpoint contains (x:string) (a:aexp) : bool :=
  match a with
  | ANum n ⇒ false
  | AId y ⇒ String.eqb y x
  | <{ a₁ + a₂ }> ⇒ (contains x a₁ || contains x a₂)%bool
  | <{ a₁ - a₂ }> ⇒ (contains x a₁ || contains x a₂)%bool
  | <{ a₁ × a₂ }> ⇒ (contains x a₁ || contains x a₂)%bool
  end.

Lemma contains_false_equiv: ∀ (y:string) a,
    contains y a = false →
    ∀ (σ:state) n, aeval σ a = aeval ( y !-> n ; σ ) a.
Proof.
  intros y.
  induction a; intros HC σ m; simpl in *; try reflexivity.
  - destruct (String.eqb_spec x y).
    + inversion HC.
    + rewrite t_update_neq; auto.
  - apply Bool.orb_false_elim in HC.
    destruct HC as [HA₁ HA₂].
    auto.
  - apply Bool.orb_false_elim in HC.
    destruct HC as [HA₁ HA₂].
    auto.
  - apply Bool.orb_false_elim in HC.
    destruct HC as [HA₁ HA₂].
    auto.
Qed.

Because commands are not pure, we can't blindly substitute.

Fixpoint substitute_com (x:string) (ax:aexp) (c:com) : (com × bool) :=
  match c with
  | <{ skip }> ⇒ (c, false)
  | <{ y := a }> ⇒
      let a' := substitute_aexp x ax a in
      (<{ y := a' }>, ((y =? x)%string || contains y ax)%bool)
  | <{ c₁ ; c₂ }> ⇒
      let '(c₁', stop) := substitute_com x ax c₁ in
      if stop
      then (<{ c₁' ; c₂ }>, stop)
      else
        let '(c₂', stop) := substitute_com x ax c₂ in
        (<{ c₁' ; c₂' }>, stop)
  | <{ if b then c₁ else c₂ end }> ⇒
      let '(c₁', stop1) := substitute_com x ax c₁ in
      let '(c₂', stop2) := substitute_com x ax c₂ in
      (<{ if (substitute_bexp x ax b) then c₁' else c₂' end }>, (stop1 || stop2)%bool)
  | <{ while b do c end }> ⇒ (<{ while b do c end }>, true)
  end.

Examples of when it is OK (or not) to substitute:

Eval compute in substitute_com X 0 <{ Z := 3; Y := X + X ; Y := X }>.
Eval compute in substitute_com X 0 <{ X := 3; X := X + X ; Y := X }>.

Define an invariant that says when we can safely substitute the expression <{ ax }> for <{ x }> in a state σ.

Definition subst_invariant x ax σ :=
aeval σ <{ x }> = aeval σ ax.

Define the relational post condition for reasoning about the results of substitution.

Definition post_condition x ax b (σ:state) :=
  fun σ1 σ2 ⇒
    σ1 = σ2
    ∧ (b = false → σ1 x = σ x ∧ aeval σ ax = aeval σ1 ax).

#[local]
Instance pose_condition_refl : ∀ x ax σ,
    Reflexive (post_condition x ax true σ).
Proof.
  intros.
  red.
  intros.
  unfold post_condition.
  split. reflexivity. intros. inversion H.
Qed.

Lemma post_condition_mono : ∀ x ax σ st₁ st₂ b₁ b₂,
    (b₁ = true → b₂ = true) →
    post_condition x ax b₁ σ st₁ st₂ →
    post_condition x ax b₂ σ st₁ st₂.
Proof.
  intros.
  unfold post_condition in ×.
  intuition.
  - destruct b₁.
    + rewrite H in H₀. inversion H₀. reflexivity.
    + apply H₂. reflexivity.
  - destruct b₁.
    + rewrite H in H₀. inversion H₀. reflexivity.
    + apply H₂. reflexivity.
Qed.

Lemma substitute_com_correct1 :
  ∀ x ax c c' b
    (HS: substitute_com x ax c = (c', b)),
    ∀ σ (P: subst_invariant x ax σ),
        eutt (prod_rel (post_condition x ax b σ) eq)
             (ℑ ⟦c⟧ σ)
             (ℑ ⟦c'⟧ σ).
Proof.
  intros x ax c.
  induction c; intros; simpl in HS; inversion HS; subst; simpl; norm.
  - apply eutt_Ret. unfold post_condition. auto.
  - apply eutt_Ret.
    simpl.
    constructor; auto.
    split; simpl; auto.
    + rewrite <- substitute_aexp_aeval; auto.
    + intros H.
      destruct (String.eqb_spec x₀ x).
      × subst. simpl in H. inversion H.
      × split.
       -- rewrite Bool.orb_false_l in H.
          unfold subst_invariant in P.
          apply t_update_neq.
          assumption.
       -- simpl in H.
          erewrite contains_false_equiv. reflexivity.
          assumption.
  - destruct (substitute_com x ax c₁).
    specialize (IHc1 c b₀ eq_refl σ P).
    destruct b₀.
    + inversion HS. subst.
      cbn.
      norm.
      eapply eutt_clo_bind.
      apply IHc1.
      intros u₁ u₂ HP.
      destruct u₁, u₂, u, u₀.
      cbn.
      destruct HP as [HM _].
      destruct HM. simpl in H.
      subst.
      reflexivity.
    + destruct (substitute_com x ax c₂).
      inversion HS. subst.
      cbn.
      norm.
      eapply eutt_clo_bind.
      apply IHc1.
      intros u₁ u₂ HP.
      destruct u₁, u₂, u, u₀.
      cbn.
      destruct HP as [[HM H]].
      simpl in HM.
      subst.
      specialize (H eq_refl).
      destruct H as [HM HE].
      simpl in ×.
      assert (subst_invariant x ax m₀).
      { unfold subst_invariant in ×. simpl. rewrite HM. rewrite <- HE. apply P. }
      specialize (IHc2 c₀ b eq_refl m₀ H).
      eapply eutt_subrel.
      2: { apply IHc2. }
      intros. unfold post_condition in H₁.
      inversion H₁.
      destruct a, u, b₀, u.
      constructor; auto.
      unfold post_condition.
      intuition.
  - destruct (substitute_com x ax c₁).
    destruct (substitute_com x ax c₂).
    cbn.
    inversion HS. subst.
    cbn.
    norm.
    cbn.
    rewrite <- substitute_bexp_beval; auto.
    destruct (beval σ b).
    + eapply eutt_subrel.
      2:{ apply IHc1; auto. }
      intros. constructor.
      eapply post_condition_mono.
      2: { apply H. }
      intros. intuition.
      inversion H; auto.
    + eapply eutt_subrel.
      2: { apply IHc2; auto. }
      intros.
      constructor.
      eapply post_condition_mono.
      2: { apply H. }
      intros. intuition.
      inversion H; auto.
  - reflexivity.
Qed.

Fixpoint com_append (c₁ c₂ : com) : com :=
  match c₁ with
  | <{ skip }> ⇒ c₂
  | <{ c₁₁ ; c₁₂}> ⇒ <{ c₁₁ ; (com_append c₁₂ c₂) }>
  | _ ⇒ <{ c₁ ; c₂ }>
  end.

(* TODO: This proof can be cleaned up using ImpEquiv *)
Lemma com_append_correct : ∀ c₁ c₂,
    com_append c₁ c₂ ≡ <{ c₁ ; c₂ }>.
Proof.
  induction c₁; intro c₂; simpl; try reflexivity.
  - rewrite skipL_sound. reflexivity.
  - rewrite seqA_sound. rewrite IHc1_2. reflexivity.
Qed.

#[global]
Instance Proper_com_append: Proper (com_eq ==> com_eq ==> com_eq) com_append.
Proof.
  intros c₁₁.
  destruct c₁₁; intros c₁₂ EQ₁ c₂₁ c₂₂ EQ₂; simpl.
  - rewrite com_append_correct. rewrite <- EQ₁. rewrite skipL_sound. assumption.
  - rewrite EQ₁. rewrite com_append_correct. rewrite EQ₂. reflexivity.
  - rewrite com_append_correct. rewrite com_append_correct. rewrite <- EQ₁.
    rewrite seqA_sound. rewrite EQ₂. reflexivity.
  - rewrite com_append_correct. rewrite <- EQ₁. rewrite EQ₂. reflexivity.
  - rewrite com_append_correct. rewrite <- EQ₁. rewrite EQ₂. reflexivity.
Qed.

Fixpoint com_assocR c : com :=
  match c with
  | <{ skip }> ⇒ c
  | <{ y := a }> ⇒ c
  | <{ c₁ ; c₂ }> ⇒
      let c₁' := com_assocR c₁ in
      let c₂' := com_assocR c₂ in
      com_append c₁' c₂'
  | <{ if b then c₁ else c₂ end }> ⇒
      let c₁' := com_assocR c₁ in
      let c₂' := com_assocR c₂ in
      <{ if b then c₁' else c₂' end }>
  | <{ while b do c end }> ⇒
      let c' := com_assocR c in
      <{ while b do c' end }>
  end.

Lemma com_assocR_correct : ∀ c,
    c ≡ com_assocR c.
Proof.
  induction c; simpl; try reflexivity.
  - rewrite <- IHc1. rewrite <- IHc2.
    rewrite com_append_correct.
    reflexivity.
  - rewrite <- IHc1. rewrite <- IHc2.
    reflexivity.
  - rewrite <- IHc. reflexivity.
Qed.

Fixpoint propagate_com (c:com) : com :=
  match c with
  | <{ skip }> ⇒ c
  | <{ y := a }> ⇒ c
  | <{ y := a ; c₂ }> ⇒
      let c₂' := propagate_com c₂ in
      if contains y a
      then <{ y := a ; c₂' }>
      else <{ y := a; fst (substitute_com y a c₂') }>
  | <{ c₁ ; c₂ }> ⇒
      let c₁' := propagate_com c₁ in
      let c₂' := propagate_com c₂ in
      <{ c₁' ; c₂' }>
  | <{ if b then c₁ else c₂ end }> ⇒
      let c₁' := propagate_com c₁ in
      let c₂' := propagate_com c₂ in
      <{ if b then c₁' else c₂' end }>
  | <{ while b do c end }> ⇒
      let c' := propagate_com c in
      <{ while b do c' end }>
  end.

Lemma subst_invariant_good : ∀ (x:string) a σ,
    contains x a = false →
    subst_invariant x a (x !-> aeval σ a; σ).
Proof.
  intros.
  unfold subst_invariant.
  eapply contains_false_equiv in H.
  rewrite <- H.
  symmetry.
  simpl.
  rewrite t_update_eq.
  reflexivity.
Qed.

Lemma substitute_com_subst : ∀ c x a σ,
    contains x a = false →
    ℑ ⟦ c ⟧ (x !-> aeval σ a; σ) ≈ ℑ ⟦ fst (substitute_com x a c) ⟧ (x !-> aeval σ a; σ).
Proof.
  intros.
  destruct (substitute_com x a c) eqn:HS.
  simpl.
  apply substitute_com_correct1 with (σ := (x !-> aeval σ a; σ)) in HS.
  eapply eutt_subrel.
  2: { apply HS. }
  intros.
  destruct a₀, u, b₀, u.
  inversion H₀; clear H₀.
  unfold post_condition in fst_rel.
  simpl in ×.
  intuition. subst. tauto.
  apply subst_invariant_good.
  assumption.
Qed.

Lemma propagate_com_sound : ∀ c,
    c ≊ (propagate_com c).
Proof.
  induction c.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl.
    destruct c₁.
    + simpl. rewrite <- IHc2. reflexivity.
    + destruct (contains x a) eqn:H.
      × rewrite <- IHc2. reflexivity.
      × intro.
        cbn.
        norm.
        cbn.
        eapply transitivity.
        apply IHc2.
        apply substitute_com_subst.
        assumption.
    + rewrite <- IHc1. rewrite <- IHc2. reflexivity.
    + simpl in ×.
      rewrite IHc1.
      rewrite <- IHc2.
      reflexivity.
    + simpl. rewrite <- IHc1. rewrite <- IHc2. reflexivity.
  - simpl. rewrite <- IHc1. rewrite <- IHc2. reflexivity.
  - simpl. rewrite <- IHc. reflexivity.
Qed.

Definition example : com :=
  <{ X := 4 + 5;
     Y := X;
     if ((X - Y) = (2 + 4)) then skip
     else Y := X end;
     if (0 ≤ (4 - (2 + 1))) then Y := 0
     else skip end;
     while (Y = 0) do
             X := X + 1
             end
    }>.

Eval compute in fold_constants_com (propagate_com example).

Example correct: example ≊ (fold_constants_com (propagate_com example)).
Proof.
rewrite fold_constants_com_sound.
apply propagate_com_sound.
Qed.

Fixpoint loop_unroll_while (n:nat) (b:bexp) (c:com) : com :=
  match n with
  | 0 ⇒ <{ while b do c end }>
  | S n ⇒ <{ if b then c ; (loop_unroll_while n b c) else skip end }>
  end.

Lemma loop_unroll_sound : ∀ (n:nat) (b:bexp) (c:com),
    <{ while b do c end }> ≡ loop_unroll_while n b c.
Proof.
  induction n; intros; simpl.
  - reflexivity.
  - rewrite <- IHn.
    apply loop_unroll1_sound_strong.
Qed.

Fixpoint loop_unroll_com n (c:com) : com :=
  match c with
  | <{ skip }> ⇒ c
  | <{ y := a }> ⇒ c
  | <{ c₁ ; c₂ }> ⇒
      let c₁' := loop_unroll_com n c₁ in
      let c₂' := loop_unroll_com n c₂ in
      <{ c₁' ; c₂' }>
  | <{ if b then c₁ else c₂ end }> ⇒
      let c₁' := loop_unroll_com n c₁ in
      let c₂' := loop_unroll_com n c₂ in
      <{ if b then c₁' else c₂' end }>
  | <{ while b do c end }> ⇒
      loop_unroll_while n b c
  end.

Lemma loop_unroll_com_sound : ∀ n c,
    c ≊ (loop_unroll_com n c).
Proof.
  induction c.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. rewrite <- IHc1. rewrite <- IHc2. reflexivity.
  - simpl. rewrite <- IHc1. rewrite <- IHc2. reflexivity.
  - simpl. unfold com_equiv. intros σ.
    apply com_eq_subrel_equiv.
    apply loop_unroll_sound.
Qed.

Fixpoint iterate_opt (n:nat) (opt : com → com) c :=
  match n with
  | 0 ⇒ c
  | S n ⇒ iterate_opt n opt (opt c)
  end.

Lemma iterate_opt_sound :
  ∀ n (opt : com → com) (OPTSOUND: ∀ c, c ≊ opt c) c,
    c ≊ iterate_opt n opt c.
Proof.
  intros n opt OPTSOUND.
  induction n; intros; simpl.
  - reflexivity.
  - rewrite <- IHn.
    apply OPTSOUND.
Qed.

Definition optimize (n:nat) (c:com) : com :=
let c' := com_assocR (loop_unroll_com n c) in
iterate_opt n (fun c ⇒ fold_constants_com (propagate_com c)) c'.

Lemma optimize_sound : ∀ n c,
    c ≊ optimize n c.
Proof.
  intros n c.
  unfold optimize.
  rewrite <- iterate_opt_sound.
  rewrite <- com_assocR_correct.
  apply loop_unroll_com_sound.
  intros c₀.
  rewrite fold_constants_com_sound.
  apply propagate_com_sound.
Qed.

Imp code for factorial for a specific number:

Definition fact_n n := <{ X := n ; fact_in_coq }>.

Definition fact_opt n :=
optimize (n+1) (fact_n n).

Definition fact_opt8 := fact_opt 8.
Eval compute in com_assocR fact_opt8.

Definition fact_opt5 := fact_opt 5.

Eval compute in fact_n 5.
Eval compute in fact_opt5.

Lemma fact_opt_correct : ∀ (n:nat),
    <{ X := n ; fact_in_coq }> ≊ fact_opt n.
Proof.
  intros n.
  unfold fact_in_coq.
  apply optimize_sound.
Qed.

Lemma store_store_elimination_correct : ∀ x a₁ a₂,
    (contains x a₂ = false) →
    <{ x := a₁ ; x := a₂ }> ≊ <{ x := a₂ }>.
Proof.
  intros x a₁ a₂ H σ.
  simpl.
  norm.
  cbn.
  apply eutt_Ret.
  specialize (contains_false_equiv x a₂ H) as EQ.
  rewrite <- EQ.
  rewrite t_update_shadow.
  reflexivity.
Qed.

Lemma asgn_commutes : ∀ (x y:string) a₁ a₂,
    (contains x a₂ = false) →
    (contains y a₁ = false) →
    x ≠ y →
    <{ x := a₁ ; y := a₂ }> ≊ <{ y := a₂; x := a₁ }>.
Proof.
  intros x y a₁ a₂ C₁ C₂ NEQ σ.
  simpl.
  norm.
  cbn.
  apply eutt_Ret.
  simpl.
  specialize (contains_false_equiv x a₂ C₁) as EQ₁.
  rewrite <- EQ₁.
  specialize (contains_false_equiv y a₁ C₂) as EQ₂.
  rewrite <- EQ₂.
  rewrite t_update_permute; auto.
Qed.

Eval compute in fact_opt5.

x1 = a₁ ; x₂ = a₂ ; x₃ = a₃ ; c x1 = x₃ x1 = a₁ ; x₂ = a₂ ; x₁ = a₃ ; c // x₁ <> x₂ /\ not (contains x₁ a₂) /\ not (contains x₂ a₃) x1 = a₁ ; x₁ = a₃ ; x₂ = a₂ ; c x1 = a₃ ; x₂ = a₂ ; c // not contains x₁ a₃

Fixpoint dead_store_elimination (c:com) : com :=
  match c with
  | <{ skip }> ⇒ c
  | <{ x := a }> ⇒ c
  | <{ x₁ := a₁; c₂ }> ⇒
      let c₂' := dead_store_elimination c₂ in
      match c₂' with
      | <{ x₂ := a₂ }> ⇒
          if ((String.eqb x₁ x₂)
              && negb (contains x₁ a₂))%bool
          then
            <{ x₂ := a₂ }>
          else
            <{ x₁ := a₁ ; c₂' }>
      | <{ x₂ := a₂ ; c₃' }> ⇒
          match c₃' with
          | <{ x₃ := a₃ }> ⇒
              if (String.eqb x₁ x₃
                  && negb (String.eqb x₂ x₃)
                  && negb (contains x₃ a₂)
                  && negb (contains x₂ a₃)
                  && negb (contains x₁ a₃))%bool
              then <{ x₃ := a₃ ; x₂ := a₂ }>
              else <{ x₁ := a₁ ; c₂' }>
          | <{ x₃ := a₃ ; c₄' }> ⇒
              if (String.eqb x₁ x₃
                  && negb (String.eqb x₂ x₃)
                  && negb (contains x₃ a₂)
                  && negb (contains x₂ a₃)
                  && negb (contains x₁ a₃))%bool
              then <{ x₃ := a₃ ; x₂ := a₂ ; c₄' }>
              else if ((String.eqb x₁ x₂)
                       && negb (String.eqb x₂ x₃)
                       && negb (contains x₁ a₂))%bool
                   then <{ x₂ := a₂ ; x₃ := a₃ ; c₄' }>
                   else <{ x₁ := a₁ ; c₂' }>
          | _ ⇒
              if ((String.eqb x₁ x₂)
                  && negb (contains x₁ a₂))%bool
              then
                <{ x₂ := a₂ ; c₃' }>
              else
                <{ x₁ := a₁ ; c₂' }>
          end
      | _ ⇒ <{ x₁ := a₁ ; c₂' }>
      end
  | <{ c₁ ; c₂ }> ⇒
      let c₂' := dead_store_elimination c₂ in
      <{ c₁ ; c₂' }>
  | <{ if b then c₁ else c₂ end }> ⇒
      let c₁' := dead_store_elimination c₁ in
      let c₂' := dead_store_elimination c₂ in
      <{ if b then c₁' else c₂' end }>
  | <{ while b do c end }> ⇒
      let c' := dead_store_elimination c in
      <{ while b do c' end }>
  end.

Eval compute in (dead_store_elimination <{ X := 0 ; Y := 1 ; Y := 2 ; skip }>).
Eval compute in (dead_store_elimination (com_assocR fact_opt5)).
Eval compute in (dead_store_elimination <{ Y := 120; Z := 0; skip }>).
Eval compute in (dead_store_elimination <{ Y:= 0; Y := 120; Z := 0; skip }>).

Lemma dead_store_elimination_correct :
  ∀ c,
    c ≊ (dead_store_elimination c).
Proof.
  induction c; simpl; try reflexivity.
  - destruct c₁; simpl; try (rewrite <- IHc2; try reflexivity).
    + destruct (dead_store_elimination c₂); simpl; try (rewrite <- IHc2; try reflexivity).
      × destruct (String.eqb_spec x x₀); subst; simpl.
        2: { rewrite IHc2. reflexivity. }
        destruct (contains x₀ a₀) eqn : HC; simpl.
        1: { rewrite IHc2. reflexivity. }
        rewrite IHc2. apply store_store_elimination_correct; auto.
      × destruct c₁; simpl; try (rewrite <- IHc2; try reflexivity).
        destruct c₃.
        -- destruct (String.eqb_spec x x₀); subst; simpl.
           2:{ rewrite IHc2. reflexivity. }
           destruct (contains x₀ a₀) eqn : HC; simpl.
           rewrite IHc2. reflexivity.
           rewrite IHc2. rewrite <- seqA_sound. rewrite store_store_elimination_correct; auto.
           reflexivity.
        -- destruct (String.eqb_spec x x₁); subst; simpl.
           2: { rewrite IHc2. reflexivity. }
           destruct (String.eqb_spec x₀ x₁); subst; simpl.
           1: { rewrite IHc2. reflexivity. }
           destruct (contains x₁ a₀) eqn : HC₁; simpl.
           1: { rewrite IHc2. reflexivity. }
           destruct (contains x₀ a₁) eqn : HC₂; simpl.
           1: { rewrite IHc2. reflexivity. }
           destruct (contains x₁ a₁) eqn : HC₃; simpl.
           1: { rewrite IHc2. reflexivity. }
           rewrite IHc2. rewrite asgn_commutes; auto.
           rewrite <- seqA_sound.
           rewrite store_store_elimination_correct; auto.
           reflexivity.
        -- destruct c3_1; simpl.
           ** destruct (String.eqb_spec x x₀); subst; simpl.
              2 : { rewrite IHc2. reflexivity. }
              destruct (contains x₀ a₀) eqn : HC₁; simpl.
              1 : { rewrite IHc2. reflexivity. }
              rewrite IHc2. rewrite <- seqA_sound.
              rewrite store_store_elimination_correct; auto.
              reflexivity.
           ** destruct (String.eqb_spec x x₁); subst; simpl.
              1: { destruct (String.eqb_spec x₀ x₁); subst; simpl.
                   destruct (String.eqb_spec x₁ x₁); subst; simpl.
                   2: { contradiction. }
                   rewrite IHc2. reflexivity.
                   destruct (contains x₁ a₀) eqn : HC; simpl.
                   destruct (String.eqb_spec x₁ x₀); subst; simpl.
                   destruct (contains x₀ a) eqn : HC₁; simpl.
                   contradiction.
                   contradiction.
                   rewrite <- IHc2. reflexivity.
                   destruct (contains x₀ a₁) eqn : HC₁; subst; simpl.
                   destruct (String.eqb_spec x₁ x₀); subst.
                   contradiction.
                   simpl.
                   rewrite <- IHc2. reflexivity.
                   destruct (contains x₁ a₁) eqn : HC₂; subst; simpl.
                   destruct (String.eqb_spec x₁ x₀); subst; simpl.
                   contradiction.
                   rewrite IHc2. reflexivity.
                   rewrite <- seqA_sound in IHc2.
                   rewrite asgn_commutes in IHc2; auto.
                   rewrite seqA_sound in IHc2.
                   rewrite IHc2.
                   rewrite <- seqA_sound.
                   rewrite store_store_elimination_correct; auto.
                   reflexivity. }
              destruct (String.eqb_spec x x₀); subst; simpl.
              2: { rewrite <- IHc2. reflexivity. }
              destruct (String.eqb_spec x₀ x₁); subst; simpl.
              rewrite IHc2. reflexivity.
              destruct (contains x₀ a₀) eqn : HC; simpl.
              rewrite IHc2. reflexivity.
              rewrite IHc2.
              rewrite <- seqA_sound.
              rewrite store_store_elimination_correct; auto.
              reflexivity.
           ** destruct (String.eqb_spec x x₀); simpl; subst.
              destruct (contains x₀ a₀) eqn : HC; simpl.
              rewrite IHc2. reflexivity.
              rewrite IHc2.
              rewrite <- seqA_sound.
              rewrite store_store_elimination_correct; auto.
              reflexivity.
              rewrite IHc2. reflexivity.
           ** destruct (String.eqb_spec x x₀); simpl; subst.
              destruct (contains x₀ a₀) eqn : HC; simpl.
              rewrite IHc2. reflexivity.
              rewrite IHc2.
              rewrite <- seqA_sound.
              rewrite store_store_elimination_correct; auto.
              reflexivity.
              rewrite IHc2. reflexivity.
           ** destruct (String.eqb_spec x x₀); simpl; subst.
              destruct (contains x₀ a₀) eqn : HC; simpl.
              rewrite IHc2. reflexivity.
              rewrite IHc2.
              rewrite <- seqA_sound.
              rewrite store_store_elimination_correct; auto.
              reflexivity.
              rewrite IHc2. reflexivity.
        -- destruct (String.eqb_spec x x₀); simpl; subst.
           destruct (contains x₀ a₀) eqn : HC; simpl.
           rewrite IHc2. reflexivity.
           rewrite IHc2.
           rewrite <- seqA_sound.
           rewrite store_store_elimination_correct; auto.
              reflexivity.
              rewrite IHc2. reflexivity.
        -- destruct (String.eqb_spec x x₀); simpl; subst.
           destruct (contains x₀ a₀) eqn : HC; simpl.
           rewrite IHc2. reflexivity.
           rewrite IHc2.
           rewrite <- seqA_sound.
           rewrite store_store_elimination_correct; auto.
              reflexivity.
              rewrite IHc2. reflexivity.
  - rewrite <- IHc1, <- IHc2. reflexivity.
  - rewrite <- IHc. reflexivity.
Qed.

Example opt_fact_sound :
  fact_n 5 ≊ <{ X := 5; Z:= 0; Y := 120; skip }>.
Proof.
  unfold fact_n.
  rewrite fact_opt_correct.
  rewrite dead_store_elimination_correct.
  reflexivity.
Qed.