Commit a169f150 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

fix the proof fro sum_frac_all correctness

parent 4661f503
...@@ -217,6 +217,7 @@ Instance dval_EqDecision : EqDecision dval. ...@@ -217,6 +217,7 @@ Instance dval_EqDecision : EqDecision dval.
iFrame. iApply ("H" with "Hps"). iFrame. iApply ("H" with "Hps").
Qed. Qed.
Lemma sum_frac_correct E p ps: Lemma sum_frac_correct E p ps:
env_ps_dv_interp E (sum_frac ps p) env_ps_dv_interp E (p :: ps). env_ps_dv_interp E (sum_frac ps p) env_ps_dv_interp E (p :: ps).
Proof. Proof.
...@@ -252,9 +253,14 @@ Instance dval_EqDecision : EqDecision dval. ...@@ -252,9 +253,14 @@ Instance dval_EqDecision : EqDecision dval.
- done. - done.
- intros acc. simpl. specialize (IHps ((sum_frac acc a))). rewrite -IHps. - intros acc. simpl. specialize (IHps ((sum_frac acc a))). rewrite -IHps.
rewrite -env_ps_dv_interp_app. rewrite sum_frac_correct. rewrite -env_ps_dv_interp_app. rewrite sum_frac_correct.
assert (a :: ps ++ acc = ps ++ a :: acc). admit. rewrite !app_comm_cons.
rewrite H0. by rewrite !env_ps_dv_interp_app. rewrite (app_comm_cons [] acc).
Admitted. rewrite (app_comm_cons [] ps).
rewrite -!env_ps_dv_interp_app.
iStartProof. iSplit.
+ iIntros "[[H1 H2] H3]"; eauto with iFrame.
+ iIntros "(H1 & H2 & H3)". eauto with iFrame.
Qed.
Lemma sum_frac_all_correct E ps : Lemma sum_frac_all_correct E ps :
env_ps_dv_interp E ps env_ps_dv_interp E (sum_frac_all ps). env_ps_dv_interp E ps env_ps_dv_interp E (sum_frac_all ps).
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment