Commit a1285d86 authored by Dan Frumin's avatar Dan Frumin

Get rid of the unnecessary [to_val e = None] premise

It can be deduce from [head_reducible e], since values are non-reducible.
parent 7c97c6ec
......@@ -53,12 +53,14 @@ Section properties.
(Hclosed : Closed e)
(Hclosed' : Closed e')
(Hsafe : σ, head_reducible e σ) :
to_val e = None ->
( σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs)
({E,E;Γ} fill K' e' log t : τ)
{E,E;Γ} fill K' e log t : τ.
Proof.
iIntros (Hval Hstep) "IH".
assert (to_val e = None) as Hval.
{ destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
by eapply val_stuck. }
iIntros (Hstep) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
rewrite /env_subst.
rewrite fill_subst. iModIntro.
......@@ -81,12 +83,14 @@ Section properties.
(Hclosed : Closed e)
(Hclosed' : Closed e')
(Hsafe : σ, head_reducible e σ) :
to_val e = None ->
( σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs)
{E1,E2;Γ} fill K' e' log t : τ
{E1,E2;Γ} fill K' e log t : τ.
Proof.
iIntros (Hval Hstep) "IH".
assert (to_val e = None) as Hval.
{ destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
by eapply val_stuck. }
iIntros (Hstep) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
rewrite /env_subst fill_subst.
rewrite Closed_subst_p_id.
......
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