Commit 4dc1ebda authored by Ralf Jung's avatar Ralf Jung

Merge branch 'robbert/not_stuck_fill' into 'master'

Rename lemma `not_stuck_under_ectx` → `not_stuck_fill`, to be consistent with `stuck_fill`.

See merge request !339
parents 4f300830 8e455e52
Pipeline #21581 passed with stage
in 15 minutes and 47 seconds
......@@ -470,7 +470,7 @@ Proof.
lazymatch K with
| [] => fail
| _ => apply (prim_step_matched_by_erased_steps_ectx K);
apply IH; [done| by eapply (not_stuck_under_ectx (fill K))]
apply IH; [done| by eapply (not_stuck_fill (fill K))]
end
in
reshape_expr e tac
......@@ -587,11 +587,11 @@ Proof.
end.
apply (prim_step_matched_by_erased_steps_ectx [ResolveMCtx _ _]).
apply IH; [rewrite !app_length /=; lia|done|
by eapply (not_stuck_under_ectx (fill [ResolveMCtx _ _])); simpl].
by eapply (not_stuck_fill (fill [ResolveMCtx _ _])); simpl].
- (** e1 is of the form ([Resolve] e1_ e1_2 e13) and e1_3 takes a prim_step. *)
apply (prim_step_matched_by_erased_steps_ectx [ResolveRCtx _ _]).
apply IH; [rewrite !app_length /=; lia|done|
by eapply (not_stuck_under_ectx (fill [ResolveRCtx _ _])); simpl].
by eapply (not_stuck_fill (fill [ResolveRCtx _ _])); simpl].
Qed.
Lemma erased_prim_step_prim_step e1 σ1 κ e2 σ2 efs:
......
......@@ -168,9 +168,17 @@ Section language.
to_val e = None irreducible e σ irreducible (K e) σ.
Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
Lemma not_stuck_fill K `{!@LanguageCtx Λ K} e σ :
not_stuck (K e) σ not_stuck e σ.
Proof.
rewrite /not_stuck -!not_eq_None_Some. intros [?|?].
- auto using fill_not_val.
- destruct (decide (to_val e = None)); auto using reducible_fill.
Qed.
Lemma stuck_fill `{!@LanguageCtx Λ K} e σ :
stuck e σ stuck (K e) σ.
Proof. intros [??]. split. by apply fill_not_val. by apply irreducible_fill. Qed.
Proof. rewrite -!not_not_stuck. eauto using not_stuck_fill. Qed.
Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) κ σ1 σ2 :
t1 t1' step (t1,σ1) κ (t2,σ2) t2', t2 t2' step (t1',σ1) κ (t2',σ2).
......@@ -235,16 +243,6 @@ Section language.
rtc pure_step e1 e2 rtc pure_step (K e1) (K e2).
Proof. eauto using rtc_congruence, pure_step_ctx. Qed.
Lemma not_stuck_under_ectx K `{!@LanguageCtx Λ K} e σ :
not_stuck (K e) σ not_stuck e σ.
Proof.
rewrite /not_stuck /reducible /=.
intros [[? HK]|(?&?&?&?&Hstp)]; simpl in *.
- left. apply not_eq_None_Some; intros ?%fill_not_val; simplify_eq.
- destruct (to_val e) eqn:?; first by left; eauto.
apply fill_step_inv in Hstp; naive_solver.
Qed.
(* We do not make this an instance because it is awfully general. *)
Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 :
PureExec φ n e1 e2
......
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