Commit 95433e05 authored by Ralf Jung's avatar Ralf Jung

revert language argument of LanguageCtx back to implicit

parent da93f357
...@@ -201,7 +201,7 @@ Section ectx_language. ...@@ -201,7 +201,7 @@ Section ectx_language.
Qed. Qed.
(* Every evaluation context is a context. *) (* Every evaluation context is a context. *)
Global Instance ectx_lang_ctx K : LanguageCtx _ (fill K). Global Instance ectx_lang_ctx K : LanguageCtx (fill K).
Proof. Proof.
split; simpl. split; simpl.
- eauto using fill_not_val. - eauto using fill_not_val.
......
...@@ -137,8 +137,8 @@ Section ectxi_language. ...@@ -137,8 +137,8 @@ Section ectxi_language.
intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app. intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
Qed. Qed.
Global Instance ectxi_lang_ctx_item Ki : LanguageCtx _ (fill_item Ki). Global Instance ectxi_lang_ctx_item Ki : LanguageCtx (fill_item Ki).
Proof. change (LanguageCtx _ (fill [Ki])). apply _. Qed. Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.
End ectxi_language. End ectxi_language.
Arguments fill {_} _ _%E. Arguments fill {_} _ _%E.
......
...@@ -89,7 +89,7 @@ Proof. ...@@ -89,7 +89,7 @@ Proof.
iIntros (v) "Hv". by iApply "HΦ". iIntros (v) "Hv". by iApply "HΦ".
Qed. Qed.
Lemma ht_bind `{!LanguageCtx Λ K} s E P Φ Φ' e : Lemma ht_bind `{!LanguageCtx K} s E P Φ Φ' e :
{{ P }} e @ s; E {{ Φ }} ( v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }}) {{ P }} e @ s; E {{ Φ }} ( v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
{{ P }} K e @ s; E {{ Φ' }}. {{ P }} K e @ s; E {{ Φ' }}.
Proof. Proof.
......
...@@ -53,9 +53,8 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := { ...@@ -53,9 +53,8 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
to_val e1' = None prim_step (K e1') σ1 κ e2 σ2 efs to_val e1' = None prim_step (K e1') σ1 κ e2 σ2 efs
e2', e2 = K e2' prim_step e1' σ1 κ e2' σ2 efs e2', e2 = K e2' prim_step e1' σ1 κ e2' σ2 efs
}. }.
Arguments LanguageCtx : clear implicits.
Instance language_ctx_id Λ : LanguageCtx Λ (@id (expr Λ)). Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
Proof. constructor; naive_solver. Qed. Proof. constructor; naive_solver. Qed.
Inductive atomicity := StronglyAtomic | WeaklyAtomic. Inductive atomicity := StronglyAtomic | WeaklyAtomic.
...@@ -142,19 +141,19 @@ Section language. ...@@ -142,19 +141,19 @@ Section language.
Atomic StronglyAtomic e Atomic a e. Atomic StronglyAtomic e Atomic a e.
Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed. Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
Lemma reducible_fill `{!LanguageCtx Λ K} e σ : Lemma reducible_fill `{!@LanguageCtx Λ K} e σ :
to_val e = None reducible (K e) σ reducible e σ. to_val e = None reducible (K e) σ reducible e σ.
Proof. Proof.
intros ? (e'&σ'&k&efs&Hstep); unfold reducible. intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto. apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
Qed. Qed.
Lemma reducible_no_obs_fill `{!LanguageCtx Λ K} e σ : Lemma reducible_no_obs_fill `{!@LanguageCtx Λ K} e σ :
to_val e = None reducible_no_obs (K e) σ reducible_no_obs e σ. to_val e = None reducible_no_obs (K e) σ reducible_no_obs e σ.
Proof. Proof.
intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs. intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs.
apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto. apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
Qed. Qed.
Lemma irreducible_fill `{!LanguageCtx Λ K} e σ : Lemma irreducible_fill `{!@LanguageCtx Λ K} e σ :
to_val e = None irreducible e σ irreducible (K e) σ. to_val e = None irreducible e σ irreducible (K e) σ.
Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed. Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
...@@ -186,7 +185,7 @@ Section language. ...@@ -186,7 +185,7 @@ Section language.
Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) := Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
pure_exec : φ relations.nsteps pure_step n e1 e2. pure_exec : φ relations.nsteps pure_step n e1 e2.
Lemma pure_step_ctx K `{!LanguageCtx Λ K} e1 e2 : Lemma pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
pure_step e1 e2 pure_step e1 e2
pure_step (K e1) (K e2). pure_step (K e1) (K e2).
Proof. Proof.
...@@ -198,13 +197,13 @@ Section language. ...@@ -198,13 +197,13 @@ Section language.
+ edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto. + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
Qed. Qed.
Lemma pure_step_nsteps_ctx K `{!LanguageCtx Λ K} n e1 e2 : Lemma pure_step_nsteps_ctx K `{!@LanguageCtx Λ K} n e1 e2 :
relations.nsteps pure_step n e1 e2 relations.nsteps pure_step n e1 e2
relations.nsteps pure_step n (K e1) (K e2). relations.nsteps pure_step n (K e1) (K e2).
Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed. Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed.
(* We do not make this an instance because it is awfully general. *) (* We do not make this an instance because it is awfully general. *)
Lemma pure_exec_ctx K `{!LanguageCtx Λ K} φ n e1 e2 : Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 :
PureExec φ n e1 e2 PureExec φ n e1 e2
PureExec φ n (K e1) (K e2). PureExec φ n (K e1) (K e2).
Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed. Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.
......
...@@ -147,7 +147,7 @@ Proof. ...@@ -147,7 +147,7 @@ Proof.
iModIntro. iSplit; first done. iFrame "Hσ Hefs". by iApply twp_value'. iModIntro. iSplit; first done. iFrame "Hσ Hefs". by iApply twp_value'.
Qed. Qed.
Lemma twp_bind K `{!LanguageCtx Λ K} s E e Φ : Lemma twp_bind K `{!LanguageCtx K} s E e Φ :
WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }] - WP K e @ s; E [{ Φ }]. WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }] - WP K e @ s; E [{ Φ }].
Proof. Proof.
revert Φ. cut ( Φ', WP e @ s; E [{ Φ' }] - Φ, revert Φ. cut ( Φ', WP e @ s; E [{ Φ' }] - Φ,
...@@ -169,7 +169,7 @@ Proof. ...@@ -169,7 +169,7 @@ Proof.
- by setoid_rewrite and_elim_r. - by setoid_rewrite and_elim_r.
Qed. Qed.
Lemma twp_bind_inv K `{!LanguageCtx Λ K} s E e Φ : Lemma twp_bind_inv K `{!LanguageCtx K} s E e Φ :
WP K e @ s; E [{ Φ }] - WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }]. WP K e @ s; E [{ Φ }] - WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }].
Proof. Proof.
iIntros "H". remember (K e) as e' eqn:He'. iIntros "H". remember (K e) as e' eqn:He'.
......
...@@ -143,7 +143,7 @@ Proof. ...@@ -143,7 +143,7 @@ Proof.
iIntros (v) "H". by iApply "H". iIntros (v) "H". by iApply "H".
Qed. Qed.
Lemma wp_bind K `{!LanguageCtx Λ K} s E e Φ : Lemma wp_bind K `{!LanguageCtx K} s E e Φ :
WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }} WP K e @ s; E {{ Φ }}. WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }} WP K e @ s; E {{ Φ }}.
Proof. Proof.
iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre. iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
...@@ -160,7 +160,7 @@ Proof. ...@@ -160,7 +160,7 @@ Proof.
iModIntro. iFrame "Hσ Hefs". by iApply "IH". iModIntro. iFrame "Hσ Hefs". by iApply "IH".
Qed. Qed.
Lemma wp_bind_inv K `{!LanguageCtx Λ K} s E e Φ : Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
WP K e @ s; E {{ Φ }} WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}. WP K e @ s; E {{ Φ }} WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}.
Proof. Proof.
iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre. iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
......
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