Commit 976b02f6 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/lang-axioms' into 'master'

Explain our language axioms better

Closes #271

See merge request !440
parents 635cdf1e 7a4f28b1
Pipeline #28095 passed with stage
in 16 minutes and 4 seconds
...@@ -4,7 +4,7 @@ From iris.algebra Require Export base. ...@@ -4,7 +4,7 @@ From iris.algebra Require Export base.
From iris.program_logic Require Import language. From iris.program_logic Require Import language.
Set Default Proof Using "Type". Set Default Proof Using "Type".
(* TAKE CARE: When you define an [ectxLanguage] canonical structure for your (** TAKE CARE: When you define an [ectxLanguage] canonical structure for your
language, you need to also define a corresponding [language] canonical language, you need to also define a corresponding [language] canonical
structure. Use the coercion [LanguageOfEctx] as defined in the bottom of this structure. Use the coercion [LanguageOfEctx] as defined in the bottom of this
file for doing that. *) file for doing that. *)
...@@ -29,15 +29,23 @@ Section ectx_language_mixin. ...@@ -29,15 +29,23 @@ Section ectx_language_mixin.
mixin_fill_inj K : Inj (=) (=) (fill K); mixin_fill_inj K : Inj (=) (=) (fill K);
mixin_fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e); mixin_fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e);
mixin_step_by_val K K' e1 e1' σ1 κ e2 σ2 efs : (** Given a head redex [e1_redex] somewhere in a term, and another
fill K e1 = fill K' e1' decomposition of the same term into [fill K' e1'] such that [e1'] is not
to_val e1 = None a value, then the head redex context is [e1']'s context [K'] filled with
head_step e1' σ1 κ e2 σ2 efs another context [K'']. In particular, this implies [e1 = fill K''
K'', K' = comp_ectx K K''; e1_redex] by [fill_inj], i.e., [e1]' contains the head redex.)
(* If [fill K e] takes a head step, then either [e] is a value or [K] is This implies there can be only one head redex, see
the empty evaluation context. In other words, if [e] is not a value then [head_redex_unique]. *)
there cannot be another redex position elsewhere in [fill K e]. *) mixin_step_by_val K' K_redex e1' e1_redex σ1 κ e2 σ2 efs :
fill K' e1' = fill K_redex e1_redex
to_val e1' = None
head_step e1_redex σ1 κ e2 σ2 efs
K'', K_redex = comp_ectx K' K'';
(** If [fill K e] takes a head step, then either [e] is a value or [K] is
the empty evaluation context. In other words, if [e] is not a value
wrapping it in a context does not add new head redex positions. *)
mixin_head_ctx_step_val K e σ1 κ e2 σ2 efs : mixin_head_ctx_step_val K e σ1 κ e2 σ2 efs :
head_step (fill K e) σ1 κ e2 σ2 efs is_Some (to_val e) K = empty_ectx; head_step (fill K e) σ1 κ e2 σ2 efs is_Some (to_val e) K = empty_ectx;
}. }.
...@@ -90,11 +98,11 @@ Section ectx_language. ...@@ -90,11 +98,11 @@ Section ectx_language.
Proof. apply ectx_language_mixin. Qed. Proof. apply ectx_language_mixin. Qed.
Lemma fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e). Lemma fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e).
Proof. apply ectx_language_mixin. Qed. Proof. apply ectx_language_mixin. Qed.
Lemma step_by_val K K' e1 e1' σ1 κ e2 σ2 efs : Lemma step_by_val K' K_redex e1' e1_redex σ1 κ e2 σ2 efs :
fill K e1 = fill K' e1' fill K' e1' = fill K_redex e1_redex
to_val e1 = None to_val e1' = None
head_step e1' σ1 κ e2 σ2 efs head_step e1_redex σ1 κ e2 σ2 efs
K'', K' = comp_ectx K K''. K'', K_redex = comp_ectx K' K''.
Proof. apply ectx_language_mixin. Qed. Proof. apply ectx_language_mixin. Qed.
Lemma head_ctx_step_val K e σ1 κ e2 σ2 efs : Lemma head_ctx_step_val K e σ1 κ e2 σ2 efs :
head_step (fill K e) σ1 κ e2 σ2 efs is_Some (to_val e) K = empty_ectx. head_step (fill K e) σ1 κ e2 σ2 efs is_Some (to_val e) K = empty_ectx.
...@@ -140,20 +148,40 @@ Section ectx_language. ...@@ -140,20 +148,40 @@ Section ectx_language.
head_step e σ κ e' σ' efs head_step e σ κ e' σ' efs
if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e'). if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
(* Some lemmas about this language *) (** * Some lemmas about this language *)
Lemma fill_not_val K e : to_val e = None to_val (fill K e) = None. Lemma fill_not_val K e : to_val e = None to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed. Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
Lemma head_prim_step e1 σ1 κ e2 σ2 efs :
head_step e1 σ1 κ e2 σ2 efs prim_step e1 σ1 κ e2 σ2 efs.
Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
Lemma head_reducible_no_obs_reducible e σ : Lemma head_reducible_no_obs_reducible e σ :
head_reducible_no_obs e σ head_reducible e σ. head_reducible_no_obs e σ head_reducible e σ.
Proof. intros (?&?&?&?). eexists. eauto. Qed. Proof. intros (?&?&?&?). eexists. eauto. Qed.
Lemma not_head_reducible e σ : ¬head_reducible e σ head_irreducible e σ. Lemma not_head_reducible e σ : ¬head_reducible e σ head_irreducible e σ.
Proof. unfold head_reducible, head_irreducible. naive_solver. Qed. Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.
(** The decomposition into head redex and context is unique.
In all sensible instances, [comp_ectx K' empty_ectx] will be the same as
[K'], so the conclusion is [K = K' ∧ e = e'], but we do not require a law
to actually prove that so we cannot use that fact here. *)
Lemma head_redex_unique K K' e e' σ :
fill K e = fill K' e'
head_reducible e σ
head_reducible e' σ
K = comp_ectx K' empty_ectx e = e'.
Proof.
intros Heq (κ & e2 & σ2 & efs & Hred) (κ' & e2' & σ2' & efs' & Hred').
edestruct (step_by_val K' K e' e) as [K'' HK];
[by eauto using val_head_stuck..|].
subst K. move: Heq. rewrite -fill_comp. intros <-%(inj (fill _)).
destruct (head_ctx_step_val _ _ _ _ _ _ _ Hred') as [[]%not_eq_None_Some|HK''].
{ by eapply val_head_stuck. }
subst K''. rewrite fill_empty. done.
Qed.
Lemma head_prim_step e1 σ1 κ e2 σ2 efs :
head_step e1 σ1 κ e2 σ2 efs prim_step e1 σ1 κ e2 σ2 efs.
Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
Lemma head_step_not_stuck e σ κ e' σ' efs : head_step e σ κ e' σ' efs not_stuck e σ. Lemma head_step_not_stuck e σ κ e' σ' efs : head_step e σ κ e' σ' efs not_stuck e σ.
Proof. rewrite /not_stuck /reducible /=. eauto 10 using head_prim_step. Qed. Proof. rewrite /not_stuck /reducible /=. eauto 10 using head_prim_step. Qed.
......
...@@ -4,7 +4,7 @@ From iris.algebra Require Export base. ...@@ -4,7 +4,7 @@ From iris.algebra Require Export base.
From iris.program_logic Require Import language ectx_language. From iris.program_logic Require Import language ectx_language.
Set Default Proof Using "Type". Set Default Proof Using "Type".
(* TAKE CARE: When you define an [ectxiLanguage] canonical structure for your (** TAKE CARE: When you define an [ectxiLanguage] canonical structure for your
language, you need to also define a corresponding [language] and [ectxLanguage] language, you need to also define a corresponding [language] and [ectxLanguage]
canonical structure for canonical structure inference to work properly. You canonical structure for canonical structure inference to work properly. You
should use the coercion [EctxLanguageOfEctxi] and [LanguageOfEctx] for that, and should use the coercion [EctxLanguageOfEctxi] and [LanguageOfEctx] for that, and
...@@ -38,12 +38,20 @@ Section ectxi_language_mixin. ...@@ -38,12 +38,20 @@ Section ectxi_language_mixin.
mixin_of_to_val e v : to_val e = Some v of_val v = e; mixin_of_to_val e v : to_val e = Some v of_val v = e;
mixin_val_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs to_val e1 = None; mixin_val_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs to_val e1 = None;
mixin_fill_item_inj Ki : Inj (=) (=) (fill_item Ki);
mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) is_Some (to_val e); mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) is_Some (to_val e);
(** [fill_item] is always injective on the expression for a fixed
context. *)
mixin_fill_item_inj Ki : Inj (=) (=) (fill_item Ki);
(** [fill_item] with (potentially different) non-value expressions is
injective on the context. *)
mixin_fill_item_no_val_inj Ki1 Ki2 e1 e2 : mixin_fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None to_val e2 = None to_val e1 = None to_val e2 = None
fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2; fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2;
(** If [fill_item Ki e] takes a head step, then [e] is a value (unlike for
[ectx_language], an empty context is impossible here). In other words,
if [e] is not a value then wrapping it in a context does not add new
head redex positions. *)
mixin_head_ctx_step_val Ki e σ1 κ e2 σ2 efs : mixin_head_ctx_step_val Ki e σ1 κ e2 σ2 efs :
head_step (fill_item Ki e) σ1 κ e2 σ2 efs is_Some (to_val e); head_step (fill_item Ki e) σ1 κ e2 σ2 efs is_Some (to_val 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