From mininix Require Export utils nix.operational.
From stdpp Require Import options.

(** Properties of operational semantics *)
Lemma float_to_bounded_Z_ok f : int_ok (float_to_bounded_Z f).
Proof.
  rewrite /float_to_bounded_Z.
  destruct (Float.to_Z f); simplify_option_eq; done.
Qed.

Lemma int_ok_alt i :
  int_ok i ↔ ∀ n, (63 ≤ n)%Z → Z.testbit i n = bool_decide (i < 0)%Z.
Proof.
  rewrite -Z.bounded_iff_bits //.
  rewrite /int_ok bool_decide_spec /int_min /int_max Z.shiftl_1_l. lia.
Qed.

Lemma int_ok_land i1 i2 : int_ok i1 → int_ok i2 → int_ok (Z.land i1 i2).
Proof.
  rewrite !int_ok_alt=> Hi1 Hi2 n ?. rewrite Z.land_spec Hi1 // Hi2 //.
  apply eq_bool_prop_intro. rewrite andb_True !bool_decide_spec Z.land_neg //.
Qed.

Lemma int_ok_lor i1 i2 : int_ok i1 → int_ok i2 → int_ok (Z.lor i1 i2).
Proof.
  rewrite !int_ok_alt=> Hi1 Hi2 n ?. rewrite Z.lor_spec Hi1 // Hi2 //.
  apply eq_bool_prop_intro. rewrite orb_True !bool_decide_spec Z.lor_neg //.
Qed.

Lemma int_ok_lxor i1 i2 : int_ok i1 → int_ok i2 → int_ok (Z.lxor i1 i2).
Proof.
  rewrite !int_ok_alt=> Hi1 Hi2 n ?. rewrite Z.lxor_spec Hi1 // Hi2 //.
  apply eq_bool_prop_intro. rewrite xorb_True !bool_decide_spec.
  rewrite !Z.lt_nge Z.lxor_nonneg. lia.
Qed.

Lemma sem_bin_op_num_ok {op f n1 n2 bl} :
  num_ok n1 → num_ok n2 →
  sem_bin_op_num op n1 = Some f → f n2 = Some bl → base_lit_ok bl.
Proof.
  intros; destruct op, n1, n2; simplify_option_eq;
    try (by apply (bool_decide_pack _));
    auto using int_ok_land, int_ok_lor, int_ok_lxor.
Qed.

Lemma sem_bin_op_string_ok {op f s1 s2} :
  sem_bin_op_string op = Some f → base_lit_ok (f s1 s2).
Proof. intros; destruct op; naive_solver. Qed.

Global Hint Extern 0 (no_recs (_ <$> _)) => by apply map_Forall_fmap : core.

Ltac inv_step := repeat
  match goal with
  | H : ¬no_recs (_ <$> _) |- _ => destruct H; by apply map_Forall_fmap
  | H : ?e -{_}-> _ |- _ => assert_succeeds (is_app_constructor e); inv H
  | H : ctx1 _ _ ?K |- _ => is_var K; inv H
  end.

Global Instance Attr_inj τ : Inj (=) (=) (Attr τ).
Proof. by injection 1. Qed.

Lemma fmap_attr_expr_Attr τ (es : gmap string expr) :
  attr_expr <$> (Attr τ <$> es) = es.
Proof. apply map_eq=> x. rewrite !lookup_fmap. by destruct (_ !! _). Qed.

Lemma no_recs_insert αs x e : no_recs αs → no_recs (<[x:=AttrN e]> αs).
Proof. by apply map_Forall_insert_2. Qed.
Lemma no_recs_insert_inv αs x τ e :
  αs !! x = None → no_recs (<[x:=Attr τ e]> αs) → no_recs αs.
Proof. intros ??%map_Forall_insert; naive_solver. Qed.
Lemma no_recs_lookup αs x τ e : no_recs αs → αs !! x = Some (Attr τ e) → τ = NONREC.
Proof. intros Hall. apply Hall. Qed.

Lemma no_recs_attr_subst αs ds : no_recs αs → no_recs (attr_subst ds <$> αs).
Proof.
  intros. eapply map_Forall_fmap, map_Forall_impl; [done|]. by intros ? [[]] [=].
Qed.

Lemma from_attr_no_recs {A} (f g : expr → A) (αs : gmap string attr) :
  no_recs αs → from_attr f g <$> αs = g ∘ attr_expr <$> αs.
Proof.
  intros Hrecs. apply map_eq=> x. rewrite !lookup_fmap. specialize (Hrecs x).
  destruct (αs !! x) as [[]|] eqn:?; naive_solver.
Qed.

