Commit 6780792e authored by Dan Frumin's avatar Dan Frumin
Browse files

Finish with `denv_lookup_interp`.

parent 73ddad1f
......@@ -49,19 +49,6 @@ Section denv.
| S i => None :: denv_singleton i lv q dv
end.
Fixpoint denv_lookup (i : nat) (m : denv) : option (frac * dval) :=
match m with
| [] => None
| dio :: m' =>
match i with
| O =>
''(DenvItem lv q dv) dio;
guard (lv = ULvl);
Some (q, dv)
| S i => denv_lookup i m'
end
end.
Fixpoint denv_insert (i : nat) (x: lvl) (q: frac) (dv: dval) (m: denv) {struct m} : denv :=
match m with
| [] => denv_singleton i x q dv
......@@ -101,6 +88,10 @@ Section denv.
end
end.
Definition denv_lookup (i : nat) (m : denv) : option (frac * dval) :=
''(m', q, dv) denv_delete_full_aux i m;
Some (q, dv).
Definition denv_delete_full (i : nat) (m : denv) : option (denv * dval) :=
''(m', q, dv) denv_delete_full_aux i m;
guard (q = 1)%Qp;
......@@ -232,11 +223,6 @@ Section denv_spec.
denv_interp E (denv_insert i x q dv m).
Proof. by rewrite -!denv_interp_aux_0 denv_insert_interp_aux. Qed.
Lemma denv_lookup_interp E i q dv m:
denv_lookup i m = Some (q, dv)
m', denv_interp E m dloc_interp E (dLoc i) C{q} dval_interp E dv denv_interp E m'.
Proof. Admitted.
Lemma denv_merge_interp_aux E m1 m2 k :
denv_interp_aux E m1 k denv_interp_aux E m2 k denv_interp_aux E (denv_merge m1 m2) k.
Proof.
......@@ -295,6 +281,31 @@ Section denv_spec.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega. done.
Qed.
Lemma denv_delete_frac_interp_aux_flip E i k m m' q dv :
denv_delete_frac i m = Some (m', q, dv)
(denv_interp_aux E m' k dloc_interp E (dLoc (k+i)) C{q} dval_interp E dv)
- denv_interp_aux E m k.
Proof.
iInduction m as [|dio m] "IHm" forall (i k m').
- simpl. iIntros (Hz). inversion Hz.
- iIntros (Ha). simpl in Ha.
destruct i as [|i].
+ destruct dio as [[x q' dv']|]; simplify_eq/=.
case_option_guard; simplify_eq/=.
iIntros "[[Hl1 Hl2] Hm] /=". by iFrame.
+ destruct (denv_delete_frac i m) as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=.
iIntros "[[$ Hmf] Hl]".
iSpecialize ("IHm" $! _ (k+1)%nat with "[] [-]"); eauto.
{ assert ((k+1+i)%nat = (k + S i)%nat) as -> by omega. iFrame "Hl".
iApply (big_sepL_mono with "Hmf").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega.
done. }
iApply (big_sepL_mono with "IHm").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega. done.
Qed.
Lemma denv_delete_frac_interp E i m m' q dv :
denv_delete_frac i m = Some (m', q, dv)
denv_interp E m denv_interp E m' dloc_interp E (dLoc i) C{q} dval_interp E dv.
......@@ -325,6 +336,31 @@ Section denv_spec.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega. done.
Qed.
Lemma denv_delete_full_interp_aux_flip E i k m m' q dv :
denv_delete_full_aux i m = Some (m', q, dv)
denv_interp_aux E m' k dloc_interp E (dLoc (k+i)) C{q} dval_interp E dv
denv_interp_aux E m k.
Proof.
iInduction m as [|dio m] "IHm" forall (i k m').
- simpl. iIntros (Hz). inversion Hz.
- iIntros (Ha). simpl in Ha.
destruct i as [|i].
+ destruct dio as [[x q' dv']|]; simplify_eq/=.
case_option_guard; simplify_eq/=.
iIntros "[[Hl1 Hl2] Hm] /=". by iFrame.
+ destruct (denv_delete_full_aux i m) as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=.
iIntros "[[$ Hm] Hl]".
iSpecialize ("IHm" $! i (k+1)%nat with "[] [-]"); eauto.
* assert ((k+1+i)%nat = (k + S i)%nat) as -> by omega. iFrame "Hl".
iApply (big_sepL_mono with "Hm").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega.
done.
* iApply (big_sepL_mono with "IHm").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega. done.
Qed.
Lemma denv_delete_full_interp E i m m' dv :
denv_delete_full i m = Some (m', dv)
denv_interp E m denv_interp E m' dloc_interp E (dLoc i) C{1} dval_interp E dv.
......@@ -335,6 +371,19 @@ Section denv_spec.
by rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux.
Qed.
Lemma denv_lookup_interp E i q dv m:
denv_lookup i m = Some (q, dv)
m', denv_interp E m dloc_interp E (dLoc i) C{q} dval_interp E dv denv_interp E m'.
Proof.
rewrite /denv_lookup=>?.
destruct (denv_delete_full_aux i m) as [[[mf qf] dvf]|] eqn:Hm; simplify_eq/=.
exists mf. iSplit.
- rewrite -!denv_interp_aux_0.
iIntros "Hm". iDestruct (denv_delete_full_interp_aux with "Hm") as "[$ $]"; eauto.
- rewrite -!denv_interp_aux_0.
iIntros "[Hl Hm]". iApply denv_delete_full_interp_aux_flip; eauto with iFrame.
Qed.
Lemma denv_delete_frac_2_interp E i mIn mOut mIn1 mOut1 q dv :
denv_delete_frac_2 i mIn mOut = Some (mIn1, mOut1, q, dv)
denv_interp E mIn -
......
Markdown is supported
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