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

80 lines in denv.v

parent 450428f7
......@@ -36,17 +36,21 @@ Section denv.
| None :: m' => denv_wf E m'
end.
Definition denv_item_opt_merge (dio1 dio2 : option denv_item) : option denv_item :=
Definition denv_item_opt_merge
(dio1 dio2 : option denv_item) : option denv_item :=
match dio1, dio2 with
| None, dio | dio, None => dio
| Some di1, Some di2 =>
Some (DenvItem (denv_level di1 denv_level di2) ((denv_frac di1) + (denv_frac di2)) (denv_dval di1))
Some (DenvItem (denv_level di1 denv_level di2)
((denv_frac di1) + (denv_frac di2))
(denv_dval di1))
end.
Fixpoint denv_merge (m1 m2 : denv) : denv :=
match m1, m2 with
| m, [] | [], m => m
| dio1 :: m1', dio2 :: m2' => denv_item_opt_merge dio1 dio2 :: denv_merge m1' m2'
| dio1 :: m1', dio2 :: m2' =>
denv_item_opt_merge dio1 dio2 :: denv_merge m1' m2'
end.
Definition denv_stack_merge (ms : list denv) : denv :=
......@@ -58,20 +62,23 @@ Section denv.
| S i => None :: denv_singleton i lv q dv
end.
Fixpoint denv_insert (i : nat) (x: lvl) (q: frac) (dv: dval) (m: denv) {struct m} : denv :=
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
| dio :: m' =>
match i with
| O => match dio with
| None => Some (DenvItem x q dv) :: m'
| Some di => Some (DenvItem ((denv_level di)x) ((denv_frac di) + q) dv) :: m'
| Some di =>
Some (DenvItem ((denv_level di)x) ((denv_frac di) + q) dv) :: m'
end
| S i => dio :: denv_insert i x q dv m'
end
end.
Fixpoint denv_delete_frac (i : nat) (m : denv) {struct m} : option (denv * frac * dval) :=
Fixpoint denv_delete_frac (i : nat) (m : denv) {struct m}
: option (denv * frac * dval) :=
match m with
| [] => None
| dio :: m' =>
......@@ -84,17 +91,20 @@ Section denv.
end
end.
Fixpoint denv_delete_frac_stack (i : nat) (ms : list denv) : option (list denv * frac * dval) :=
Fixpoint denv_delete_frac_stack (i : nat) (ms : list denv)
: option (list denv * frac * dval) :=
match ms with
| [] => None
| m :: ms' =>
match denv_delete_frac i m with
| Some (m', q, dv) => Some (m'::ms', q, dv)
| None => ''(ms1, q, dv) denv_delete_frac_stack i ms'; Some (m::ms1, q, dv)
| None =>
''(ms1, q, dv) denv_delete_frac_stack i ms'; Some (m::ms1, q, dv)
end
end.
Fixpoint denv_delete_full_aux (i : nat) (m : denv) {struct m} : option (denv * frac * dval) :=
Fixpoint denv_delete_full_aux (i : nat) (m : denv) {struct m} :
option (denv * frac * dval) :=
match m with
| [] => None
| dio :: m' =>
......@@ -107,7 +117,8 @@ Section denv.
end
end.
Fixpoint denv_delete_full_stack_aux (i : nat) (ms : list denv) : option (list denv * frac * dval) :=
Fixpoint denv_delete_full_stack_aux (i : nat) (ms : list denv)
: option (list denv * frac * dval) :=
match ms with
| [] => None
| m::ms' =>
......@@ -115,7 +126,8 @@ Section denv.
| None, None => None
| None, Some (ms1, q1, dv1) => Some (m::ms1, q1, dv1)
| Some (m1, q2, dv2), None => Some (m1::ms', q2, dv2)
| Some (m1, q2, dv2), Some (ms1, q1, dv1) => Some (m1::ms1, (q1+q2)%Qp, dv2)
| Some (m1, q2, dv2), Some (ms1, q1, dv1) =>
Some (m1::ms1, (q1+q2)%Qp, dv2)
end
end.
......@@ -131,15 +143,18 @@ Section denv.
Definition denv_unlock (m: denv) : denv :=
map (λ dio, ''(DenvItem _ q dv) dio; Some (DenvItem ULvl q dv)) m.
Definition denv_delete_full_2 (i : nat) (ms : list denv) (m : denv) : option (list denv * denv * dval) :=
Definition denv_delete_full_2 (i : nat) (ms : list denv) (m : denv)
: option (list denv * denv * dval) :=
match denv_delete_full_stack_aux i ms, denv_delete_full_aux i m with
| None, Some (m', q, dv) => guard (q = 1)%Qp; Some (ms, m', dv)
| Some (ms', q, dv), None => guard (q = 1)%Qp; Some (ms', m, dv)
| Some (ms', q1, dv), Some (m', q2, _) => guard (q1 + q2 = 1)%Qp; Some (ms', m', dv)
| Some (ms', q1, dv), Some (m', q2, _) =>
guard (q1 + q2 = 1)%Qp; Some (ms', m', dv)
| _, _ => None
end.
Definition denv_delete_frac_2 (i : nat) (ms : list denv) (m : denv) : option (list denv * denv * frac * dval) :=
Definition denv_delete_frac_2 (i : nat) (ms : list denv) (m : denv)
: option (list denv * denv * frac * dval) :=
match denv_delete_frac_stack i ms with
| Some (ms', q, dv) => Some (ms', m, q, dv)
| None =>
......@@ -168,7 +183,8 @@ Section denv_spec.
Fixpoint denv_stack_interp (ms1 ms2 : list denv) E (P : iProp Σ) :=
match ms1,ms2 with
| m::ms,m'::ms' => denv_stack_interp ms ms' E (denv_interp E m - denv_interp E m' P)
| m::ms,m'::ms' =>
denv_stack_interp ms ms' E (denv_interp E m - denv_interp E m' P)
| [],[] => P
| _, _ => False
end%I.
......@@ -180,7 +196,7 @@ Section denv_spec.
Definition denv_interp_aux (L : known_locs) (m : denv) (k : nat) : iProp Σ :=
([ list] i dio m,
from_option (λ '(DenvItem lv q dv),
dloc_interp L (dLoc (k+i)) C[lv]{q} dval_interp L dv) True dio)%I.
dloc_interp L (dLoc (k+i)) C[lv]{q} dval_interp L dv) True dio)%I.
(** ** Helper lemmas *)
Lemma denv_interp_aux_0 L m :
......@@ -208,7 +224,8 @@ Section denv_spec.
dloc_interp E (dLoc (k+i)) C[x]{q} dval_interp E dv
denv_interp_aux E (denv_singleton i x q dv) k.
Proof.
assert ((lookup i (denv_singleton i x q dv)) = Some (Some (DenvItem x q dv))) as Hdi.
assert ((lookup i (denv_singleton i x q dv)) =
Some (Some (DenvItem x q dv))) as Hdi.
{ induction i; simpl; eauto. }
rewrite /denv_interp_aux.
rewrite (big_sepL_delete' _ _ i); last eassumption.
......@@ -267,7 +284,8 @@ Section denv_spec.
Proof. by rewrite -!denv_interp_aux_0 denv_insert_interp_aux. Qed.
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.
denv_interp_aux E m1 k denv_interp_aux E m2 k
denv_interp_aux E (denv_merge m1 m2) k.
Proof.
iInduction m1 as [|dio1 m1] "IH1" forall (m2 k).
- destruct m2; iIntros "[_ $]".
......@@ -282,7 +300,8 @@ Section denv_spec.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. reflexivity. }
(* TODO: this can be factored away *)
destruct dio1 as [d1|], dio2 as [d2|]; simpl; iFrame.
+ destruct d1, d2. simpl. iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
+ destruct d1, d2. simpl.
iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "$".
iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. done.
......@@ -310,7 +329,8 @@ Section denv_spec.
+ 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/=.
+ destruct (denv_delete_frac i m)
as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=.
iIntros "[$ Hm]".
iSpecialize ("IHm" $! _ (k+1)%nat with "[] [Hm]"); eauto.
{ iApply (big_sepL_mono with "Hm").
......@@ -336,7 +356,8 @@ Section denv_spec.
+ 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/=.
+ 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".
......@@ -351,12 +372,17 @@ Section denv_spec.
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.
Proof. intros ?. by rewrite -!denv_interp_aux_0 denv_delete_frac_interp_aux. Qed.
denv_interp E m
denv_interp E m' dloc_interp E (dLoc i) C{q} dval_interp E dv.
Proof.
intros ?.
by rewrite -!denv_interp_aux_0 denv_delete_frac_interp_aux.
Qed.
Lemma denv_delete_full_interp_aux E i k m m' q dv :
denv_delete_full_aux i m = Some (m', q, dv)
denv_interp_aux E m k denv_interp_aux E m' k dloc_interp E (dLoc (k+i)) C{q} dval_interp E dv.
denv_interp_aux E m k
denv_interp_aux E m' k dloc_interp E (dLoc (k+i)) C{q} dval_interp E dv.
Proof.
iInduction m as [|dio m] "IHm" forall (i k m').
- simpl. iIntros (Hz). inversion Hz.
......@@ -365,7 +391,8 @@ Section denv_spec.
+ 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/=.
+ destruct (denv_delete_full_aux i m)
as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=.
iIntros "[$ Hm]".
iSpecialize ("IHm" $! i (k+1)%nat with "[] [Hm]"); eauto.
* iApply (big_sepL_mono with "Hm").
......@@ -391,7 +418,8 @@ Section denv_spec.
+ 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/=.
+ 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".
......@@ -406,25 +434,31 @@ Section denv_spec.
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.
denv_interp E m
denv_interp E m' dloc_interp E (dLoc i) C{1} dval_interp E dv.
Proof.
rewrite /denv_delete_full.
destruct (denv_delete_full_aux i m) as [[[??]?]|] eqn:Hm; intros ?; simplify_eq/=.
destruct (denv_delete_full_aux i m)
as [[[??]?]|] eqn:Hm; intros ?; simplify_eq/=.
case_option_guard; simplify_eq/=.
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'.
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/=.
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.
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.
iIntros "[Hl Hm]".
iApply denv_delete_full_interp_aux_flip; eauto with iFrame.
Qed.
Lemma denv_unlock_interp E m :
......@@ -499,8 +533,10 @@ Section denv_spec.
length ms = length ms'.
Proof.
revert ms'; induction ms; intros ms'; first by inversion 1. simpl.
destruct (denv_delete_frac i a) as [[[m' q'] dv']|]; first by inversion 1; eauto.
destruct (denv_delete_frac_stack i ms) as [[[m' q'] dv']|] eqn:Hms; last by inversion 1.
destruct (denv_delete_frac i a)
as [[[m' q'] dv']|]; first by inversion 1; eauto.
destruct (denv_delete_frac_stack i ms)
as [[[m' q'] dv']|] eqn:Hms; last by inversion 1.
intros; simplify_eq/=. f_equal. by apply IHms.
Qed.
......@@ -510,7 +546,8 @@ Section denv_spec.
Proof.
revert ms' q dv; induction ms; intros ms' q dv; first by inversion 1. simpl.
destruct (denv_delete_full_aux i a) as [[[m' q'] dv']|];
destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] ?]|] eqn:Hms; intros Hdel; simplify_eq/=.
destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] ?]|] eqn:Hms;
intros Hdel; simplify_eq/=.
- f_equal. by eapply IHms.
- by f_equal.
- f_equal. by eapply IHms.
......@@ -529,7 +566,8 @@ Section denv_spec.
length ms = length ms'.
Proof.
rewrite /denv_delete_full_2. intros.
repeat case_match; simplify_option_eq; eauto using denv_delete_full_stack_aux_length.
repeat case_match;
simplify_option_eq; eauto using denv_delete_full_stack_aux_length.
Qed.
Lemma denv_delete_frac_stack_interp E i ms ms' q dv :
......@@ -538,8 +576,10 @@ Section denv_spec.
Proof.
iInduction ms as [|m ms] "IH" forall (ms'); iIntros (Hdel); simplify_eq/=.
destruct (denv_delete_frac i m) as [[[m' q'] dv']|] eqn:Hm; simplify_eq/=.
- iApply denv_stack_interp_intro. iIntros "Hm". by iApply denv_delete_frac_interp.
- destruct (denv_delete_frac_stack i ms) as [[[m' q'] dv']|] eqn:Hms; simplify_eq/=.
- iApply denv_stack_interp_intro. iIntros "Hm".
by iApply denv_delete_frac_interp.
- destruct (denv_delete_frac_stack i ms)
as [[[m' q'] dv']|] eqn:Hms; simplify_eq/=.
iSpecialize ("IH" with "[]"). eauto.
iApply (denv_stack_interp_mono with "IH").
iIntros "$ $".
......@@ -549,19 +589,25 @@ Section denv_spec.
denv_delete_full_stack_aux i ms = Some (ms', q, dv)
denv_stack_interp ms ms' E (dloc_interp E (dLoc i) C{q} dval_interp E dv)%I.
Proof.
iInduction ms as [|m ms] "IH" forall (ms' q dv); iIntros (Hdel); simplify_eq/=.
destruct (denv_delete_full_aux i m) as [[[m' q'] dv']|] eqn:Hm; simplify_eq/=.
- destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] ?]|] eqn:Hms; simplify_eq/=.
iInduction ms as [|m ms] "IH" forall (ms' q dv);
iIntros (Hdel); simplify_eq/=.
destruct (denv_delete_full_aux i m)
as [[[m' q'] dv']|] eqn:Hm; simplify_eq/=.
- destruct (denv_delete_full_stack_aux i ms)
as [[[ms1 q1] ?]|] eqn:Hms; simplify_eq/=.
+ iSpecialize ("IH" with "[]"). eauto.
iApply (denv_stack_interp_mono with "IH").
iIntros "Hl Hm". rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux /=; last done.
iIntros "Hl Hm".
rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux /=; last done.
iDestruct "Hm" as "[$ Hl2]".
iDestruct (mapsto_value_agree with "Hl Hl2") as %->.
iCombine "Hl Hl2" as "$".
+ iApply denv_stack_interp_intro.
iIntros "Hm". rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done.
iIntros "Hm".
rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done.
iDestruct "Hm" as "[$ $]".
- destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] ?]|] eqn:Hms; simplify_eq/=.
- destruct (denv_delete_full_stack_aux i ms)
as [[[ms1 q1] ?]|] eqn:Hms; simplify_eq/=.
iSpecialize ("IH" with "[]"). eauto.
iApply (denv_stack_interp_mono with "IH").
iIntros "$ $".
......@@ -570,20 +616,23 @@ Section denv_spec.
Lemma denv_delete_full_2_interp E i ms m ms' m' dv :
denv_delete_full_2 i ms m = Some (ms', m', dv)
denv_stack_interp ms ms' E
(denv_interp E m - denv_interp E m' dloc_interp E (dLoc i) C dval_interp E dv)%I.
(denv_interp E m -
denv_interp E m' dloc_interp E (dLoc i) C dval_interp E dv)%I.
Proof.
rewrite /denv_delete_full_2. intros.
destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] dv1]|] eqn:Hms;
destruct (denv_delete_full_aux i m) as [[[m2 q2] dv2]|] eqn:Hm; simplify_eq;
case_option_guard; simplify_eq/=.
- iApply denv_stack_interp_mono; first by iApply denv_delete_full_stack_interp.
- iApply denv_stack_interp_mono;
first by iApply denv_delete_full_stack_interp.
iIntros "Hl1". rewrite -!denv_interp_aux_0.
rewrite denv_delete_full_interp_aux; last done.
iIntros "[$ Hl2]".
iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl". rewrite H1.
iFrame.
- iApply denv_stack_interp_mono; first by iApply denv_delete_full_stack_interp.
- iApply denv_stack_interp_mono;
first by iApply denv_delete_full_stack_interp.
eauto with iFrame.
- iApply denv_stack_interp_intro.
rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done.
......@@ -593,14 +642,17 @@ Section denv_spec.
Lemma denv_delete_frac_2_interp E i ms m ms' m' q dv :
denv_delete_frac_2 i ms m = Some (ms', m', q, dv)
denv_stack_interp ms ms' E
(denv_interp E m - denv_interp E m' dloc_interp E (dLoc i) C{q} dval_interp E dv)%I.
(denv_interp E m -
denv_interp E m' dloc_interp E (dLoc i) C{q} dval_interp E dv)%I.
Proof.
rewrite /denv_delete_frac_2. intros.
destruct (denv_delete_frac_stack i ms) as [[[ms1 q1] dv1]|] eqn:Hms; simplify_eq/=.
destruct (denv_delete_frac_stack i ms)
as [[[ms1 q1] dv1]|] eqn:Hms; simplify_eq/=.
- iApply denv_stack_interp_mono;
first by iApply denv_delete_frac_stack_interp.
eauto with iFrame.
- destruct (denv_delete_frac i m) as [[[m2 q2] dv2]|] eqn:Hnew; simplify_eq/=.
- destruct (denv_delete_frac i m)
as [[[m2 q2] dv2]|] eqn:Hnew; simplify_eq/=.
iApply denv_stack_interp_intro.
rewrite -!denv_interp_aux_0 denv_delete_frac_interp_aux; last done.
eauto with iFrame.
......@@ -636,7 +688,8 @@ Section denv_spec.
Forall (denv_wf E) ms
denv_wf E (denv_stack_merge ms).
Proof.
induction ms as [|m ms]; simpl; eauto. rewrite Forall_cons =>Hm. destruct Hm as [Hm Hms].
induction ms as [|m ms]; simpl; eauto.
rewrite Forall_cons =>Hm. destruct Hm as [Hm Hms].
apply denv_wf_merge; eauto.
Qed.
......@@ -652,15 +705,18 @@ Section denv_spec.
denv_wf E m denv_delete_full_aux i m = Some (m', q, dv)
denv_wf E m' dval_wf E dv.
Proof.
revert i m'; induction m as [|[di|] m]; intros i m'; simpl; first naive_solver.
revert i m'; induction m as [|[di|] m];
intros i m'; simpl; first naive_solver.
- destruct di as [dl df dval]. destruct i.
case_option_guard; simplify_eq/=; try naive_solver.
intros ? ?; destruct_and!.
destruct (denv_delete_full_aux i m) as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=.
destruct (denv_delete_full_aux i m)
as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=.
split_and!; eauto; eapply IHm; eauto.
- destruct i; first naive_solver.
intros ??.
destruct (denv_delete_full_aux i m) as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=.
destruct (denv_delete_full_aux i m)
as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=.
eapply IHm; eauto.
Qed.
......@@ -668,7 +724,8 @@ Section denv_spec.
denv_wf E m denv_lookup i m = Some (q, dv) dval_wf E dv.
Proof.
rewrite /denv_lookup.
destruct (denv_delete_full_aux i m) as [[[? q0] dv0]|] eqn:Hdel; last naive_solver.
destruct (denv_delete_full_aux i m)
as [[[? q0] dv0]|] eqn:Hdel; last naive_solver.
intros; simplify_eq/=.
eapply denv_delete_full_aux_wf; eauto.
Qed.
......@@ -678,10 +735,12 @@ Section denv_spec.
Proof. Admitted.
Lemma denv_wf_delete_full E dv i m m':
denv_wf E m denv_delete_full i m = Some (m', dv) denv_wf E m' dval_wf E dv.
denv_wf E m denv_delete_full i m = Some (m', dv)
denv_wf E m' dval_wf E dv.
Proof.
rewrite /denv_delete_full.
destruct (denv_delete_full_aux i m) as [[[m0 q0] dv0]|] eqn:Hdel; last naive_solver.
destruct (denv_delete_full_aux i m)
as [[[m0 q0] dv0]|] eqn:Hdel; last naive_solver.
simpl; intros; case_option_guard; simplify_eq/=.
eapply denv_delete_full_aux_wf; eauto.
Qed.
......
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