Lemma sem_and_attr_empty : sem_and_attr ∅ = ELit (LitBool true).
Proof. done. Qed.
Lemma sem_and_attr_insert es x e :
  es !! x = None → (∀ y, is_Some (es !! y) → attr_le x y) →
  sem_and_attr (<[x:=e]> es) = EIf e (sem_and_attr es) (ELit (LitBool false)).
Proof. intros. by rewrite /sem_and_attr map_fold_sorted_insert. Qed.

Lemma matches_strict es ms ds x e :
  es !! x = None →
  ms !! x = None →
  matches es ms false ds →
  matches (<[x:=e]> es) ms false ds.
Proof.
  remember false as strict.
  induction 3; simplify_eq/=;
    repeat match goal with
    | H : <[ _ := _ ]> _ !! _ = None |- _ => apply lookup_insert_None in H as [??]
    | _ => rewrite (insert_commute _ x) //
    | _ => constructor
    | _ => apply lookup_insert_None
    end; eauto.
Qed.

Lemma subst_empty e : subst ∅ e = e.
Proof.
  induction e; repeat destruct select (option _); do 2 f_equal/=; auto.
  - apply map_eq=> x. rewrite lookup_fmap.
    destruct (_ !! x) as [[e'|]|] eqn:Hx; do 2 f_equal/=. apply (H _ _ Hx).
  - induction H; f_equal/=; auto.
  - apply map_eq; intros i. rewrite lookup_fmap.
    destruct (_ !! i) as [[τ e]|] eqn:?; do 2 f_equal/=.
    by eapply (H _ (Attr _ _)).
Qed.

Lemma subst_union ds1 ds2 e :
  subst (union_kinded ds1 ds2) e = subst ds1 (subst ds2 e).
Proof.
  revert ds1 ds2. induction e; intros ds1 ds2; f_equal/=; auto.
  - rewrite lookup_union_with.
    destruct mkd as [[[]]|],
      (ds1 !! x) as [[[] t1]|], (ds2 !! x) as [[[] t2]|]; naive_solver.
  - apply map_eq=> y. rewrite !lookup_fmap.
    destruct (_ !! y) as [[e'|]|] eqn:Hy; do 2 f_equal/=.
    rewrite -(H _ _ Hy) //.
  - induction H; f_equal/=; auto.
  - apply map_eq=> y. rewrite !lookup_fmap.
    destruct (_ !! y) as [[τ e]|] eqn:Hy; do 2 f_equal/=.
    rewrite -(H _ _ Hy) //.
Qed.

Lemma SAppL μ e1 e1' e2 :
  e1 -{SHALLOW}-> e1' → EApp e1 e2 -{μ}-> EApp e1' e2.
Proof. apply (SCtx (λ e, EApp e _)). constructor. Qed.
Lemma SAppR μ ms strict e1 e2 e2' :
  e2 -{SHALLOW}-> e2' →
  EApp (EAbsMatch ms strict e1) e2 -{μ}-> EApp (EAbsMatch ms strict e1) e2'.
Proof. apply SCtx. constructor. Qed.
Lemma SSeq μ μ' e1 e1' e2 :
  e1 -{μ'}-> e1' → ESeq μ' e1 e2 -{μ}-> ESeq μ' e1' e2.
Proof. apply (SCtx (λ e, ESeq _ e _)). constructor. Qed.
Lemma SList es1 e e' es2 :
  Forall (final DEEP) es1 →
  e -{DEEP}-> e' →
  EList (es1 ++ e :: es2) -{DEEP}-> EList (es1 ++ e' :: es2).
Proof. intros ?. apply (SCtx (λ e, EList (_ ++ e :: _))). by constructor. Qed.
Lemma SAttr αs x e e' :
  no_recs αs →
  αs !! x = None →
  (∀ y α, αs !! y = Some α → final DEEP (attr_expr α) ∨ attr_le x y) →
  e -{DEEP}-> e' →
  EAttr (<[x:=AttrN e]> αs) -{DEEP}-> EAttr (<[x:=AttrN e']> αs).
Proof. intros ???. apply (SCtx (λ e, EAttr (<[x:=AttrN e]> _))). by constructor. Qed.
Lemma SLetAttr μ k e1 e1' e2 :
  e1 -{SHALLOW}-> e1' → ELetAttr k e1 e2 -{μ}-> ELetAttr k e1' e2.
Proof. apply (SCtx (λ e, ELetAttr _ e _)). constructor. Qed.
Lemma SBinOpL μ op e1 e1' e2 :
  e1 -{SHALLOW}-> e1' → EBinOp op e1 e2 -{μ}-> EBinOp op e1' e2.
Proof. apply (SCtx (λ e, EBinOp _ e _)). constructor. Qed.
Lemma SBinOpR μ op e1 Φ e2 e2' :
  final SHALLOW e1 → sem_bin_op op e1 Φ →
  e2 -{SHALLOW}-> e2' → EBinOp op e1 e2 -{μ}-> EBinOp op e1 e2'.
Proof. intros ??. apply SCtx. by econstructor. Qed.
Lemma SIf μ e1 e1' e2 e3 :
  e1 -{SHALLOW}-> e1' → EIf e1 e2 e3 -{μ}-> EIf e1' e2 e3.
Proof. apply (SCtx (λ e, EIf e _ _)). constructor. Qed.

Global Hint Constructors step : step.
Global Hint Resolve SAppL SAppR SSeq SList SAttr SLetAttr SBinOpL SBinOpR SIf : step.

Lemma step_not_final μ e1 e2 : e1 -{μ}-> e2 → ¬final μ e1.
Proof.
  assert (∀ (αs : gmap string attr) x μ e,
    map_Forall (λ _, final DEEP ∘ attr_expr) (<[x:=Attr μ e]> αs) → final DEEP e).
  { intros αs x μ' e Hall. eapply (Hall _ (Attr _ _)), lookup_insert. }
  induction 1; inv 1; inv_step; decompose_Forall; naive_solver.
Qed.
Lemma final_nf μ e : final μ e → nf (step μ) e.
Proof. by intros ? [??%step_not_final]. Qed.

Lemma step_any_shallow μ e1 e2 :
  e1 -{μ}-> e2 → e1 -{SHALLOW}-> e2 ∨ final SHALLOW e1.
Proof.
  induction 1; inv_step;
    naive_solver eauto using final, no_recs_insert with step.
Qed.

Lemma step_shallow_any μ e1 e2 : e1 -{SHALLOW}-> e2 → e1 -{μ}-> e2.
Proof.
  remember SHALLOW as μ'. induction 1; inv_step; simplify_eq/=; eauto with step.
Qed.
Lemma steps_shallow_any μ e1 e2 : e1 -{SHALLOW}->* e2 → e1 -{μ}->* e2.
Proof. induction 1; eauto using rtc, step_shallow_any. Qed.
Lemma final_any_shallow μ e : final μ e → final SHALLOW e.
Proof. destruct μ; [done|]. induction 1; simplify_eq/=; eauto using final. Qed.
Lemma stuck_shallow_any μ e : stuck SHALLOW e → stuck μ e.
Proof.
  intros [Hnf Hfinal]. split; [|naive_solver eauto using final_any_shallow].
  intros [e' Hstep%step_any_shallow]; naive_solver.
Qed.

Lemma step_final_shallow μ e1 e2 :
  final SHALLOW e1 → e1 -{μ}-> e2 → final SHALLOW e2.
Proof.
  induction 1; intros; inv_step; decompose_Forall;
    eauto using step, final, no_recs_insert; try done.
  - by odestruct step_not_final.
  - apply map_Forall_insert in H0 as [??]; simpl in *; last done.
    by odestruct step_not_final.
Qed.

Lemma SAppL_rtc μ e1 e1' e2 :
  e1 -{SHALLOW}->* e1' → EApp e1 e2 -{μ}->* EApp e1' e2.
Proof. induction 1; econstructor; eauto with step. Qed.
Lemma SAppR_rtc μ ms strict e1 e2 e2' :
  e2 -{SHALLOW}->* e2' →
  EApp (EAbsMatch ms strict e1) e2 -{μ}->* EApp (EAbsMatch ms strict e1) e2'.
Proof. induction 1; econstructor; eauto with step. Qed.
Lemma SSeq_rtc μ μ' e1 e1' e2 :
  e1 -{μ'}->* e1' → ESeq μ' e1 e2 -{μ}->* ESeq μ' e1' e2.
Proof. induction 1; econstructor; eauto with step. Qed.
Lemma SList_rtc es1 e e' es2 :
  Forall (final DEEP) es1 →
  e -{DEEP}->* e' →
  EList (es1 ++ e :: es2) -{DEEP}->* EList (es1 ++ e' :: es2).
Proof. induction 2; econstructor; eauto with step. Qed.
Lemma SLetAttr_rtc μ k e1 e1' e2 :
  e1 -{SHALLOW}->* e1' → ELetAttr k e1 e2 -{μ}->* ELetAttr k e1' e2.
Proof. induction 1; econstructor; eauto with step. Qed.
Lemma SBinOpL_rtc μ op e1 e1' e2 :
  e1 -{SHALLOW}->* e1' → EBinOp op e1 e2 -{μ}->* EBinOp op e1' e2.
Proof. induction 1; econstructor; eauto with step. Qed.
Lemma SBinOpR_rtc μ op e1 Φ e2 e2' :
  final SHALLOW e1 → sem_bin_op op e1 Φ →
  e2 -{SHALLOW}->* e2' → EBinOp op e1 e2 -{μ}->* EBinOp op e1 e2'.
Proof. induction 3; econstructor; eauto with step. Qed.
Lemma SIf_rtc μ e1 e1' e2 e3 :
  e1 -{SHALLOW}->* e1' → EIf e1 e2 e3 -{μ}->* EIf e1' e2 e3.
Proof. induction 1; econstructor; eauto with step. Qed.

Lemma SApp_tc μ e1 e1' e2 :
  e1 -{SHALLOW}->+ e1' → EApp e1 e2 -{μ}->+ EApp e1' e2.
Proof. induction 1; by econstructor; eauto with step. Qed.
Lemma SSeq_tc μ μ' e1 e1' e2 :
  e1 -{μ'}->+ e1' → ESeq μ' e1 e2 -{μ}->+ ESeq μ' e1' e2.
Proof. induction 1; by econstructor; eauto with step. Qed.
Lemma SList_tc es1 e e' es2 :
  Forall (final DEEP) es1 →
  e -{DEEP}->+ e' →
  EList (es1 ++ e :: es2) -{DEEP}->+ EList (es1 ++ e' :: es2).
Proof. induction 2; by econstructor; eauto with step. Qed.
Lemma SLetAttr_tc μ k e1 e1' e2 :
  e1 -{SHALLOW}->+ e1' → ELetAttr k e1 e2 -{μ}->+ ELetAttr k e1' e2.
Proof. induction 1; by econstructor; eauto with step. Qed.
Lemma SBinOpL_tc μ op e1 e1' e2 :
  e1 -{SHALLOW}->+ e1' → EBinOp op e1 e2 -{μ}->+ EBinOp op e1' e2.
Proof. induction 1; by econstructor; eauto with step. Qed.
Lemma SBinOpR_tc μ op e1 Φ e2 e2' :
  final SHALLOW e1 → sem_bin_op op e1 Φ →
  e2 -{SHALLOW}->+ e2' → EBinOp op e1 e2 -{μ}->+ EBinOp op e1 e2'.
Proof. induction 3; by econstructor; eauto with step. Qed.
Lemma SIf_tc μ e1 e1' e2 e3 :
  e1 -{SHALLOW}->+ e1' → EIf e1 e2 e3 -{μ}->+ EIf e1' e2 e3.
Proof. induction 1; by econstructor; eauto with step. Qed.

Lemma SList_inv es1 e2 :
  EList es1 -{DEEP}-> e2 ↔ ∃ ds1 ds2 e e',
    es1 = ds1 ++ e :: ds2 ∧ e2 = EList (ds1 ++ e' :: ds2) ∧
    Forall (final DEEP) ds1 ∧
    e -{DEEP}-> e'.
Proof. split; intros; inv_step; naive_solver eauto using SList. Qed.

Lemma List_nf_cons_final es e :
  final DEEP e →
  nf (step DEEP) (EList es) →
  nf (step DEEP) (EList (e :: es)).
Proof.
  intros Hfinal Hnf [e' (ds1 & ds2 & e1 & e2 & ? & -> & Hds1 & Hstep)%SList_inv].
  destruct Hds1; simplify_eq/=.
  - by apply step_not_final in Hstep.
  - naive_solver eauto with step.
Qed.
Lemma List_nf_cons es e :
  ¬final DEEP e →
  nf (step DEEP) e →
  nf (step DEEP) (EList (e :: es)).
Proof.
  intros Hfinal Hnf [e' (ds1 & ds2 & e1 & e2 & ? & -> & Hds1 & Hstep)%SList_inv].
  destruct Hds1; naive_solver.
Qed.

Lemma List_steps_cons es1 es2 e :
  final DEEP e →
  EList es1 -{DEEP}->* EList es2 →
  EList (e :: es1) -{DEEP}->* EList (e :: es2).
Proof.
  intros ? Hstep.
  remember (EList es1) as e1 eqn:He1; remember (EList es2) as e2 eqn:He2.
  revert es1 es2 He1 He2.
  induction Hstep as [|e1 e2 e3 Hstep Hstep' IH];
    intros es1 es3 ??; simplify_eq/=; [done|].
  inv_step. eapply rtc_l; [apply (SList (_ :: _))|]; naive_solver.
Qed.

Lemma SAttr_rec_rtc μ αs :
  EAttr αs -{μ}->*
    EAttr (AttrN ∘ from_attr (subst (indirects αs)) id <$> αs).
Proof.
  destruct (decide (no_recs αs)) as [Hαs|]; [|by eauto using rtc_once, step].
  eapply reflexive_eq. f_equal. apply map_eq=> x. rewrite lookup_fmap.
  destruct (αs !! x) as [[τ e]|] eqn:?; [|done].
  assert (τ = NONREC) as -> by eauto using no_recs_lookup. done.
Qed.

Lemma SAttr_lookup_rtc αs x e e' :
  no_recs αs →
  αs !! x = None →
  (∀ y α, αs !! y = Some α → final DEEP (attr_expr α) ∨ attr_le x y) →
  e -{DEEP}->* e' →
  EAttr (<[x:=AttrN e]> αs) -{DEEP}->* EAttr (<[x:=AttrN e']> αs).
Proof.
  intros Hrecs Hx Hfirst He. revert αs Hrecs Hx Hfirst.
  induction He as [e|e1 e2 e3 He12 He23 IH]; intros eτs Hrec Hx Hfirst; [done|].
  eapply rtc_l; first by eapply SAttr. apply IH; [done..|].
  apply step_not_final in He12. naive_solver.
Qed.

Lemma SAttr_inv αs1 e2 :
  no_recs αs1 →
  EAttr αs1 -{DEEP}-> e2 ↔ ∃ αs x e e',
    αs1 = <[x:=AttrN e]> αs ∧ e2 = EAttr (<[x:=AttrN e']> αs) ∧
    αs !! x = None ∧
    (∀ y α, αs !! y = Some α → final DEEP (attr_expr α) ∨ attr_le x y) ∧
    e -{DEEP}-> e'.
Proof.
  split; [intros; inv_step|];
    naive_solver eauto using SAttr, no_recs_insert_inv.
Qed.

Lemma Attr_nf_insert_final αs x e :
  no_recs αs →
  αs !! x = None →
  final DEEP e →
  (∀ y, is_Some (αs !! y) → attr_le x y) →
  nf (step DEEP) (EAttr αs) →
  nf (step DEEP) (EAttr (<[x:=AttrN e]> αs)).
Proof.
  intros Hrecs Hx Hfinal Hleast Hnf
    [? (αs'&x'&e'&e''&Hαs&->&Hx'&?&Hstep)%SAttr_inv];
    last by eauto using no_recs_insert.
  assert (x ≠ x').
  { intros ->. apply (f_equal (.!! x')) in Hαs. rewrite !lookup_insert in Hαs.
    apply step_not_final in Hstep. naive_solver. }
  destruct Hnf. exists (EAttr (<[x':=AttrN e'']> (delete x αs'))).
  rewrite -(delete_insert αs x (AttrN e)) // Hαs delete_insert_ne //.
  refine (SCtx _ _ _ _ _ (CAttr _ _ _ _ _) _);
    [|by rewrite lookup_delete_ne| |done].
  - apply (no_recs_insert _ x e) in Hrecs. rewrite Hαs in Hrecs.
    apply no_recs_insert_inv in Hrecs; last done. by apply map_Forall_delete.
  - intros ?? ?%lookup_delete_Some; naive_solver.
Qed.
Lemma Attr_nf_insert αs x e :
  no_recs αs →
  αs !! x = None →
  ¬final DEEP e →
  (∀ y, is_Some (αs !! y) → attr_le x y) →
  nf (step DEEP) e →
  nf (step DEEP) (EAttr (<[x:=AttrN e]> αs)).
Proof.
  intros Hrecs Hx ?? Hnf [? (αs'&x'&e'&e''&Hαs&->&Hx'&Hleast'&Hstep)%SAttr_inv];
    last eauto using no_recs_insert.
  assert (x ≠ x') as Hxx'.
  { intros ->. apply (f_equal (.!! x')) in Hαs. rewrite !lookup_insert in Hαs.
    naive_solver. }
  odestruct (Hleast' x (AttrN e)); [|done|].
  - apply (f_equal (.!! x)) in Hαs.
    by rewrite lookup_insert lookup_insert_ne in Hαs.
  - apply (f_equal (.!! x')) in Hαs.
    rewrite lookup_insert lookup_insert_ne // in Hαs.
    destruct Hxx'. apply (anti_symm attr_le); naive_solver.
Qed.

Lemma Attr_step_dom μ αs1 e2 :
  EAttr αs1 -{μ}-> e2 →
  ∃ αs2, e2 = EAttr αs2 ∧ ∀ i, αs1 !! i = None ↔ αs2 !! i = None.
Proof.
  intros; inv_step; (eexists; split; [done|]).
  - intros i. by rewrite lookup_fmap fmap_None.
  - intros i. rewrite !lookup_insert_None; naive_solver.
Qed.
Lemma Attr_steps_dom μ αs1 αs2 :
  EAttr αs1 -{μ}->* EAttr αs2 → ∀ i, αs1 !! i = None ↔ αs2 !! i = None.
Proof.
  intros Hstep.
  remember (EAttr αs1) as e1 eqn:He1; remember (EAttr αs2) as e2 eqn:He2.
  revert αs1 αs2 He1 He2. induction Hstep as [|e1 e2 e3 Hstep Hstep' IH];
    intros αs1 αs3 ??; simplify_eq/=; [done|].
  apply Attr_step_dom in Hstep; naive_solver.
Qed.

Lemma Attr_step_recs αs1 αs2 :
  EAttr αs1 -{DEEP}-> EAttr αs2 → no_recs αs1 → no_recs αs2.
Proof. intros. inv_step; by eauto using no_recs_insert. Qed.
Lemma Attr_steps_recs αs1 αs2 :
  EAttr αs1 -{DEEP}->* EAttr αs2 → no_recs αs1 → no_recs αs2.
Proof.
  intros Hstep.
  remember (EAttr αs1) as e1 eqn:He1; remember (EAttr αs2) as e2 eqn:He2.
  revert αs1 αs2 He1 He2. induction Hstep as [|e1 e2 e3 Hstep Hstep' IH];
    intros αs1 αs3 ???; simplify_eq/=; [done|].
  pose proof (Attr_step_dom _ _ _ Hstep) as (es2 & -> & ?).
  apply Attr_step_recs in Hstep; naive_solver.
Qed.

Lemma Attr_step_insert αs1 αs2 x e :
  no_recs αs1 →
  αs1 !! x = None →
  final DEEP e →
  EAttr αs1 -{DEEP}-> EAttr αs2 →
  EAttr (<[x:=AttrN e]> αs1) -{DEEP}-> EAttr (<[x:=AttrN e]> αs2).
Proof.
  intros Hrecs Hx ?
    (αs' & x' & e1 & e1' & ? & ? & ? & ? & ?)%SAttr_inv; [|done]; simplify_eq.
  apply lookup_insert_None in Hx as [??]. rewrite !(insert_commute _ x) //.
  eapply SAttr; [|by rewrite lookup_insert_ne| |done].
  - by eapply no_recs_insert, no_recs_insert_inv.
  - intros y e' ?%lookup_insert_Some; naive_solver.
Qed.
Lemma Attr_steps_insert αs1 αs2 x e :
  no_recs αs1 →
  αs1 !! x = None →
  final DEEP e →
  EAttr αs1 -{DEEP}->* EAttr αs2 →
  EAttr (<[x:=AttrN e]> αs1) -{DEEP}->* EAttr (<[x:=AttrN e]> αs2).
Proof.
  intros Hrecs Hx ? Hstep.
  remember (EAttr αs1) as e1 eqn:He1; remember (EAttr αs2) as e2 eqn:He2.
  revert αs1 αs2 Hx Hrecs He1 He2.
  induction Hstep as [|e1 e2 e3 Hstep Hstep' IH];
    intros αs1 αs3 ????; simplify_eq/=; [done|].
  pose proof (Attr_step_dom _ _ _ Hstep) as (αs2 & -> & Hdom).
  eapply rtc_l; first by eapply Attr_step_insert.
  eapply IH; naive_solver eauto using Attr_step_recs.
Qed.

Reserved Infix "=D=>" (right associativity, at level 55).

Inductive step_delayed : relation expr :=
  | RDrefl e :
      e =D=> e
  | RDId x e1 e2 :
      e1 =D=> e2 →
      EId x (Some (ABS, e1)) =D=> e2
  | RDBinOp op e1 e1' e2 e2' :
      e1 =D=> e1' → e2 =D=> e2' → EBinOp op e1 e2 =D=> EBinOp op e1' e2'
  | RDIf e1 e1' e2 e2' e3 e3' :
      e1 =D=> e1' → e2 =D=> e2' → e3 =D=> e3' → EIf e1 e2 e3 =D=> EIf e1' e2' e3'
where "e1 =D=> e2" := (step_delayed e1 e2).

Global Instance step_delayed_po : PreOrder step_delayed.
Proof.
  split; [constructor|].
  intros e1 e2 e3 Hstep. revert e3.
  induction Hstep; inv 1; eauto using step_delayed.
Qed.
Hint Extern 0 (_ =D=> _) => reflexivity : core.

Lemma delayed_final_l e1 e2 :
  final SHALLOW e1 →
  e1 =D=> e2 →
  e1 = e2.
Proof. intros Hfinal. induction 1; try by inv Hfinal. Qed.

Lemma delayed_final_r μ e1 e2 :
  final μ e2 →
  e1 =D=> e2 →
  e1 -{μ}->* e2.
Proof.
  intros Hfinal. induction 1; try by inv Hfinal.
  eapply rtc_l; [constructor|]. eauto.
Qed.

Lemma delayed_step_l μ e1 e1' e2 :
  e1 =D=> e1' →
  e1 -{μ}-> e2 →
  ∃ e2', e1' -{μ}->* e2' ∧ e2 =D=> e2'.
Proof.
  intros Hrem. revert μ e2.
  induction Hrem; intros μ ? Hstep.
  - eauto using rtc_once.
  - inv_step. by exists e2.
  - inv_step.
    + eapply delayed_final_l in Hrem1 as ->, Hrem2 as ->; [|by eauto..].
      eexists; split; [|done]. eapply rtc_once. by econstructor.
    + apply IHHrem1 in H2 as (e1'' & ? & ?).
      eexists; split; [by eapply SBinOpL_rtc|]. by constructor.
    + eapply delayed_final_l in Hrem1 as ->; [|by eauto..].
      apply IHHrem2 in H2 as (e2'' & ? & ?).
      eexists (EBinOp _ e1' e2''); split; [|by constructor].
      by eapply SBinOpR_rtc.
  - inv_step.
    + eapply delayed_final_l in Hrem1 as <-; [|by repeat constructor].
      eexists; split; [eapply rtc_once; constructor|]. by destruct b.
    + apply IHHrem1 in H2 as (e1'' & ? & ?).
      eexists; split; [by eapply SIf_rtc|]. by constructor.
Qed.

Lemma delayed_steps_l μ e1 e1' e2 :
  e1 =D=> e1' →
  e1 -{μ}->* e2 →
  ∃ e2', e1' -{μ}->* e2' ∧ e2 =D=> e2'.
Proof.
  intros Hdel Hsteps. revert e1' Hdel.
  induction Hsteps as [e|e1 e2 e3 Hstep Hsteps IH]; intros e1' Hdel.
  { eexists; by split. }
  eapply delayed_step_l in Hstep as (e2' & Hstep2 & Hdel2); [|done].
  apply IH in Hdel2 as (e3' & ? & ?). eexists; by split; [etrans|].
Qed.

Lemma delayed_step_r μ e1 e1' e2 :
  e1' =D=> e1 →
  e1 -{μ}-> e2 →
  ∃ e2', e1' -{μ}->+ e2' ∧ e2' =D=> e2.
Proof.
  intros Hrem. revert μ e2.
  induction Hrem; intros μ ? Hstep.
  - eauto using tc_once.
  - apply IHHrem in Hstep as (e1' & ? & ?).
    eexists. split; [|done]. eapply tc_l; [econstructor|done].
  - inv_step.
    + exists e0; split; [|done].
      eapply tc_rtc_l; [by eapply SBinOpL_rtc, delayed_final_r, Hrem1|].
      eapply tc_rtc_l; [by eapply SBinOpR_rtc, delayed_final_r, Hrem2|].
      eapply tc_once. by econstructor.
    + apply IHHrem1 in H2 as (e1'' & ? & ?).
      eexists; split; [by eapply SBinOpL_tc|]. by constructor.
    + apply IHHrem2 in H2 as (e2'' & ? & ?).
      eexists (EBinOp _ e1' e2''); split; [|by apply RDBinOp].
      eapply tc_rtc_l; [by eapply SBinOpL_rtc, delayed_final_r, Hrem1|].
      by eapply SBinOpR_tc.
  - inv_step.
    + exists (if b then e2 else e3). split; [|by destruct b].
      eapply tc_rtc_l;
        [eapply SIf_rtc, delayed_final_r, Hrem1; by repeat constructor|].
      eapply tc_once; constructor.
    + apply IHHrem1 in H2 as (e1'' & ? & ?).
      eexists; split; [by eapply SIf_tc|]. by constructor.
Qed.

Lemma delayed_steps_r μ e1 e1' e2 :
  e1' =D=> e1 →
  e1 -{μ}->* e2 →
  ∃ e2', e1' -{μ}->* e2' ∧ e2' =D=> e2.
Proof.
  intros Hdel Hsteps. revert e1' Hdel.
  induction Hsteps as [e|e1 e2 e3 Hstep Hsteps IH]; intros e1' Hdel.
  { eexists; by split. }
  eapply delayed_step_r in Hstep as (e2' & Hstep2%tc_rtc & Hdel2); [|done].
  apply IH in Hdel2 as (e3' & ? & ?). eexists; by split; [etrans|].
Qed.

(** Determinism *)

Lemma bin_op_det op e Φ Ψ :
  sem_bin_op op e Φ →
  sem_bin_op op e Ψ →
  Φ = Ψ.
Proof. by destruct 1; inv 1. Qed.

Lemma bin_op_rel_det op e1 Φ e2 d1 d2 :
  sem_bin_op op e1 Φ →
  Φ e2 d1 →
  Φ e2 d2 →
  d1 = d2.
Proof.
  assert (AntiSymm eq attr_le) by apply _.
  unfold AntiSymm in *. inv 1; repeat case_match; naive_solver.
Qed.

Lemma matches_present x e md es ms strict βs :
  es !! x = Some e → ms !! x = Some md →
  matches es ms strict βs →
  βs !! x = Some (AttrN e).
Proof.
  intros Hes Hms. induction 1; try done.
  - by apply lookup_insert_Some in Hes as [[]|[]]; simplify_map_eq.
  - by simplify_map_eq.
Qed.

Lemma matches_default x es ms d strict βs :
  es !! x = None →
  ms !! x = Some (Some d) →
  matches es ms strict βs →
  βs !! x = Some (AttrR d).
Proof.
  intros Hes Hms. induction 1; try done.
  - by apply lookup_insert_None in Hes as []; simplify_map_eq.
  - by apply lookup_insert_Some in Hms as [[]|[]]; simplify_map_eq.
Qed.

Lemma matches_weaken x es ms strict βs :
  matches es ms strict βs →
  matches (delete x es) (delete x ms) strict (delete x βs).
Proof.
  induction 1; [constructor|constructor|..]; rename x0 into y;
    (destruct (decide (x = y)) as [->|Hxy];
      [ rewrite !delete_insert_delete //
      | rewrite !delete_insert_ne //; constructor;
        by simplify_map_eq ]).
Qed.

Lemma matches_det es ms strict βs1 βs2 :
  matches es ms strict βs1 →
  matches es ms strict βs2 →
  βs1 = βs2.
Proof.
  intros Hβs1. revert βs2. induction Hβs1; intros βs2 Hβs2;
    try (inv Hβs2; done || (by exfalso; eapply (insert_non_empty (M:=stringmap)))).
  - eapply (matches_weaken x) in Hβs2 as Hβs2'.
    rewrite !delete_insert // in Hβs2'.
    rewrite (IHHβs1 _ Hβs2') insert_delete //.
    eapply matches_present; eauto; apply lookup_insert.
  - eapply (matches_weaken x) in Hβs2 as Hβs2'.
    rewrite delete_notin // delete_insert // in Hβs2'.
    rewrite (IHHβs1 _ Hβs2') insert_delete //.
    eapply matches_default; eauto. apply lookup_insert.
Qed.

Lemma ctx_det K1 K2 e1 e2 μ μ1' μ2' :
  K1 e1 = K2 e2 →
  ctx1 μ1' μ K1 →
  ctx1 μ2' μ K2 →
  red (step μ1') e1 →
  red (step μ2') e2 →
  K1 = K2 ∧ e1 = e2 ∧ μ1' = μ2'.
Proof.
  intros Hes HK1 HK2 Hred1 Hred2.
  induction HK1; inv HK2; try done.
  - apply not_elem_of_app_cons_inv_l in Hes as [<- [<- <-]]; first done.
    + intros He1. apply (proj1 (Forall_forall _ _) H0) in He1.
      inv Hred1. by apply step_not_final in H1.
    + intros He2. apply (proj1 (Forall_forall _ _) H) in He2.
      inv Hred2. by apply step_not_final in H1.
  - destruct (decide (x = x0)) as [<-|].
    { by apply map_insert_inv_eq in Hes as [[= ->] [= ->]]. }
    apply map_insert_inv_ne in Hes as (Hx0 & Hx & Hαs); try done.
    apply H1 in Hx0 as [contra | Hxlex0].
    + inv Hred2. by apply step_not_final in H5.
    + apply H4 in Hx as [contra | Hx0lex].
      * inv Hred1. by apply step_not_final in H5.
      * assert (Hasym : AntiSymm eq attr_le) by apply _.
        by pose proof (Hasym _ _ Hxlex0 Hx0lex).
  - inv Hred1. inv_step.
  - inv Hred2. inv_step.
  - inv Hred1. by apply step_not_final in H1.
  - inv Hred2. by apply step_not_final in H1.
Qed.

Lemma step_det μ e d1 d2 :
  e -{μ}-> d1 →
  e -{μ}-> d2 →
  d1 = d2.
Proof.
  intros Hred1. revert d2.
  induction Hred1; intros d2 Hred2; inv Hred2; try by inv_step.
  - by apply (matches_det _ _ _ _ _ H0) in H8 as <-.
  - inv_step. by apply step_not_final in H3.
  - inv_step. destruct H. by apply no_recs_insert.
  - assert (Φ = Φ0) as <- by (by eapply bin_op_det).
    by eapply bin_op_rel_det.
  - inv_step; by apply step_not_final in H6.
  - inv_step. by apply step_not_final in Hred1.
  - inv_step. destruct H2. by apply no_recs_insert.
  - inv_step; by apply step_not_final in Hred1.
  - eapply ctx_det in H0 as (?&?&?); [|by eauto..]; naive_solver.
Qed.