Commit cd8f3be9 authored by Robbert's avatar Robbert

Merge branch 'head_prim_fill_reducible' into 'master'

Add `head_prim_fill_reducible`.

See merge request iris/iris!293
parents 9b77b750 4767c8f9
Pipeline #18407 passed with stage
in 14 minutes and 30 seconds
......@@ -151,8 +151,23 @@ Section ectx_language.
Lemma not_head_reducible e σ : ¬head_reducible e σ head_irreducible e σ.
Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.
Lemma fill_prim_step K e1 σ1 κ e2 σ2 efs :
prim_step e1 σ1 κ e2 σ2 efs prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs.
Proof.
destruct 1 as [K' e1' e2' -> ->].
rewrite !fill_comp. by econstructor.
Qed.
Lemma fill_reducible K e σ : reducible e σ reducible (fill K e) σ.
Proof.
intros (κ&e'&σ'&efs&?). exists κ, (fill K e'), σ', efs.
by apply fill_prim_step.
Qed.
Lemma head_prim_reducible e σ : head_reducible e σ reducible e σ.
Proof. intros (κ&e'&σ'&efs&?). eexists κ, e', σ', efs. by apply head_prim_step. Qed.
Lemma head_prim_fill_reducible e K σ :
head_reducible e σ reducible (fill K e) σ.
Proof. intro. by apply fill_reducible, head_prim_reducible. Qed.
Lemma head_prim_reducible_no_obs e σ : head_reducible_no_obs e σ reducible_no_obs e σ.
Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
Lemma head_prim_irreducible e σ : irreducible e σ head_irreducible e σ.
......
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