Library iris.program_logic.ectxi_language

From iris.algebra Require Export base.
From iris.program_logic Require Import language ectx_language.

Class EctxiLanguage (expr val ectx_item state : Type) := {
  of_val : val → expr;
  to_val : expr → option val;
  fill_item : ectx_item → expr → expr;
  head_step : expr → state → expr → state → option expr → Prop;

  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;
  val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef → to_val e1 = None;

  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;

  head_ctx_step_val Ki e σ1 e2 σ2 ef :
    head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e);
}.

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.

  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_val_2:
  (∀ Ki e1 e2, is_Some (to_val e1) → is_Some (to_val e2) →
         is_Some (to_val (fill_item Ki e1)) →
         is_Some (to_val (fill_item Ki e2))) →
  ∀ K e1 e2, is_Some (to_val e1) → is_Some (to_val e2) →
         is_Some (to_val (fill K e1)) →
         is_Some (to_val (fill K e2)).
  Proof.
    intros HKi K. revert HKi.
    induction K; intros HKi e1 e2; eauto.
    rewrite //=. intros Hv1 Hv2 Hfill.
    eapply HKi.
    - eapply fill_item_val. eauto.
    - eapply IHK.
      × apply HKi.
      × apply Hv1.
      × apply Hv2.
      × eapply fill_item_val. eauto.
    - 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.

  Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
    fill K e1 = fill K' e1' → to_val e1 = None → head_step e1' σ1 e2 σ2 ef →
    ∃ K'', K' = K ++ 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 :=
    
    Build_EctxLanguage expr val ectx state of_val to_val [] (++) fill head_step _ _ _ _ _ _ _ _ _.
  Solve Obligations with eauto using to_of_val, of_to_val, val_stuck,
    fill_not_val, step_by_val, fold_right_app, app_eq_nil.

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

  Lemma head_step_det_prim_det:
        (∀ e σ e1' σ1' ef1' e2' σ2' ef2',
            head_step e σ e1' σ1' ef1' →
            head_step e σ e2' σ2' ef2' →
            e1' = e2' ∧ σ1' = σ2' ∧ ef1' = ef2') →
        (∀ e σ e1' σ1' ef1' e2' σ2' ef2',
            prim_step e σ e1' σ1' ef1' →
            prim_step e σ e2' σ2' ef2' →
            e1' = e2' ∧ σ1' = σ2' ∧ ef1' = ef2').
   Proof.
     intros Hdet e σ e1' σ1' ef1' e2' σ2' ef2' Hprim1 Hprim2.
     inversion Hprim1 as [K1 efill1 e1'' ??]; subst.
     inversion Hprim2 as [K2 efill2 e2'' ??]; subst.
     assert (efill1 = efill2 ∧ K1 = K2) as (->&->).
     { edestruct (step_by_val K1 K2) as (K1'&Hpre1); eauto using val_stuck.
       edestruct (step_by_val K2 K1) as (K2'&Hpre2); eauto using val_stuck.
       rewrite Hpre1 in Hpre2.
       rewrite -app_assoc -{1}(app_nil_r K1) in Hpre2.
       apply app_inv_head in Hpre2.
       symmetry in Hpre2. apply app_eq_nil in Hpre2 as (->&->).
       rewrite ?app_nil_r in Hpre1. subst.
       split; auto.
       eapply fill_inj; eauto.
     }
     edestruct (Hdet efill2 σ e1'' σ1' ef1' e2'') as (->&->&->); eauto.
   Qed.

End ectxi_language.