Commit da8435a2 authored by Dan Frumin's avatar Dan Frumin
Browse files

Move big_sepL_U to U.v

parent 4cb82329
......@@ -73,4 +73,15 @@ Section contents.
Global Instance from_modal_later P : FromModal modality_U (U P) (U P) P.
Proof. by rewrite /FromModal. Qed.
Lemma big_sepL_U {A} (l : list A) Φ :
(([ list] ix l, U (Φ i x)) U ([ list] ix l, Φ i x))%I.
Proof.
iInduction l as [|x l'] "IH" forall (Φ); simpl.
- iIntros "_"; by iModIntro.
- iIntros "[HΦ H]".
iDestruct ("IH" with "H") as "H".
iModIntro. iFrame.
Qed.
End contents.
......@@ -159,17 +159,6 @@ Section denv_spec.
Proof.
Admitted.
(* TODO: DF, move to U.v; prove the other direction *)
Lemma big_sepL_U {A} (l : list A) Φ :
(([ list] ix l, U (Φ i x)) - U ([ list] ix l, Φ i x))%I.
Proof.
iInduction l as [|x l'] "IH" forall (Φ).
- simpl. iIntros "_". by iModIntro.
- simpl. iIntros "[HΦ H]".
iDestruct ("IH" with "H") as "H".
iModIntro. iFrame.
Qed.
Lemma denv_unlock_interp E m :
denv_interp E m - U (denv_interp E (denv_unlock m)).
Proof.
......
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