finished proof for sum_frac & sum_frac_all

theories/vcgen/splitenv.v

@@ -28,11 +28,34 @@ Section splitenv.
      dloc_interp E (dLoc (ps_loc p)) ↦(ps_lvl p, ps_frc p) dval_interp E (ps_val p))%I.
 
 
-
   Lemma env_ps_dv_interp_app E s1 s2 :
     ((env_ps_dv_interp E s1 ∗ env_ps_dv_interp E s2))%I ≡ (env_ps_dv_interp E (s1 ++ s2))%I.
   Proof. by unfold env_ps_dv_interp; rewrite big_sepL_app. Qed.
 
+  Lemma env_ps_dv_interp_cons E p ps:
+  dloc_interp E (dLoc (ps_loc p)) ↦(ps_lvl p,ps_frc p) dval_interp E (ps_val p) ∗
+   env_ps_dv_interp E ps  ⊣⊢ env_ps_dv_interp E (p :: ps).
+  Proof.
+    unfold env_ps_dv_interp. rewrite !big_opL_cons. iStartProof.
+    iSplit; eauto with iFrame.
+  Qed.
+
+  Lemma env_ps_dv_interp_cons_perm E a b ps:
+    env_ps_dv_interp E (b :: a :: ps)  ⊣⊢
+    env_ps_dv_interp E (a :: b :: ps).
+  Proof.
+    unfold env_ps_dv_interp. rewrite !big_opL_cons. iStartProof.
+    iSplit; iIntros "(? & ? & ?)"; iFrame.
+  Qed.
+
+  Lemma env_ps_dv_interp_mono E b ps1 ps2:
+    (env_ps_dv_interp E ps1 -∗ env_ps_dv_interp E ps2) ⊢
+    (env_ps_dv_interp E (b :: ps1) -∗ env_ps_dv_interp E (b :: ps2)).
+  Proof.
+    iIntros "H (Hb & Hps)".
+    iFrame. iApply ("H" with "Hps").
+  Qed.
+
 
   Definition env_to_known_locs (Γls : env_ps) : env_locs := map fst Γls.
 

theories/vcgen/vcgen.v

@@ -106,14 +106,13 @@ Section vcg.
     | [] => Φ
     end.
 
-
   Fixpoint append_inhale_list (ps : env_ps_dv) (Φ : wp_expr) : wp_expr :=
     match ps with
     | (i, ((x,q), dv)) :: s' => InhaleKnown (dLoc i) dv x q (append_inhale_list s' Φ)
     | [] => Φ
     end.
 
-Lemma vcg_inhale_list_sound' E s t :
+  Lemma vcg_inhale_list_sound' E s t :
     wp_interp E (append_inhale_list s t) -∗ env_ps_dv_interp E s ∗ wp_interp E t.
   Proof.
     unfold env_ps_dv_interp.
@@ -176,15 +175,15 @@ Lemma vcg_inhale_list_sound' E s t :
        iFrame. iApply ("IH" $! e); first done. iFrame.
   Qed.
 
