From 91a2d149011fd1bd9cc2a73380348e38eaa97970 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Mar 2016 17:05:47 +0100
Subject: [PATCH] Simplify and clean up wp_fix.

Shorten proofs and name variables that we introduce.
---
 program_logic/weakestpre_fix.v | 264 ++++++++++++++-------------------
 1 file changed, 108 insertions(+), 156 deletions(-)

diff --git a/program_logic/weakestpre_fix.v b/program_logic/weakestpre_fix.v
index 80c5862e9..3e6586224 100644
--- a/program_logic/weakestpre_fix.v
+++ b/program_logic/weakestpre_fix.v
@@ -1,172 +1,124 @@
 From Coq Require Import Wf_nat.
 From iris.program_logic Require Import weakestpre wsat.
+Local Hint Extern 10 (_ ≤ _) => omega.
+Local Hint Extern 10 (@eq coPset _ _) => set_solver.
+Local Hint Extern 10 (✓{_} _) =>
+  repeat match goal with
+  | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
+  end; solve_validN.
 
-(** This files provides an alternative definition of wp in terms of a
-    fixpoint of a contractive function, rather than a CoInductive type.
-    This is how we define wp on paper.
-    We show that the two versions are equivalent. *)
-
+(** This files provides an alternative definition of wp in terms of a fixpoint
+of a contractive function, rather than a CoInductive type. This is how we define
+wp on paper.  We show that the two versions are equivalent. *)
 Section def.
-  Context {Λ : language} {Σ : iFunctor}.
-  Local Notation iProp := (iProp Λ Σ).
-
-  Definition coPsetC := leibnizC (coPset).
+Context {Λ : language} {Σ : iFunctor}.
+Local Notation iProp := (iProp Λ Σ).
+Local Notation coPsetC := (leibnizC (coPset)).
 
