Commit 94922d09 authored by Ralf Jung's avatar Ralf Jung

make strongly_atomic_atomic more convenient

parent e76ca2de
Pipeline #5779 passed with stages
in 9 minutes and 23 seconds
......@@ -195,9 +195,7 @@ Definition is_atomic (e : expr) :=
end.
Lemma is_atomic_correct s e : is_atomic e Atomic s (to_expr e).
Proof.
enough (is_atomic e Atomic StronglyAtomic (to_expr e)).
{ destruct s; auto using strongly_atomic_atomic. }
intros He. apply ectx_language_atomic.
intros He. apply strongly_atomic_atomic, ectx_language_atomic.
- intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
......
......@@ -109,9 +109,9 @@ Section language.
Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Lemma strongly_atomic_atomic e :
Atomic StronglyAtomic e Atomic WeaklyAtomic e.
Proof. unfold Atomic. eauto using val_irreducible. Qed.
Lemma strongly_atomic_atomic e a :
Atomic StronglyAtomic e Atomic a e.
Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
Lemma reducible_fill `{LanguageCtx Λ K} e σ :
to_val e = None reducible (K e) σ reducible 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