- Notation "l ↦( x , q ) v" :=
-    (mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l  ↦( x , q )  v").
-
+  Notation "l ↦( x , q ) v" :=
+  (mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l  ↦( x , q )  v").
 
 
-  Lemma find_and_remove_env_ps_dv_interp E ps i ps' x q dv :
-    find_and_remove ps (dLoc i) = Some (ps', (x,q,dv)) →
-    env_ps_dv_interp E ps ⊣⊢ env_ps_dv_interp E ps' ∗ (dloc_interp E (dLoc i)) ↦(x , q) (dval_interp E dv).
-  Proof. unfold env_ps_dv_interp. apply find_and_remove_big_sepL. Qed.
+ Lemma find_and_remove_env_ps_dv_interp E ps i ps' x q dv :
+   find_and_remove ps (dLoc i) = Some (ps', (x,q,dv)) →
+   env_ps_dv_interp E ps ⊣⊢
+   env_ps_dv_interp E ps' ∗ (dloc_interp E (dLoc i)) ↦(x , q) (dval_interp E dv).
+ Proof. unfold env_ps_dv_interp. apply find_and_remove_big_sepL. Qed.
 
 Instance dval_EqDecision : EqDecision dval.
  Proof. solve_decision. Defined.
@@ -201,23 +200,6 @@ Instance dval_EqDecision : EqDecision dval.
       end
     end.
 
-  Lemma env_ps_dv_interp_cons_perm E a b ps:
-    env_ps_dv_interp E (b :: a :: ps)  ⊣⊢
-    env_ps_dv_interp E (a :: b :: ps).
-  Proof.
-    unfold env_ps_dv_interp. rewrite !big_opL_cons. iStartProof.
-    iSplit; iIntros "(? & ? & ?)"; iFrame.
-  Qed.
-
-  Lemma env_ps_dv_interp_tail E b ps1 ps2:
-    (env_ps_dv_interp E ps1 -∗ env_ps_dv_interp E ps2) ⊢
-    (env_ps_dv_interp E (b :: ps1) -∗ env_ps_dv_interp E (b :: ps2)).
-  Proof.
-    iIntros "H (Hb & Hps)".
-    iFrame. iApply ("H" with "Hps").
-  Qed.
-
-
   Lemma sum_frac_correct E p ps:
     env_ps_dv_interp E (sum_frac ps p) ⊣⊢ env_ps_dv_interp E (p :: ps).
   Proof.
@@ -226,22 +208,25 @@ Instance dval_EqDecision : EqDecision dval.
              simplify_eq /=; iIntros "[H1 H2]"; iFrame);
         try eauto; destruct p as [i [[xi qi ] dvi]];
           repeat (case_bool_decide; simplify_eq /=; simpl).
-    - iIntros "H"; iSpecialize ("IH" with "H"). admit.
+    -  iIntros "H"; iSpecialize ("IH" with "H").
+       rewrite (app_comm_cons []).
+       rewrite -!env_ps_dv_interp_cons. iDestruct "IH" as "(H1 & $)". simpl.
+       rewrite mapsto_fractional. iDestruct "H1" as "(H1 & H2)". iFrame.
     - rewrite env_ps_dv_interp_cons_perm.
-      iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
+      iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
     - rewrite env_ps_dv_interp_cons_perm.
-      iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
+      iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
     - rewrite env_ps_dv_interp_cons_perm.
-      iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
-    - admit.
+      iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
+    - iIntros "H". iApply "IH". rewrite (app_comm_cons []).
+       rewrite -!env_ps_dv_interp_cons. iDestruct "H" as "(H1 & H2 & H3)". iFrame.
     - rewrite env_ps_dv_interp_cons_perm.
-      iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
+      iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
     - rewrite env_ps_dv_interp_cons_perm.
-      iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
+      iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
     - rewrite env_ps_dv_interp_cons_perm.
-      iApply env_ps_dv_interp_tail. iIntros "H". iApply ("IH" with "H").
-  Admitted.
-
+      iApply env_ps_dv_interp_mono. iIntros "H". iApply ("IH" with "H").
+  Qed.
 
   Definition sum_frac_all (ps: env_ps_dv) := fold_left (sum_frac) ps [].
 
@@ -346,7 +331,8 @@ Instance dval_EqDecision : EqDecision dval.
   Lemma vcg_sp_correct E s de s1 s2 dv R :
     vcg_sp E s de = Some (s1, s2, dv) →
     env_ps_dv_interp E s -∗
-    env_ps_dv_interp E s1 ∗ awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ env_ps_dv_interp E s2).
+      env_ps_dv_interp E s1 ∗
+      awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ env_ps_dv_interp E s2).
   Proof.
     revert s s1 s2 dv. induction de;
     iIntros (s s1 s2 dv Hsp) "Hs"; simplify_eq/=.