-  Definition pre_wp_def (wp : coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp)
-             (E : coPset) (e1 : expr Λ) (Φ : valC Λ -n> iProp)
-             (n : nat) (r1 : iRes Λ Σ) : Prop :=
-    ∀ rf k Ef σ1, 0 ≤ k < n → E ∩ Ef = ∅ →
-                  wsat (S k) (E ∪ Ef) σ1 (r1 ⋅ rf) →
-                  (∀ v, to_val e1 = Some v →
-                        ∃ r2, Φ v (S k) r2 ∧ wsat (S k) (E ∪ Ef) σ1 (r2 ⋅ rf)) ∧
-                  (to_val e1 = None → 0 < k →
-                   reducible e1 σ1 ∧
-                   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef →
-                      ∃ r2 r2',
-                        wsat k (E ∪ Ef) σ2 (r2 ⋅ r2' ⋅ rf) ∧
-                        wp E e2 Φ k r2 ∧
-                        default True ef (λ ef, wp ⊤ ef (cconst True%I) k r2'))).
+Program Definition wp_pre
+    (wp : coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp)
+    (E : coPset) (e1 : expr Λ) (Φ : valC Λ -n> iProp) :  iProp :=
+  {| uPred_holds n r1 := ∀ rf k Ef σ1,
+       0 ≤ k < n → E ∩ Ef = ∅ →
+       wsat (S k) (E ∪ Ef) σ1 (r1 ⋅ rf) →
+       (∀ v, to_val e1 = Some v →
+         ∃ r2, Φ v (S k) r2 ∧ wsat (S k) (E ∪ Ef) σ1 (r2 ⋅ rf)) ∧
+       (to_val e1 = None → 0 < k →
+         reducible e1 σ1 ∧
+         (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef →
+           ∃ r2 r2',
+             wsat k (E ∪ Ef) σ2 (r2 ⋅ r2' ⋅ rf) ∧
+             wp E e2 Φ k r2 ∧
+             default True ef (λ ef, wp ⊤ ef (cconst True%I) k r2'))) |}.
+Next Obligation.
+  intros wp E e1 Φ n r1 r1' Hwp Hr1 rf k Ef σ1 ???; simpl in *.
+  destruct (Hwp rf k Ef σ1); auto.
+  by rewrite (dist_le _ _ _ _ Hr1); last omega.
+Qed.
+Next Obligation.
+  intros wp E e1 Φ n1 n2 r1 ? Hwp [r2 ?] ?? rf k Ef σ1 ???; setoid_subst.
+  destruct (Hwp (r2 ⋅ rf) k Ef σ1) as [Hval Hstep]; rewrite ?assoc; auto.
+  split.
+  - intros v Hv. destruct (Hval v Hv) as [r3 [??]].
+    exists (r3 â‹… r2). rewrite -assoc. eauto using uPred_weaken, cmra_included_l.
+  - intros ??. destruct Hstep as [Hred Hpstep]; auto.
+    split; [done|]=> e2 σ2 ef ?.
+    edestruct Hpstep as (r3&r3'&?&?&?); eauto.
+    exists r3, (r3' â‹… r2); split_and?; auto.
+    + by rewrite assoc -assoc.
+    + destruct ef; simpl in *; eauto using uPred_weaken, cmra_included_l.
+Qed.
 
-  Program Definition pre_wp
-          (wp : coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp)
-          (E : coPset) (e1 : expr Λ) (Φ : valC Λ -n> iProp) :  iProp :=
-    {| uPred_holds := pre_wp_def wp E e1 Φ |}.
-  Next Obligation.
-    intros ????? r1 r1' Hwp EQr.
-    intros ???? Hk ??. edestruct Hwp as [Hval Hstep]; [done..| |].
-    { eapply wsat_ne'; last done. apply (dist_le n); last omega.
-      by rewrite EQr. }
-    split; done.
-  Qed.
-  Next Obligation.
-    intros ???? n1 n2 r1 r2 Hwp [r3 Hr] Hn Hvalid.
-    intros ???? Hk ??. edestruct (Hwp (r3 â‹… rf) k) as [Hval Hstep]; [|done..| |].
-    { omega. }
-    {  eapply wsat_ne'; last done. by rewrite Hr assoc. }
-    split.
-    - intros v Hv. destruct (Hval v Hv) as [r4 [HΦ Hw]].
-      exists (r4 â‹… r3). split.
-      + eapply uPred_weaken; first exact: HΦ; eauto.
-        * by eexists.
-        * apply wsat_valid in Hw; last done. solve_validN.
-      + by rewrite -assoc.
-    - intros ??. edestruct Hstep as [Hred Hpstep]; [done..|].
-      split; first done. intros ????.
-      edestruct Hpstep as (r4 & r4' & Hw & He2 & Hef); [done..|].
-      exists r4, (r4' â‹… r3). split_and?.
-      + move: Hw. by rewrite -!assoc.
-      + done.
-      + destruct ef; last done.
-        eapply uPred_weaken; first exact: Hef; eauto.
-        * by eexists.
-        * apply wsat_valid in Hw; last omega. solve_validN.
-  Qed.
+Lemma wp_pre_contractive' n E e Φ1 Φ2 r
+    (wp1 wp2 : coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp) :
+  (∀ i : nat, i < n → wp1 ≡{i}≡ wp2) → Φ1 ≡{n}≡ Φ2 →
+  wp_pre wp1 E e Φ1 n r → wp_pre wp2 E e Φ2 n r.
+Proof.
+  intros HI HΦ Hwp rf k Ef σ1 ???.
+  destruct (Hwp rf k Ef σ1) as [Hval Hstep]; auto.
+  split.
+  { intros v ?. destruct (Hval v) as (r2&?&?); auto.
+    exists r2. split; [apply HΦ|]; auto. }
+  intros ??. destruct Hstep as [Hred Hpstep]; auto.
+  split; [done|]=> e2 σ2 ef ?.
+  destruct (Hpstep e2 σ2 ef) as (r2&r2'&?&?&?); [done..|].
+  exists r2, r2'; split_and?; auto.
+  - apply HI with k; auto.
+    assert (wp1 E e2 Φ2 ≡{n}≡ wp1 E e2 Φ1) as HwpΦ by (by rewrite HΦ).
+    apply HwpΦ; auto.
+  - destruct ef as [ef|]; simpl in *; last done.
+    apply HI with k; auto.
+Qed.
+Instance wp_pre_ne n wp E e : Proper (dist n ==> dist n) (wp_pre wp E e).
+Proof.
+  split; split;
+    eapply wp_pre_contractive'; eauto using dist_le, (symmetry (R:=dist _)).
+Qed.
 
-  Local Instance pre_wp_ne n wp E e :
-    Proper (dist n ==> dist n) (pre_wp wp E e).
-  Proof.
-    cut (∀ n Φ1 Φ2, Φ1 ≡{n}≡ Φ2 → ∀ r,
-              pre_wp wp E e Φ1 n r → pre_wp wp E e Φ2 n r).
-    { intros H Φ1 Φ2 EQΦ. split; split; eapply H.
-      - eauto using dist_le.
-      - symmetry. eauto using dist_le. }
-    clear n. intros n Φ1 Φ2 EQΦ r Hwp.
-    intros ???? Hk ??. edestruct Hwp as [Hval Hstep]; [done..|].
-    split.
-    - intros ??. edestruct Hval as [r2 [HΦ Hw]]; [done..|].
-      exists r2. split; last done. apply EQΦ, HΦ.
-      + omega.
-      + apply wsat_valid in Hw; last omega. solve_validN.
-    - intros ??. edestruct Hstep as [Hred Hpstep]; [done..|].
-      split; first done. intros ????.
-      edestruct Hpstep as (r2 & r2' & Hw & He2 & Hef); [done..|].
-      exists r2, r2'. split_and?; try done.
-      eapply uPred_holds_ne, He2.
-      + apply (dist_le n); last omega. by rewrite -EQΦ.
-      + apply wsat_valid in Hw; last omega. solve_validN.
-  Qed.
+Definition wp_preC
+    (wp : coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp) :
+    coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp :=
+  CofeMor (λ E : coPsetC, CofeMor (λ e : exprC Λ, CofeMor (wp_pre wp E e))).
 
-  Definition pre_wp_mor wp : coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp :=
-    CofeMor (λ E : coPsetC, CofeMor (λ e : exprC Λ, CofeMor (pre_wp wp E e))).
+Local Instance pre_wp_contractive : Contractive wp_preC.
+Proof.
+  split; split; eapply wp_pre_contractive'; auto using (symmetry (R:=dist _)).
+Qed.
 
-  Local Instance pre_wp_contractive : Contractive pre_wp_mor.
-  Proof.
-    cut (∀ n (wp1 wp2 : coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp),
-           (∀ i : nat, i < n → wp1 ≡{i}≡ wp2) → ∀ E e Φ r,
-              pre_wp wp1 E e Φ n r → pre_wp wp2 E e Φ n r).
-    { intros H n wp1 wp2 HI. split; split; eapply H; intros.
-      - apply HI. omega.
-      - symmetry. apply HI. omega. }
-    intros n wp1 wp2 HI E e1 Φ r1 Hwp.
-    intros ???? Hk ??. edestruct Hwp as [Hval Hstep]; [done..|].
-    split; first done.
-    intros ??. edestruct Hstep as [Hred Hpstep]; [done..|].
-    split; first done. intros ????.
-    edestruct Hpstep as (r2 & r2' & Hw & He2 & Hef); [done..|].
-    exists r2, r2'. split_and?; try done.
-    - eapply uPred_holds_ne, He2.
-      + apply HI. omega.
-      + apply wsat_valid in Hw; last omega. solve_validN.
-    - destruct ef; last done. eapply uPred_holds_ne, Hef.
-      + apply HI. omega.
-      + apply wsat_valid in Hw; last omega. solve_validN.
-  Qed.
+Definition wp_fix : coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp := 
+  fixpoint wp_preC.
 
-  Definition wp_fix : coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp := 
-    fixpoint pre_wp_mor.
+Lemma wp_fix_unfold E e Φ : wp_fix E e Φ ⊣⊢ wp_preC wp_fix E e Φ.
+Proof. by rewrite /wp_fix -fixpoint_unfold. Qed.
 
-  Lemma wp_fix_unfold E e Φ : pre_wp_mor wp_fix E e Φ ⊣⊢ wp_fix E e Φ.
-  Proof. rewrite -fixpoint_unfold. done. Qed.
-
-  Lemma wp_fix_sound (E : coPset) (e : expr Λ) (Φ : val Λ -> iProp)
-    (Hproper : ∀ n, Proper (dist n ==> dist n) (Φ : valC Λ -> iProp)) :
-    wp_fix E e (@CofeMor _ _ _ Hproper) ⊢ wp E e Φ.
-  Proof.
-    split. rewrite wp_eq /wp_def {2}/uPred_holds.
-    intros n. revert E e Φ Hproper.
-    induction n as [n IH] using lt_wf_ind=> E e Φ Hproper r1 Hr1 Hwp.
+Lemma wp_fix_correct E e (Φ : valC Λ -n> iProp) : wp_fix E e Φ ⊣⊢ wp E e Φ.
+Proof.
+  split=> n r Hr. rewrite wp_eq /wp_def {2}/uPred_holds.
+  split; revert r E e Φ Hr.
+  - induction n as [n IH] using lt_wf_ind=> r1 E e Φ ? Hwp.
     case EQ: (to_val e)=>[v|].
-    - rewrite -(of_to_val _ _ EQ) {IH}. constructor. rewrite pvs_eq.
-      intros rf k Ef σ ???. destruct k; first (exfalso; omega).
+    + rewrite -(of_to_val _ _ EQ) {IH}. constructor. rewrite pvs_eq.
+      intros rf [|k] Ef σ ???; first omega.
       apply wp_fix_unfold in Hwp; last done.
-      edestruct (Hwp rf k Ef σ); eauto with omega; set_solver.
-    - constructor; first done. intros ???? Hk ??.
+      destruct (Hwp rf k Ef σ); auto.
+    + constructor; [done|]=> rf k Ef σ1 ???.
       apply wp_fix_unfold in Hwp; last done.
-      edestruct Hwp as [Hval Hstep]; [|done..|]; first omega.
-      edestruct Hstep as [Hred Hpstep]; [done|omega|]. clear Hstep.
-      split; first done. intros ????.
-      edestruct Hpstep as (r2 & r2' & Hw & He2 & Hef); [done..|].
-      exists r2, r2'. split_and?; first done.
-      + apply: IH; last done; first omega.
-        apply wsat_valid in Hw; last omega. solve_validN.
-      + intros e' ?. subst ef. apply: IH; last done; first omega.
-        apply wsat_valid in Hw; last omega. solve_validN.
-  Qed.
-
-  Lemma wp_fix_complete (E : coPset) (e : expr Λ) (Φ : val Λ -> iProp)
-    (Hproper : ∀ n, Proper (dist n ==> dist n) (Φ : valC Λ -> iProp)) :
-    wp E e Φ ⊢ wp_fix E e (@CofeMor _ _ _ Hproper).
-  Proof.
-    split. rewrite wp_eq /wp_def {1}/uPred_holds.
-    intros n. revert E e Φ Hproper.
-    induction n as [n IH] using lt_wf_ind=> E e Φ Hproper r1 Hr1 Hwp.
-    apply wp_fix_unfold; first done.
-    intros rf k Ef σ1 ???. split.
-    - intros ? Hval. destruct Hwp as [??? Hpvs|]; last by destruct (to_val e1).
+      destruct (Hwp rf k Ef σ1) as [Hval [Hred Hpstep]]; auto.
+      split; [done|]=> e2 σ2 ef ?.
+      destruct (Hpstep e2 σ2 ef) as (r2&r2'&?&?&?); [done..|].
+      exists r2, r2'; split_and?; auto.
+      intros ? ->. change (weakestpre.wp_pre ⊤ (cconst True%I) e' k r2'); eauto.
+  - induction n as [n IH] using lt_wf_ind=> r1 E e Φ ? Hwp.
+    apply wp_fix_unfold; [done|]=> rf k Ef σ1 ???. split.
+    + intros v Hval.
+      destruct Hwp as [??? Hpvs|]; rewrite ?to_of_val in Hval; simplify_eq/=.
       rewrite pvs_eq in Hpvs.
-      edestruct (Hpvs rf (S k) Ef σ1) as (r2 & ? & ?); [omega|set_solver|done|].
-      exists r2. split; last done. rewrite to_of_val in Hval.
-      by simplify_option_eq.
-    - intros Hval ?. destruct Hwp as [|??? _ Hwp].
-      { by rewrite to_of_val in Hval. }
-      edestruct Hwp as [? Hpstep]; try done; first omega; [].
-      split; first done.
-      intros ????. edestruct Hpstep as (r2 & r2' & Hw & He2 & Hef); [done..|].
-      exists r2, r2'. split_and?; first done.
-      + apply IH, He2; first omega.
-        apply wsat_valid in Hw; last omega. solve_validN.
-      + destruct ef; last done.
-        apply IH, Hef; first omega; last done.
-        apply wsat_valid in Hw; last omega. solve_validN.
-  Qed.
+      destruct (Hpvs rf (S k) Ef σ1) as (r2&?&?); eauto.
+    + intros Hval ?.
+      destruct Hwp as [|???? Hwp]; rewrite ?to_of_val in Hval; simplify_eq/=.
+      edestruct (Hwp rf k Ef σ1) as [? Hpstep]; auto.
+      split; [done|]=> e2 σ2 ef ?.
+      destruct (Hpstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
+      exists r2, r2'. destruct ef; simpl; auto.
+Qed.
 End def.
-- 
GitLab