ectxi_language.v 4.28 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
(** An axiomatization of languages based on evaluation context items, including
    a proof that these are instances of general ectx-based languages. *)
From iris.algebra Require Export base.
From iris.program_logic Require Import language ectx_language.

(* We need to make thos arguments indices that we want canonical structure
   inference to use a keys. *)
Class EctxiLanguage (expr val ectx_item state : Type) := {
  of_val : val  expr;
  to_val : expr  option val;
  fill_item : ectx_item  expr  expr;
12
  head_step : expr  state  expr  state  list expr  Prop;
13 14 15

  to_of_val v : to_val (of_val v) = Some v;
  of_to_val e v : to_val e = Some v  of_val v = e;
16
  val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs  to_val e1 = None;
17 18 19 20 21 22 23

  fill_item_inj Ki :> Inj (=) (=) (fill_item Ki);
  fill_item_val Ki e : is_Some (to_val (fill_item Ki e))  is_Some (to_val e);
  fill_item_no_val_inj Ki1 Ki2 e1 e2 :
    to_val e1 = None  to_val e2 = None 
    fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2;

24 25
  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);
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
}.

Arguments of_val {_ _ _ _ _} _.
Arguments to_val {_ _ _ _ _} _.
Arguments fill_item {_ _ _ _ _} _ _.
Arguments head_step {_ _ _ _ _} _ _ _ _ _.

Arguments to_of_val {_ _ _ _ _} _.
Arguments of_to_val {_ _ _ _ _} _ _ _.
Arguments val_stuck {_ _ _ _ _} _ _ _ _ _ _.
Arguments fill_item_val {_ _ _ _ _} _ _ _.
Arguments fill_item_no_val_inj {_ _ _ _ _} _ _ _ _ _ _ _.
Arguments head_ctx_step_val {_ _ _ _ _} _ _ _ _ _ _ _.
Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.

Section ectxi_language.
  Context {expr val ectx_item state}
          {Λ : EctxiLanguage expr val ectx_item state}.
  Implicit Types (e : expr) (Ki : ectx_item).
  Notation ectx := (list ectx_item).

  Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.

49 50 51
  Lemma fill_app (K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
  Proof. apply fold_right_app. Qed.

52 53 54 55 56 57 58 59 60 61 62 63 64 65
  Instance fill_inj K : Inj (=) (=) (fill K).
  Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.

  Lemma fill_val K e : is_Some (to_val (fill K e))  is_Some (to_val e).
  Proof.
    induction K; simpl; first done. intros ?%fill_item_val. eauto.
  Qed.

  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.

  (* When something does a step, and another decomposition of the same expression
  has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
  other words, [e] also contains the reducible expression *)
66 67
  Lemma step_by_val K K' e1 e1' σ1 e2 σ2 efs :
    fill K e1 = fill K' e1'  to_val e1 = None  head_step e1' σ1 e2 σ2 efs 
68 69 70 71 72 73 74 75 76 77 78 79 80 81
    exists K'', K' = K ++ K''. (* K `prefix_of` K' *)
  Proof.
    intros Hfill Hred Hnval; revert K' Hfill.
    induction K as [|Ki K IH]; simpl; intros K' Hfill; first by eauto.
    destruct K' as [|Ki' K']; simplify_eq/=.
    { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
      eauto using fill_not_val, head_ctx_step_val. }
    cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
    eauto using fill_item_no_val_inj, val_stuck, fill_not_val.
  Qed.

  Global Program Instance : EctxLanguage expr val ectx state :=
    (* For some reason, Coq always rejects the record syntax claiming I
       fixed fields of different records, even when I did not. *)
82
    Build_EctxLanguage expr val ectx state of_val to_val [] (++) fill head_step _ _ _ _ _ _ _ _ _.
83
  Solve Obligations with eauto using to_of_val, of_to_val, val_stuck,
84
    fill_not_val, fill_app, step_by_val, fold_right_app, app_eq_nil.
85 86 87 88

  Global Instance ectxi_lang_ctx_item Ki :
    LanguageCtx (ectx_lang expr) (fill_item Ki).
  Proof. change (LanguageCtx _ (fill [Ki])). apply _. Qed.
89 90

  Lemma step_is_head K e σ :
91 92
    to_val e = None 
    ( Ki K e', e = fill (Ki :: K) e'  ¬head_reducible e' σ) 
93 94 95 96
    reducible (fill K e) σ  head_reducible e σ.
  Proof.
    intros Hnonval Hnondecomp (e'&σ''&ef&Hstep).
    change fill with ectx_language.fill in Hstep.
97 98 99
    apply fill_step_inv in Hstep as (e2'&_&Hstep); last done.
    clear K. destruct Hstep as [[|Ki K] e1' e2'' -> -> Hstep]; [red; eauto|].
    destruct (Hnondecomp Ki K e1'); unfold head_reducible; eauto.
100
  Qed.
101
End ectxi_language.