From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Mon, 7 Jul 2025 21:52:08 +0200 Subject: Initialize repository --- theories/nix/operational_props.v | 680 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 680 insertions(+) create mode 100644 theories/nix/operational_props.v (limited to 'theories/nix/operational_props.v') diff --git a/theories/nix/operational_props.v b/theories/nix/operational_props.v new file mode 100644 index 0000000..4041bfe --- /dev/null +++ b/theories/nix/operational_props.v @@ -0,0 +1,680 @@ +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. -- cgit v1.2.3