Commit 7546cf67 authored by Dan Frumin's avatar Dan Frumin

Simplify the `bot_l` rule

parent 2e80e6f2
...@@ -10,14 +10,12 @@ Hint Resolve bot_typed : typeable. ...@@ -10,14 +10,12 @@ Hint Resolve bot_typed : typeable.
Section contents. Section contents.
Context `{logrelG Σ}. Context `{logrelG Σ}.
Lemma bot_l ϕ Δ Γ E K t τ : Lemma bot_l Δ Γ E K t τ :
(ϕ - {E;Δ;Γ} fill K (bot #()) log t : τ) -
{E;Δ;Γ} fill K (bot #()) log t : τ. {E;Δ;Γ} fill K (bot #()) log t : τ.
Proof. Proof.
iIntros "Hlog".
iLöb as "IH". iLöb as "IH".
rel_rec_l. rel_rec_l.
unlock bot; simpl_subst/=. unlock bot; simpl_subst/=.
iApply ("IH" with "Hlog"). iApply "IH".
Qed. Qed.
End contents. End contents.
...@@ -223,7 +223,7 @@ Section contents. ...@@ -223,7 +223,7 @@ Section contents.
iApply (bin_log_related_app with "Hlog"). iApply (bin_log_related_app with "Hlog").
iApply bin_log_related_unit. iApply bin_log_related_unit.
+ iMod ("Hcl" with "[-Hlog]"); first close_shoot. + iMod ("Hcl" with "[-Hlog]"); first close_shoot.
rel_apply_l (bot_l False). iIntros ([]). rel_apply_l bot_l.
Qed. Qed.
Lemma bin_log_or_bot_r Δ Γ E (v v' : val) : Lemma bin_log_or_bot_r Δ Γ E (v v' : val) :
......
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