From 73df1945b31c0beee88cf4476df4ccd09d31403b Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Wed, 26 Jun 2024 20:50:18 +0200 Subject: Import Coq project --- .envrc | 1 + .gitignore | 12 ++ Makefile | 20 ++ _CoqProject | 1 + binop.v | 87 ++++++++ complete.v | 413 ++++++++++++++++++++++++++++++++++++++ correct.v | 299 ++++++++++++++++++++++++++++ expr.v | 250 +++++++++++++++++++++++ flake.lock | 61 ++++++ flake.nix | 23 +++ interpreter.v | 103 ++++++++++ maptools.v | 476 ++++++++++++++++++++++++++++++++++++++++++++ matching.v | 609 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ relations.v | 73 +++++++ sem.v | 167 ++++++++++++++++ semprop.v | 426 +++++++++++++++++++++++++++++++++++++++ shared.v | 66 ++++++ sound.v | 630 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 18 files changed, 3717 insertions(+) create mode 100644 .envrc create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 _CoqProject create mode 100644 binop.v create mode 100644 complete.v create mode 100644 correct.v create mode 100644 expr.v create mode 100644 flake.lock create mode 100644 flake.nix create mode 100644 interpreter.v create mode 100644 maptools.v create mode 100644 matching.v create mode 100644 relations.v create mode 100644 sem.v create mode 100644 semprop.v create mode 100644 shared.v create mode 100644 sound.v diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..3550a30 --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..9e35ae7 --- /dev/null +++ b/.gitignore @@ -0,0 +1,12 @@ +*.aux +*.glob +*.vio +*.vo +*.vok +*.vos +.CoqMakefile.d +.Makefile.coq.d +.direnv +.lia.cache +Makefile.coq +Makefile.coq.conf diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..1e32cef --- /dev/null +++ b/Makefile @@ -0,0 +1,20 @@ +# Modified from the Logical Foundations Makefile + +COQMFFLAGS := -Q . mininix + +ALLVFILES := maptools.v relations.v expr.v shared.v binop.v matching.v sem.v \ + interpreter.v complete.v sound.v correct.v semprop.v + +build: Makefile.coq + $(MAKE) -f Makefile.coq + +clean:: + if [ -e Makefile.coq ]; then $(MAKE) -f Makefile.coq cleanall; fi + $(RM) $(wildcard Makefile.coq Makefile.coq.conf) + +Makefile.coq: + coq_makefile $(COQMFFLAGS) -o Makefile.coq $(ALLVFILES) + +-include Makefile.coq + +.PHONY: build clean diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..145dd21 --- /dev/null +++ b/_CoqProject @@ -0,0 +1 @@ +-Q . mininix diff --git a/binop.v b/binop.v new file mode 100644 index 0000000..c8f87fd --- /dev/null +++ b/binop.v @@ -0,0 +1,87 @@ +Require Import Coq.NArith.BinNat. +Require Import Coq.Strings.Ascii. +Require Import Coq.Strings.String. +From stdpp Require Import fin_sets gmap option. +From mininix Require Import expr maptools shared. + +Open Scope string_scope. +Open Scope N_scope. +Open Scope Z_scope. +Open Scope nat_scope. + +Definition right_union {A} (bs1 bs2 : gmap string A) : gmap string A := + bs2 ∪ bs1. + +Variant binop_r : op → value → value → value → Prop := + | Bo_PlusInt n1 n2 : binop_r O_Plus (V_Int n1) (V_Int n2) (V_Int (n1 + n2)) + | Bo_PlusStr s1 s2 : binop_r O_Plus (V_Str s1) (V_Str s2) (V_Str (s1 ++ s2)) + | Bo_MinInt n1 n2 : binop_r O_Min (V_Int n1) (V_Int n2) (V_Int (n1 - n2)) + | Bo_UpdAttrset bs1 bs2 : + binop_r O_Upd (V_Attrset bs1) (V_Attrset bs2) + (V_Attrset (right_union bs1 bs2)) + | Bo_Eq v1 v2 : binop_r O_Eq v1 v2 (expr_eq v1 v2) + | Bo_DivInt (n1 n2 : Z) : n2 ≠ 0%Z → binop_r O_Div n1 n2 (n1 / n2)%Z + | Bo_LtInt (n1 n2 : Z) : binop_r O_Lt n1 n2 (bool_decide (n1 < n2)%Z) + | Bo_LtStr s1 s2 : binop_r O_Lt (V_Str s1) (V_Str s2) (string_lt s1 s2). + +Notation "u1 '⟦' op '⟧' u2 '-⊚->' v" := (binop_r op u1 u2 v) (at level 55). + +Definition binop_eval (op : op) (v1 v2 : value) : option value := + match op with + | O_Plus => + match v1, v2 with + | V_Int n1, V_Int n2 => Some (V_Int (n1 + n2)) + | V_Str s1, V_Str s2 => Some (V_Str (s1 ++ s2)) + | _, _ => None + end + | O_Min => + match v1, v2 with + | V_Int n1, V_Int n2 => Some (V_Int (n1 - n2)) + | _, _ => None + end + | O_Upd => + match v1, v2 with + | V_Attrset bs1, V_Attrset bs2 => + Some (V_Attrset (right_union bs1 bs2)) + | _, _ => None + end + | O_Eq => Some (V_Bool (expr_eq (X_V v1) (X_V v2))) + | O_Div => + match v1, v2 with + | V_Int n1, V_Int n2 => + if decide (n2 = 0)%Z + then None + else Some (V_Int (n1 / n2)%Z) + | _, _ => None + end + | O_Lt => + match v1, v2 with + | V_Int n1, V_Int n2 => Some (V_Bool (bool_decide (n1 < n2)%Z)) + | V_Str s1, V_Str s2 => Some (V_Bool (string_lt s1 s2)) + | _, _ => None + end + end. + +Theorem binop_eval_sound op u1 u2 v : + binop_eval op u1 u2 = Some v → binop_r op u1 u2 v. +Proof. + intros Heval. + destruct op, u1, u2; try discriminate; simplify_eq/=; try constructor. + destruct (decide (n0 = 0)%Z); try discriminate. + simplify_eq/=. by constructor. +Qed. + +Theorem binop_eval_complete op u1 u2 v : + binop_r op u1 u2 v → binop_eval op u1 u2 = Some v. +Proof. + intros Heval. inv Heval; try done. + unfold binop_eval. by apply decide_False. +Qed. + +Theorem binop_deterministic op u1 u2 v1 v2 : + u1 ⟦op⟧ u2 -⊚-> v1 → u1 ⟦op⟧ u2 -⊚-> v2 → v1 = v2. +Proof. + intros Heval1 Heval2. + apply binop_eval_complete in Heval1, Heval2. + congruence. +Qed. diff --git a/complete.v b/complete.v new file mode 100644 index 0000000..9939b50 --- /dev/null +++ b/complete.v @@ -0,0 +1,413 @@ +Require Import Coq.Strings.String. +From stdpp Require Import gmap relations. +From mininix Require Import binop expr interpreter maptools matching sem. + +Lemma eval_le n uf e v' : + eval n uf e = Some v' → + ∀ m, n ≤ m → eval m uf e = Some v'. +Proof. + revert uf e v'. + induction n; [discriminate|]. + intros uf e v' Heval [] Hle; [lia|]. + apply le_S_n in Hle. + rewrite eval_S in *. + destruct e; repeat (case_match || simplify_option_eq || by eauto). + apply bind_Some. exists H. + split; try by reflexivity. + apply map_mapM_Some_L in Heqo. + apply map_mapM_Some_L. + eapply map_Forall2_impl_L, Heqo. + eauto. +Qed. + +Lemma eval_value n (v : value) : 0 < n → eval n false v = Some v. +Proof. destruct n, v; by try lia. Qed. + +Lemma eval_strong_value n (sv : strong_value) : + 0 < n → + eval n false sv = Some (value_from_strong_value sv). +Proof. destruct n, sv; by try lia. Qed. + +Lemma eval_force_strong_value v : ∃ n, + eval n true (expr_from_strong_value v) = Some (value_from_strong_value v). +Proof. + induction v using strong_value_ind'; try by exists 2. + unfold expr_from_strong_value. simpl. + fold expr_from_strong_value. + induction bs using map_ind. + + by exists 2. + + apply map_Forall_insert in H as [[n Hn] H2]; try done. + apply IHbs in H2 as [o Ho]. clear IHbs. + exists (S (n `max` o)). + rewrite eval_S. csimpl. + setoid_rewrite map_mapM_Some_2_L + with (m2 := value_from_strong_value <$> <[i := x]>m); csimpl. + * by rewrite <-map_fmap_compose. + * destruct o as [|o]; csimpl in *; try discriminate. + apply map_Forall2_alt_L. + split. + -- set_solver. + -- intros j u v ??. rewrite eval_S in Ho. + apply bind_Some in Ho as [vs [Ho1 Ho2]]. + setoid_rewrite map_mapM_Some_L in Ho1. simplify_eq. + unfold expr_from_strong_value in Ho2. + rewrite map_fmap_compose in Ho2. + simplify_eq. + destruct (decide (i = j)). + ++ simplify_eq. + repeat rewrite lookup_fmap, lookup_insert in *. + simplify_eq/=. + apply eval_le with (n := n); lia || done. + ++ repeat rewrite lookup_fmap, lookup_insert_ne in * by done. + repeat rewrite <-lookup_fmap in *. + apply map_Forall2_alt_L in Ho1. + destruct Ho1 as [Ho1 Ho2]. + apply eval_le with (n := o); try lia. + by apply Ho2 with (i := j). +Qed. + +Lemma eval_force_strong_value' v : + ∃ n, eval n false (X_Force (expr_from_strong_value v)) = + Some (value_from_strong_value v). +Proof. + destruct (eval_force_strong_value v) as [n Heval]. + exists (S n). by rewrite eval_S. +Qed. + +Lemma rec_subst_lookup bs x e : + bs !! x = Some (B_Nonrec e) → rec_subst bs !! x = Some e. +Proof. unfold rec_subst. rewrite lookup_fmap. by intros ->. Qed. + +Lemma rec_subst_lookup_fmap bs x e : + bs !! x = Some e → rec_subst (B_Nonrec <$> bs) !! x = Some e. +Proof. unfold rec_subst. do 2 rewrite lookup_fmap. by intros ->. Qed. + +Lemma rec_subst_lookup_fmap' bs x : + is_Some (bs !! x) ↔ is_Some (rec_subst (B_Nonrec <$> bs) !! x). +Proof. + unfold rec_subst. split; + do 2 rewrite lookup_fmap in *; + intros [b H]; by simplify_option_eq. +Qed. + +Lemma eval_base_step uf e e' v'' n : + e -->base e' → + eval n uf e' = Some v'' → + ∃ m, eval m uf e = Some v''. +Proof. + intros [] Heval. + - (* E_Force *) + destruct uf. + + (* true *) + exists (S n). rewrite eval_S. by csimpl. + + (* false *) + destruct n; try discriminate. + rewrite eval_strong_value in Heval by lia. + simplify_option_eq. + apply eval_force_strong_value'. + - (* E_Closed *) + exists (S n). rewrite eval_S. by csimpl. + - (* E_Placeholder *) + exists (S n). rewrite eval_S. by csimpl. + - (* E_MSelect *) + destruct n; try discriminate. + rewrite eval_S in Heval. simplify_option_eq. + destruct ys. simplify_option_eq. + destruct n as [|[|n]]; try discriminate. + rewrite eval_S in Heqo. simplify_option_eq. + rewrite eval_S in Heqo1. simplify_option_eq. + exists (S (S (S (S n)))). rewrite eval_S. simplify_option_eq. + rewrite eval_value by lia. simplify_option_eq. + rewrite eval_S. simplify_option_eq. + rewrite eval_le with (n := S n) (v' := V_Attrset H0) by done || lia. + by simplify_option_eq. + - (* E_Select *) + exists (S n). rewrite eval_S. csimpl. + apply bind_Some. exists (V_Attrset (<[x := e0]>bs)). + destruct n; try discriminate. split; [done|]. + apply bind_Some. exists (<[x := e0]>bs). split; [done|]. + rewrite lookup_insert. by simplify_option_eq. + - (* E_SelectOr *) + destruct n; try discriminate. + rewrite eval_S in Heval. simplify_option_eq. + destruct n as [|[|n]]; try discriminate. + rewrite eval_S in Heqo. simplify_option_eq. + rewrite eval_S in Heqo0. simplify_option_eq. + exists (S (S (S n))). rewrite eval_S. simplify_option_eq. + rewrite eval_value by lia. simplify_option_eq. + case_match. + + rewrite bool_decide_eq_true in H. destruct H as [d Hd]. + simplify_option_eq. rewrite eval_S in Heval. simplify_option_eq. + rewrite eval_S in Heqo. simplify_option_eq. + apply eval_le with (n := S n); done || lia. + + rewrite bool_decide_eq_false in H. apply eq_None_not_Some in H. + by simplify_option_eq. + - (* E_MSelectOr *) + destruct n; try discriminate. + rewrite eval_S in Heval. simplify_option_eq. + destruct ys. simplify_option_eq. + destruct n as [|[|n]]; try discriminate. + rewrite eval_S in Heqo. simplify_option_eq. + rewrite eval_S in Heqo0. simplify_option_eq. + exists (S (S (S n))). rewrite eval_S. simplify_option_eq. + rewrite eval_value by lia. simplify_option_eq. + case_match. + + rewrite bool_decide_eq_true in H. destruct H as [d Hd]. + simplify_option_eq. rewrite eval_S in Heval. simplify_option_eq. + rewrite eval_S in Heqo. simplify_option_eq. + destruct n; try discriminate. rewrite eval_S in Heqo0. + simplify_option_eq. rewrite eval_S. + simplify_option_eq. + setoid_rewrite eval_le with (n := S n) (v' := V_Attrset H0); done || lia. + + rewrite bool_decide_eq_false in H. apply eq_None_not_Some in H. + by simplify_option_eq. + - (* E_Rec *) + exists (S n). rewrite eval_S. by csimpl. + - (* E_Let *) + exists (S n). rewrite eval_S. by csimpl. + - (* E_With *) + exists (S n). rewrite eval_S. csimpl. + apply bind_Some. exists (V_Attrset bs). + by destruct n; try discriminate. + - (* E_WithNoAttrset *) + exists (S n). rewrite eval_S. csimpl. + apply bind_Some. exists v1. + destruct v1; try by destruct n; try discriminate. + exfalso. apply H. by exists bs. + - (* E_ApplySimple *) + exists (S n). rewrite eval_S. simpl. + apply bind_Some. exists (V_Fn x e1). + split; [|assumption]. + destruct n; try discriminate; reflexivity. + - (* E_ApplyAttrset *) + exists (S n). rewrite eval_S. csimpl. + apply bind_Some. exists (V_AttrsetFn m e0). + destruct n; try discriminate. split; [done|]. + apply bind_Some. exists (V_Attrset bs). split; [done|]. + apply bind_Some. exists bs. split; [done|]. + apply bind_Some. apply matches_complete in H. + by exists bs'. + - (* E_ApplyFunctor *) + exists (S n). rewrite eval_S. csimpl. + apply bind_Some. exists (V_Attrset (<["__functor" := e2]>bs)). + destruct n; try discriminate. split; [done|]. + rewrite lookup_insert. by simplify_option_eq. + - (* E_IfTrue *) + exists (S n). rewrite eval_S. csimpl. + apply bind_Some. exists true. + by destruct n; try discriminate. + - (* E_IfFalse *) + exists (S n). rewrite eval_S. csimpl. + apply bind_Some. exists false. + by destruct n; try discriminate. + - (* E_Op *) + exists (S n). rewrite eval_S. simpl. + apply bind_Some. exists v1. + destruct n; try discriminate. + split. + + apply eval_value. lia. + + apply bind_Some. exists v2. split. + * apply eval_value. lia. + * apply binop_eval_complete in H. + apply bind_Some. by exists u. + - (* E_OpHasAttrTrue *) + exists (S n). rewrite eval_S. csimpl. + apply bind_Some. exists (V_Attrset bs). + destruct n; try discriminate. rewrite eval_S in Heval. + simplify_option_eq. by rewrite bool_decide_eq_true_2. + - (* E_OpHasAttrFalse *) + exists (S n). rewrite eval_S. csimpl. + apply bind_Some. exists (V_Attrset bs). + destruct n; try discriminate. rewrite eval_S in Heval. + simplify_option_eq. rewrite eq_None_not_Some in H. + by rewrite bool_decide_eq_false_2. + - (* E_OpHasAttrNoAttrset *) + exists (S n). rewrite eval_S. csimpl. + destruct n; try discriminate. rewrite eval_S in Heval. + simplify_option_eq. + apply bind_Some. exists v. + split; [apply eval_value; lia|]. + case_match; try done. + exfalso. apply H. by exists bs. + - (* E_Assert *) + exists (S n). rewrite eval_S. csimpl. + apply bind_Some. exists true. + split; [by destruct n | done]. +Qed. + +Lemma eval_step_ctx : ∀ e e' E uf_ext uf_int n v'', + is_ctx uf_ext uf_int E → + e -->base e' → + eval n uf_ext (E e') = Some v'' → + ∃ m, eval m uf_ext (E e) = Some v''. +Proof. + intros e e' E uf_in uf_out n v'' Hctx Hbstep. + revert v''. + induction Hctx. + - intros. by apply eval_base_step with (e' := e') (n := n). + - inv H; intros. + + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + destruct xs. simplify_option_eq. + apply eval_le with (m := S n) in Heqo; try lia. + apply IHHctx in Heqo as [m He]. + exists (S (n `max` m)). + rewrite eval_S. simplify_option_eq. + rewrite eval_le with (n := m) (v' := V_Attrset H1) by lia || done. + simplify_option_eq. + case_match; by rewrite eval_le with (n := n) (v' := v'') by lia || done. + + intros. + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + destruct xs. simplify_option_eq. + apply eval_le with (m := S n) in Heqo; try lia. + apply IHHctx in Heqo as [m He]. + exists (S (n `max` m)). + rewrite eval_S. simplify_option_eq. + setoid_rewrite eval_le with (n := m); try lia || done. + simplify_option_eq. repeat case_match; + apply eval_le with (n := n); lia || done. + + intros. + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + apply eval_le with (m := S n) in Heqo; try lia. + apply IHHctx in Heqo as [m He]. + exists (S (n `max` m)). + rewrite eval_S. simplify_option_eq. + setoid_rewrite eval_le with (n := m); try lia || done. + simplify_option_eq. repeat case_match; + apply eval_le with (n := n); lia || done. + + (* X_Apply *) + intros. + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + apply eval_le with (m := S n) in Heqo; try done || lia. + apply IHHctx in Heqo as [m He]. + exists (S (n `max` m)). + rewrite eval_S. simplify_option_eq. + destruct H0; try discriminate. + * setoid_rewrite eval_le with (n := m); try done || lia. + simplify_option_eq. + setoid_rewrite eval_le with (n := n); done || lia. + * setoid_rewrite eval_le with (n := m); try done || lia. + simplify_option_eq. + rewrite eval_le with (n := n) at 1; try done || lia. + simplify_option_eq. + setoid_rewrite eval_le with (n := n); done || lia. + * setoid_rewrite eval_le with (n := m); try done || lia. + simplify_option_eq. + setoid_rewrite eval_le with (n := n); done || lia. + + intros. + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + destruct n; try discriminate. rewrite eval_S in Heqo. + simplify_option_eq. + apply eval_le with (m := S (S n)) in Heqo; try lia. + apply IHHctx in Heqo as [o He]. + exists (S (S (n `max` o))). + rewrite eval_S. simplify_option_eq. + destruct o as [|o]; try discriminate. + setoid_rewrite eval_le with (n := S o) (v' := V_AttrsetFn m e1); + try done || lia. + simplify_option_eq. + rewrite eval_le with (n := S o) (v' := V_Attrset H1); + try by rewrite eval_S || lia. + simplify_option_eq. + rewrite eval_le with (n := S n) (v' := v''); done || lia. + + intros. + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + apply eval_le with (m := S n) in Heqo. 2: lia. + apply IHHctx in Heqo as [m He]. + exists (S (n `max` m)). + rewrite eval_S. simplify_option_eq. + rewrite eval_le with (n := m) (v' := H1) by lia || done. + setoid_rewrite eval_le with (n := n) (v' := v''); try lia || done. + + intros. + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + apply eval_le with (m := S n) in Heqo. 2: lia. + apply IHHctx in Heqo as [m He]. + exists (S (n `max` m)). + destruct H0; try discriminate. + rewrite eval_S. simplify_option_eq. + setoid_rewrite eval_le with (n := m) (v' := p); try lia || done. + simplify_option_eq. destruct p; try discriminate. + apply eval_le with (n := n); lia || done. + + intros. + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + apply eval_le with (m := S n) in Heqo. 2: lia. + apply IHHctx in Heqo as [m He]. + exists (S (n `max` m)). + rewrite eval_S. simplify_option_eq. + rewrite eval_le with (n := n) (v' := H1) by lia || done. + rewrite eval_le with (n := m) (v' := H0) by lia || done. + simplify_option_eq. + apply eval_le with (n := n); lia || done. + + intros. + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + apply eval_le with (m := S n) in Heqo0. 2: lia. + apply IHHctx in Heqo0 as [m He]. + exists (S (n `max` m)). + rewrite eval_S. simplify_option_eq. + rewrite eval_le with (n := m) (v' := H1) by lia || done. + rewrite eval_le with (n := n) (v' := H0) by lia || done. + simplify_option_eq. + apply eval_le with (n := n) (v' := v''); lia || done. + + (* IsCtxItem_OpHasAttrL *) + intros. + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + apply eval_le with (m := S n) in Heqo. 2: lia. + apply IHHctx in Heqo as [m He]. + exists (S (n `max` m)). + rewrite eval_S. simplify_option_eq. + by rewrite eval_le with (n := m) (v' := H0) by lia || done. + + intros. + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + apply eval_le with (m := S n) in H. 2: lia. + apply IHHctx in H as [m He]. + exists (S (n `max` m)). + rewrite eval_S; simplify_option_eq. + apply eval_le with (n := m) (v' := v''); lia || done. + + intros. simplify_option_eq. + destruct n as [|n]; try discriminate. + rewrite eval_S in H. simplify_option_eq. + apply map_mapM_Some_L in Heqo. + destruct (map_Forall2_destruct _ _ _ _ _ Heqo) + as [v' [m2' [Hkm2' HeqH0]]]. simplify_option_eq. + apply map_Forall2_insert_inv in Heqo as [Hinterp HForall2]; try done. + apply eval_le with (m := S n) in Hinterp; try lia. + apply IHHctx in Hinterp as [m Hinterp]. + exists (S (n `max` m)). + rewrite eval_S. simplify_option_eq. + apply bind_Some. exists (<[x := v']> m2'). split; try done. + apply map_mapM_Some_L. + apply map_Forall2_insert_weak. + * apply eval_le with (n := m); lia || done. + * apply map_Forall2_impl_L + with (R1 := λ x y, eval n true x = Some y); try done. + intros u v Hjuv. by apply eval_le with (n := n); try lia. +Qed. + +Lemma eval_step e e' v'' n : + e --> e' → + eval n false e' = Some v'' → + ∃ m, eval m false e = Some v''. +Proof. + intros. inv H. + apply (eval_step_ctx e1 e2 E false uf_int n v'' H1 H2 H0). +Qed. + +Theorem eval_complete e (v' : value) : + e -->* v' → ∃ n, eval n false e = Some v'. +Proof. + intros [steps Hsteps] % rtc_nsteps. revert e v' Hsteps. + induction steps; intros e e' Hsteps; inv Hsteps. + - exists 1. apply eval_value. lia. + - destruct (IHsteps y e') as [n Hn]; try done. + clear IHsteps. by apply eval_step with (e := e) in Hn. +Qed. diff --git a/correct.v b/correct.v new file mode 100644 index 0000000..89f5894 --- /dev/null +++ b/correct.v @@ -0,0 +1,299 @@ +Require Import Coq.Strings.String. +From stdpp Require Import gmap. +From mininix Require Import + expr relations sem interpreter complete sound shared. + +Theorem correct e v' : (∃ n, eval n false e = Some v') ↔ e -->* v'. +Proof. + split. + - intros [n Heval]. by apply (eval_sound_strong n false). + - intros Heval. by apply eval_complete. +Qed. + +(* Top-level program reduction/evaluation: + we make the prelude available here. *) + +Definition with_prelude (e : expr) : expr := + subst (closed prelude) e. + +Definition tl_reds (e e' : expr) := + with_prelude e -->* e'. + +Definition tl_eval (n : nat) (e : expr) : option value := + eval n false (subst (closed prelude) e). + +Definition tl_evals e e' := ∃ n, tl_eval n e = Some e'. + +(* Macros *) + +Definition μ_neq e1 e2 := X_Cond (X_Op O_Eq e1 e2) false true. +Definition μ_or e1 e2 := X_Cond e1 true e2. +Definition μ_and e1 e2 := X_Cond e1 e2 false. +Definition μ_impl e1 e2 := X_Cond e1 e2 true. +Definition μ_neg e := X_Cond e false true. + +Definition μ_le n m := μ_or (X_Op O_Eq n m) (X_Op O_Lt n m). +Definition μ_gt n m := X_Op O_Lt m n. +Definition μ_ge n m := μ_or (X_Op O_Eq n m) (μ_gt n m). + +(* Tests/examples *) + +Definition ex1 := X_LetBinding {[ "a" := B_Rec 1%Z ]} "a". + +(* [let a = 1; in a] gives 1 *) +Theorem ex1_step : tl_reds ex1 1%Z. +Proof. + unfold ex1. + eapply rtc_l. + - by eapply E_Ctx with (E := id). + - simplify_option_eq. + eapply rtc_once. + by eapply E_Ctx with (E := id). +Qed. + +Example ex1_eval : tl_evals ex1 (V_Int 1). +Proof. by exists 3. Qed. + +(* Definition ex2 := <{ let a = 1 in with { a = 2 }; a }>. *) +Definition ex2 := X_LetBinding {[ "a" := B_Rec 1%Z ]} + (X_Incl (V_Attrset {[ "a" := X_V 2%Z ]}) "a"). + +(* [let a = 1; in with { a = 2; }; a] gives 1 *) +Theorem ex2_step : tl_reds ex2 1%Z. +Proof. + unfold ex2. + eapply rtc_l. + - by eapply E_Ctx with (E := id). + - simplify_option_eq. + eapply rtc_l. + + by eapply E_Ctx with (E := id). + + simpl. eapply rtc_once. + by eapply E_Ctx with (E := id). +Qed. + +Example ex2_eval : tl_evals ex2 (V_Int 1). +Proof. by exists 4. Qed. + +(* [with { a = 1; }; with { a = 2; }; a] gives 2 *) +Definition ex3 := + X_Incl (V_Attrset {[ "a" := X_V 1%Z ]}) + (X_Incl (V_Attrset {[ "a" := X_V 2%Z ]}) "a"). + +Theorem ex3_step : tl_reds ex3 2%Z. +Proof. + unfold ex3. + eapply rtc_l. + - eapply E_Ctx with (E := id); [done | apply E_With]. + - simpl. eapply rtc_l. + + by eapply E_Ctx with (E := id). + + simplify_option_eq. + eapply rtc_once. + by eapply E_Ctx with (E := id). +Qed. + +Example ex3_eval : tl_evals ex3 (V_Int 2). +Proof. by exists 4. Qed. + +(* [({ x, y ? x } : y) { x = 1; }] gives 1 *) +Definition ex4 := + X_Apply + (V_AttrsetFn + (M_Matcher + {[ "x" := M_Mandatory; + "y" := M_Optional "x" + ]} + true) + "y") + (V_Attrset {[ "x" := X_V 1%Z ]}). + +Example ex4_eval : tl_evals ex4 (V_Int 1). +Proof. by exists 7. Qed. + +(* [({ x ? y, y ? x } : y) { x = 1; }] gives 1 *) +Definition ex5 := + X_Apply + (V_AttrsetFn + (M_Matcher + {[ "x" := M_Optional "y"; + "y" := M_Optional "x" + ]} + true) + "y") + (V_Attrset {[ "x" := X_V 1%Z ]}). + +Example ex5_eval : tl_evals ex5 (V_Int 1). +Proof. by exists 7. Qed. + +(* [let binToString = n: + if n == 0 + then "0" + else if n == 1 + then "1" + else binToString (n / 2) + (if isEven n then "0" else "1"); + isEven = n: n != 1 && (n = 0 || isEven (n - 2)); + test = { x, y ? attrs.x, ... } @ attrs: + "x: " + x + ", y: " + y + ", z: " + attrs.z or "(no z)" + in test { x = binToString 6; }] gives "x: 110, y: 110, z: (no z)" *) +Definition ex6 := + X_LetBinding + {[ "binToString" := B_Rec $ V_Fn "n" $ + X_Cond + (X_Op O_Eq "n" 0%Z) + (V_Str "0") + (X_Cond + (X_Op O_Eq "n" 1%Z) + (V_Str "1") + (X_Op O_Plus + (X_Apply + "binToString" + (X_Op O_Div "n" 2%Z)) + (X_Cond + (X_Apply "isEven" "n") + (V_Str "0") + (V_Str "1")))); + "isEven" := B_Rec $ V_Fn "n" $ + μ_and + (μ_neq "n" 1%Z) + (μ_or + (X_Op O_Eq "n" 0%Z) + (X_Apply "isEven" (X_Op O_Min "n" 2%Z))); + "test" := B_Rec $ V_Fn "attrs" $ + X_Apply + (V_AttrsetFn + (M_Matcher + {[ "x" := M_Mandatory; + "y" := M_Optional + (X_Select "attrs" + (nonempty_singleton "x")) + ]} false) + (X_Op O_Plus + (X_Op O_Plus + (X_Op O_Plus + (X_Op O_Plus + (X_Op O_Plus + (V_Str "x: ") + "x") + (V_Str ", y: ")) + "y") + (V_Str ", z: ")) + (X_SelectOr + "attrs" + (nonempty_singleton "z") + (V_Str "(no z)")))) + "attrs" + ]} + (X_Apply "test" $ V_Attrset + {[ "x" := X_Apply "binToString" 6%Z ]}). + +Example ex6_eval : tl_evals ex6 (V_Str "x: 110, y: 110, z: (no z)"). +Proof. by exists 37. Qed. + +(* Important check of if placeholders work correctly: + [with { x = 1; }; let foo = y: let x = 2; in y; foo x] + gives 1 *) +Definition ex7 := X_Incl + (V_Attrset {[ "x" := X_V 1%Z ]}) + (X_LetBinding + {[ "foo" := B_Rec $ V_Fn "y" $ + X_LetBinding {[ "x" := B_Rec 2%Z ]} "y" + ]} + (X_Apply "foo" "x")). + +Example ex7_eval : tl_evals ex7 (V_Int 1). +Proof. by exists 7. Qed. + +Definition ex8 := + X_LetBinding + {[ "divide" := B_Rec $ V_Fn "a" $ V_Fn "b" $ + X_Assert + (μ_and (μ_ge "a" 0%Z) (μ_gt "b" 0%Z)) + (X_Cond + (X_Op O_Lt "a" "b") + 0 + (X_Op + O_Plus + (X_Apply + (X_Apply + "divide" + (X_Op O_Min "a" "b")) + "b") + 1)); + "divider" := B_Rec $ X_Attrset + {[ "__functor" := B_Nonrec $ V_Fn "self" $ V_Fn "x" $ + X_Op + O_Upd + "self" + (X_Attrset + {[ "value" := B_Nonrec $ + X_Apply + (X_Apply + "divide" + (X_Select "self" $ nonempty_singleton "value")) + "x" + ]}) + ]}; + "mkDivider" := B_Rec $ V_Fn "value" $ + X_Op + O_Upd + "divider" + (X_Attrset {[ "value" := B_Nonrec "value" ]}) + ]}%Z + (X_Select + (X_Apply (X_Apply (X_Apply "mkDivider" 100) 5) 4) + (nonempty_singleton "value"))%Z. + +Example ex8_eval : tl_evals ex8 (V_Int 5). +Proof. by exists 170. Qed. + +Example ex9 := + X_Apply + (X_Apply + (V_Attrset + {[ "__functor" := X_V $ V_Fn "self" $ V_Fn "f" $ + X_Apply "f" (X_Apply "self" "f") + ]}) + (V_Fn "go" $ V_Fn "n" $ + X_Cond + (μ_le "n" 1) + "n" + (X_Op + O_Plus + (X_Apply "go" (X_Op O_Min "n" 1)) + (X_Apply "go" (X_Op O_Min "n" 2)))))%Z + 15%Z. + +Example ex9_eval : tl_evals ex9 (V_Int 610). +Proof. by exists 78. Qed. + +Example ex10 := + X_LetBinding + {[ "true" := B_Rec 42 ]}%Z + (X_Op O_Eq "true" 42)%Z. + +Example ex10_eval : tl_evals ex10 (V_Bool true). +Proof. by exists 4. Qed. + +Definition ex11 := + X_LetBinding + {[ "x" := B_Rec "y" ]}%Z + (X_LetBinding {[ "y" := B_Rec 10 ]} "x")%Z. + +Example ex11_eval : tl_eval 1000 ex11 = None. +Proof. done. Qed. + +Definition ex12 := + X_LetBinding + {[ "pkgs" := B_Rec $ V_Attrset + {[ "x" := X_Incl (V_Attrset {[ "y" := X_V 1%Z ]}) "y" ]} + ]} + (X_Select + (X_Attrset + {[ "x" := B_Rec $ X_Select "pkgs" (nonempty_singleton "x"); + "y" := B_Rec 3%Z + ]}) + (nonempty_singleton "x")). + +Example ex12_eval : tl_eval 1000 ex12 = Some (V_Int 1). +Proof. done. Qed. + +(* Aio, quantitas magna frumentorum est. *) diff --git a/expr.v b/expr.v new file mode 100644 index 0000000..11c0737 --- /dev/null +++ b/expr.v @@ -0,0 +1,250 @@ +Require Import Coq.Strings.String. +From stdpp Require Import gmap. + +(* The Nix Expression Language *) + +(** Selected operators from Dolsta and Löh, 2008. Newer definitions at + https://nixos.org/manual/nix/stable/language/operators *) +Variant op : Type := + | O_Eq (* = *) + | O_Lt (* < *) + | O_Plus (* + *) + | O_Min (* - *) + | O_Div (* / *) + | O_Upd. (* // *) + +Hint Constructors op : core. + +Variant nonempty A := Ne_Cons (head : A) (tail : list A). +Arguments Ne_Cons {A} _ _. +Hint Constructors nonempty : core. + +Inductive expr : Type := + | X_V (v : value) (* v *) + | X_Id (x : string) (* x *) + | X_Attrset (bs : gmap string b_rhs) (* { bᵣ* } *) + | X_LetBinding (bs : gmap string b_rhs) (e : expr) (* let bᵣ* in e *) + | X_Select (e : expr) (xs : nonempty string) (* e.xs *) + | X_SelectOr (e : expr) (xs : nonempty string) (or : expr) (* e.xs or e *) + | X_Apply (e1 e2 : expr) (* e1 e2 *) + | X_Cond (e1 e2 e3 : expr) (* if e1 then e2 else e3 *) + | X_Incl (e1 e2 : expr) (* with e1; e2 *) + | X_Assert (e1 e2 : expr) (* assert e1; e2 *) + | X_Op (op : op) (e1 e2 : expr) (* e1 e2 *) + | X_HasAttr (e1 : expr) (x : string) (* e ? x *) + | X_Force (e : expr) (* force e *) + | X_Closed (e : expr) (* closed(e) *) + | X_Placeholder (x : string) (e : expr) (* placeholderₓ(e) *) +with b_rhs := + | B_Rec (e : expr) (* := e *) + | B_Nonrec (e : expr) (* :=ᵣ e *) +with matcher := + | M_Matcher (ms : gmap string m_rhs) (strict : bool) +with m_rhs := + | M_Mandatory + | M_Optional (e : expr) (* ? e *) +with value := + | V_Bool (p : bool) : value (* true | false *) + | V_Null : value (* null *) + | V_Int (n : Z) : value (* n *) + | V_Str (s : string) : value (* s *) + | V_Fn (x : string) (e : expr) : value (* x: e *) + | V_AttrsetFn (m : matcher) (e : expr) : value (* { m }: e *) + | V_Attrset (bs : gmap string expr) : value. (* { b* } *) + +Hint Constructors expr : core. + +Instance Maybe_X_Attrset : Maybe X_Attrset := λ e, + match e with + | X_Attrset bs => Some bs + | _ => None + end. + +Instance Maybe_B_Nonrec : Maybe B_Nonrec := λ rhs, + match rhs with + | B_Nonrec e => Some e + | _ => None + end. + +Instance Maybe_B_Rec : Maybe B_Rec := λ rhs, + match rhs with + | B_Rec e => Some e + | _ => None + end. + +Lemma maybe_b_rhs_excl b : + is_Some (maybe B_Nonrec b) → is_Some (maybe B_Rec b) → False. +Proof. intros [e2 Hnonrec] [e1 Hrec]. simplify_option_eq. Qed. + +Lemma no_b_nonrec__b_rec b : + ¬ is_Some (maybe B_Nonrec b) → is_Some (maybe B_Rec b). +Proof. + destruct b; try by eauto. + simplify_eq/=. intros contra. apply is_Some_alt. eauto. +Qed. + +Lemma no_b_rec__b_nonrec b : + ¬ is_Some (maybe B_Rec b) → is_Some (maybe B_Nonrec b). +Proof. + destruct b; try by eauto. + simplify_eq/=. intros contra. apply is_Some_alt. eauto. +Qed. + +Instance Maybe_V_Attrset : Maybe V_Attrset := λ e, + match e with + | V_Attrset bs => Some bs + | _ => None + end. + +Instance Maybe_V_Bool : Maybe V_Bool := λ e, + match e with + | V_Bool p => Some p + | _ => None + end. + +Global Instance B_Nonrec_inj : Inj (=) (=) B_Nonrec. +Proof. intros [] [] ?; by simplify_eq. Qed. + +Definition matcher_keys (m : matcher) : gset string := + match m with M_Matcher ms _ => dom ms end. + +Definition matcher_map (f : expr → expr) (m : matcher) : matcher := + let map_m_rhs := λ rhs, + match rhs with + | M_Optional e => M_Optional (f e) + | _ => rhs + end in + match m with + | M_Matcher ms strict => M_Matcher (map_m_rhs <$> ms) strict + end. + +Local Definition map_delete_all {K V} `{Countable K} + (ks : gset K) (m : gmap K V) : gmap K V := + set_fold (λ k m', map_delete k m') m ks. + +Local Definition b_rhs_map (f g : expr → expr) (rhs : b_rhs) : b_rhs := + match rhs with + | B_Rec e => B_Rec (f e) + | B_Nonrec e => B_Nonrec (g e) + end. + +(* See Dolstra (2006), §4.3.3 and fig. 4.6 (p. 75, PDF: p. 83) *) +Fixpoint subst (subs : gmap string expr) (e : expr) : expr := + let msubst subs' := b_rhs_map (subst subs') (subst subs) in + match e with + | X_V V_Null | X_V (V_Bool _) | X_V (V_Str _) | X_V (V_Int _) => e + | X_Id x | X_Placeholder x _ => default e (subs !! x) + | X_Attrset bs => + let subs' := map_delete_all (dom bs) subs in + X_Attrset (msubst subs' <$> bs) + | X_V (V_Attrset bs) => + X_V (V_Attrset (subst subs <$> bs)) + | X_LetBinding bs e' => + let subs' := map_delete_all (dom bs) subs in + X_LetBinding (msubst subs' <$> bs) (subst subs' e') + | X_Select e' x => X_Select (subst subs e') x + | X_SelectOr e' x or => X_SelectOr (subst subs e') x (subst subs or) + | X_V (V_Fn x e') => + let subs' := map_delete x subs in + X_V (V_Fn x (subst subs' e')) + | X_V (V_AttrsetFn (M_Matcher ms _ as m) e') => + let subs' := map_delete_all (matcher_keys m) subs in + X_V (V_AttrsetFn (matcher_map (subst subs') m) (subst subs' e')) + | X_Apply e1 e2 => X_Apply (subst subs e1) (subst subs e2) + | X_Cond e1 e2 e3 => X_Cond (subst subs e1) (subst subs e2) (subst subs e3) + | X_Incl e1 e2 => X_Incl (subst subs e1) (subst subs e2) + | X_Op op e1 e2 => X_Op op (subst subs e1) (subst subs e2) + | X_HasAttr e x => X_HasAttr (subst subs e) x + | X_Assert e1 e2 => X_Assert (subst subs e1) (subst subs e2) + | X_Closed e => X_Closed e + | X_Force e => X_Force (subst subs e) + end. + +Definition closed (bs : gmap string expr) : gmap string expr := + X_Closed <$> bs. + +Definition placeholders (bs : gmap string expr) : gmap string expr := + map_imap (λ (x : string) (e : expr), Some (X_Placeholder x e)) bs. + +Definition nonempty_singleton {A} (a : A): nonempty A := Ne_Cons a nil. + +Definition nonempty_cons {A} (a : A) (l : nonempty A) : nonempty A := + match l with Ne_Cons head tail => Ne_Cons a (head :: tail) end. + +Definition indirect (bs : gmap string b_rhs) : gmap string expr := + map_imap (λ (x : string) (rhs : b_rhs), + Some (X_Select (X_Attrset bs) (nonempty_singleton x))) bs. + +Definition rec_subst (bs : gmap string b_rhs) : gmap string expr := + let subs := indirect bs + in (λ b, match b with + | B_Rec e => subst (closed subs) e + | B_Nonrec e => e + end) <$> bs. + +Inductive strong_value : Type := + | SV_Bool (b : bool) + | SV_Null + | SV_Int (n : Z) + | SV_Str (s : string) + | SV_Fn (x : string) (e : expr) + | SV_AttrsetFn (m : matcher) (e : expr) + | SV_Attrset (bs : gmap string strong_value). + +Fixpoint value_from_strong_value (sv : strong_value) : value := + match sv with + | SV_Null => V_Null + | SV_Bool b => V_Bool b + | SV_Int n => V_Int n + | SV_Str s => V_Str s + | SV_Fn x e => V_Fn x e + | SV_AttrsetFn m e => V_AttrsetFn m e + | SV_Attrset bs => V_Attrset (X_V ∘ value_from_strong_value <$> bs) + end. + +Global Instance X_V_inj : Inj (=) (=) X_V. +Proof. intros [] [] ?; by simplify_eq. Qed. + +Definition expr_from_strong_value : strong_value → expr := + X_V ∘ value_from_strong_value. + +(* Based on the fin_maps test from stdpp *) +Fixpoint sv_size (sv : strong_value) : nat := + match sv with + | SV_Null | SV_Bool _ | SV_Int _ | SV_Str _ + | SV_Fn _ _ | SV_AttrsetFn _ _ => 1 + | SV_Attrset bs => S (map_fold (λ _ sv', plus (sv_size sv')) 0 bs) + end. + +(* Based on the fin_maps test from stdpp *) +Lemma strong_value_ind' : + ∀ P : strong_value → Prop, + P SV_Null → + (∀ b : bool, P (SV_Bool b)) → + (∀ n : Z, P (SV_Int n)) → + (∀ s : string, P (SV_Str s)) → + (∀ (x : string) (e : expr), P (SV_Fn x e)) → + (∀ (m : matcher) (e : expr), P (SV_AttrsetFn m e)) → + (∀ bs : gmap string strong_value, + map_Forall (λ i, P) bs → P (SV_Attrset bs)) → + ∀ s : strong_value, P s. +Proof. + intros P PNull PBool PInt PStr PFn PAttrsetFn PAttrset sv. + remember (sv_size sv) as n eqn:Hn. revert sv Hn. + induction (lt_wf n) as [n _ IH]; intros [| | | | | | bs] ->; simpl in *; try done. + apply PAttrset. revert bs IH. + apply (map_fold_ind (λ r bs, (∀ n', n' < S r → _) → map_Forall (λ _, P) bs)). + - intros IH. apply map_Forall_empty. + - intros k sv bs r ? IHbs IHsv. apply map_Forall_insert; [done|]. split. + + eapply IHsv; [|done]; lia. + + eapply IHbs. intros; eapply IHsv; [|done]; lia. +Qed. + +Coercion X_Id : string >-> expr. +Coercion V_Int : Z >-> value. +(* Leaving this out for now: would conflict with X_Id and + therefore cause ambiguity *) +(* Coercion X_StrVal : string >-> expr. *) +Coercion V_Bool : bool >-> value. +Coercion X_V : value >-> expr. +Coercion value_from_strong_value : strong_value >-> value. diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..82ae26f --- /dev/null +++ b/flake.lock @@ -0,0 +1,61 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1719253556, + "narHash": "sha256-A/76RFUVxZ/7Y8+OMVL1Lc8LRhBxZ8ZE2bpMnvZ1VpY=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "fc07dc3bdf2956ddd64f24612ea7fc894933eb2e", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-24.05", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..e9c35a4 --- /dev/null +++ b/flake.nix @@ -0,0 +1,23 @@ +{ + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.05"; + flake-utils.url = "github:numtide/flake-utils"; + }; + + outputs = { self, nixpkgs, flake-utils, ... }: + flake-utils.lib.eachDefaultSystem (system: + let + pkgs = import nixpkgs { inherit system; }; + in + { + devShells.default = with pkgs; mkShell { + buildInputs = [ + coqPackages.coqide + coqPackages.stdpp + coq + ]; + }; + + formatter = pkgs.nixpkgs-fmt; + }); +} diff --git a/interpreter.v b/interpreter.v new file mode 100644 index 0000000..c701b42 --- /dev/null +++ b/interpreter.v @@ -0,0 +1,103 @@ +Require Import Coq.Strings.String. +From stdpp Require Import fin_maps. +From mininix Require Import binop expr maptools matching. + +Open Scope string_scope. + +Definition eval1 (go : bool → expr → option value) + (uf : bool) (d : expr) : option value := + match d with + | X_Id _ => None + | X_Force e => go true e + | X_Closed e => go uf e + | X_Placeholder x e => go uf e + | X_V (V_Attrset bs) => + if uf + then vs' ← map_mapM (go true) bs; + Some (V_Attrset (X_V <$> vs')) + else Some (V_Attrset bs) + | X_V v => Some v + | X_Attrset bs => go uf (V_Attrset (rec_subst bs)) + | X_LetBinding bs e => + let e' := subst (closed (rec_subst bs)) e + in go uf e' + | X_Select e (Ne_Cons x ys) => + v' ← go false e; + bs ← maybe V_Attrset v'; + e'' ← bs !! x; + match ys with + | [] => go uf e'' + | y :: ys => go uf (X_Select e'' (Ne_Cons y ys)) + end + | X_SelectOr e (Ne_Cons x ys) or => + v' ← go false e; + bs ← maybe V_Attrset v'; + match bs !! x with + | Some e'' => + match ys with + | [] => go uf e'' + | y :: ys => go uf (X_SelectOr e'' (Ne_Cons y ys) or) + end + | None => go uf or + end + | X_Apply e1 e2 => + v1' ← go false e1; + match v1' with + | V_Fn x e => + let e' := subst {[x := X_Closed e2]} e + in go uf e' + | V_AttrsetFn m e => + v2' ← go false e2; + bs ← maybe V_Attrset v2'; + bs' ← matches m bs; + go uf (X_LetBinding bs' e) + | V_Attrset bs => + f ← bs !! "__functor"; + go uf (X_Apply (X_Apply f (V_Attrset bs)) e2) + | _ => None + end + | X_Cond e1 e2 e3 => + v1' ← go false e1; + b ← maybe V_Bool v1'; + go uf (if b : bool then e2 else e3) + | X_Incl e1 e2 => + v1' ← go false e1; + match v1' with + | V_Attrset bs => go uf (subst (placeholders bs) e2) + | _ => go uf e2 + end + | X_Op op e1 e2 => + e1' ← go false e1; + e2' ← go false e2; + v' ← binop_eval op e1' e2'; + go uf (X_V v') + | X_HasAttr e x => + v' ← go false e; + Some $ V_Bool $ + match v' with + | V_Attrset bs => + bool_decide (is_Some (bs !! x)) + | _ => false + end + | X_Assert e1 e2 => + v1' ← go false e1; + match v1' with + | V_Bool true => go uf e2 + | _ => None + end + end. + +Fixpoint eval (n : nat) (uf : bool) (e : expr) : option value := + match n with + | O => None + | S n => eval1 (eval n) uf e + end. + +(* Don't automatically 'simplify' eval: this can lead to very complicated + assumptions and goals. Instead, we define our own lemma which can be used + to unfold eval once. This allows us to write proofs in a much more + controlled manner, and we can still leverage tactics like simplify_option_eq + without everything blowing up uncontrollably *) +Global Opaque eval. +Lemma eval_S n : eval (S n) = eval1 (eval n). +Proof. done. Qed. diff --git a/maptools.v b/maptools.v new file mode 100644 index 0000000..2478430 --- /dev/null +++ b/maptools.v @@ -0,0 +1,476 @@ +Require Import Coq.Strings.String. +From stdpp Require Import countable fin_maps fin_map_dom. + +(** Generic lemmas for finite maps and their domains *) + +Lemma map_insert_empty_lookup {A} `{FinMap K M} + (i j : K) (u v : A) : + <[i := u]> (∅ : M A) !! j = Some v → i = j ∧ v = u. +Proof. + intros Hiel. + destruct (decide (i = j)). + - split; try done. simplify_eq /=. + rewrite lookup_insert in Hiel. congruence. + - rewrite lookup_insert_ne in Hiel; try done. + exfalso. eapply lookup_empty_Some, Hiel. +Qed. + +Lemma map_insert_ne_inv `{FinMap K M} {A} + (m1 m2 : M A) i j x y : + i ≠ j → + <[i := x]>m1 = <[j := y]>m2 → + m2 !! i = Some x ∧ m1 !! j = Some y ∧ + delete i (delete j m1) = delete i (delete j m2). +Proof. + intros Hneq Heq. + split; try split. + - rewrite <-lookup_delete_ne with (i := j) by congruence. + rewrite <-delete_insert_delete with (x := y). + rewrite <-Heq. + rewrite lookup_delete_ne by congruence. + by rewrite lookup_insert. + - rewrite <-lookup_delete_ne with (i := i) by congruence. + rewrite <-delete_insert_delete with (x := x). + rewrite Heq. + rewrite lookup_delete_ne by congruence. + by rewrite lookup_insert. + - setoid_rewrite <-delete_insert_delete with (x := x) at 1. + setoid_rewrite <-delete_insert_delete with (x := y) at 4. + rewrite <-delete_insert_ne by congruence. + by do 2 f_equal. +Qed. + +Lemma map_insert_inv `{FinMap K M} {A} + (m1 m2 : M A) i x y : + <[i := x]>m1 = <[i := y]>m2 → + x = y ∧ delete i m1 = delete i m2. +Proof. + intros Heq. + split; try split. + - apply Some_inj. + replace (Some x) with (<[i := x]>m1 !! i) by apply lookup_insert. + replace (Some y) with (<[i := y]>m2 !! i) by apply lookup_insert. + by rewrite Heq. + - replace (delete i m1) with (delete i (<[i := x]>m1)) + by apply delete_insert_delete. + replace (delete i m2) with (delete i (<[i := y]>m2)) + by apply delete_insert_delete. + by rewrite Heq. +Qed. + +Lemma fmap_insert_lookup `{FinMap K M} {A B} + (f : A → B) (m1 : M A) (m2 : M B) i x : + f <$> m1 = <[i := x]>m2 → + f <$> m1 !! i = Some x. +Proof. + intros Hmap. + rewrite <-lookup_fmap. + rewrite Hmap. + apply lookup_insert. +Qed. + +Lemma map_dom_delete_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (m1 : M A) (m2 : M B) i x y : + dom (delete i m1) = dom (delete i m2) → + dom (<[i := x]>m1) = dom (<[i := y]> m2). +Proof. + intros Hdel. + setoid_rewrite <-insert_delete_insert at 1 2. + rewrite 2 dom_insert_L. + set_solver. +Qed. + +Lemma map_dom_delete_insert_subseteq_L `{FinMapDom K M D} `{!LeibnizEquiv D} + {A B} (m1 : M A) (m2 : M B) i x y : + dom (delete i m1) ⊆ dom (delete i m2) → + dom (<[i := x]>m1) ⊆ dom (<[i := y]> m2). +Proof. + intros Hdel. + setoid_rewrite <-insert_delete_insert at 1 2. + rewrite 2 dom_insert_L. + set_solver. +Qed. + +Lemma map_dom_empty_eq_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} + (m : M A) : dom (∅ : M A) = dom m → m = ∅. +Proof. + intros Hdom. + rewrite dom_empty_L in Hdom. + symmetry in Hdom. + by apply dom_empty_inv_L. +Qed. + +Lemma map_dom_insert_eq_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} + (i : K) (x : A) (m1 m2 : M A) : + dom (<[i := x]>m1) = dom m2 → + dom (delete i m1) = dom (delete i m2) ∧ i ∈ dom m2. +Proof. set_solver. Qed. + +(** map_mapM *) + +Definition map_mapM {M : Type → Type} `{MBind F} `{MRet F} `{FinMap K M} {A B} + (f : A → F B) (m : M A) : F (M B) := + map_fold (λ i x om', m' ← om'; x' ← f x; mret $ <[i := x']>m') (mret ∅) m. + +Lemma map_mapM_dom_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (f : A → option B) (m1 : M A) (m2 : M B) : + map_mapM f m1 = Some m2 → dom m1 = dom m2. +Proof. + revert m2. + induction m1 using map_ind; intros m2 HmapM. + - unfold map_mapM in HmapM. rewrite map_fold_empty in HmapM. + simplify_option_eq. + by rewrite 2 dom_empty_L. + - unfold map_mapM in HmapM. + rewrite map_fold_insert_L in HmapM. + + simplify_option_eq. + apply IHm1 in Heqo. + rewrite 2 dom_insert_L. + by f_equal. + + intros. + destruct y; simplify_option_eq; try done. + destruct (f z2); simplify_option_eq. + * destruct (f z1); simplify_option_eq; try done. + f_equal. by apply insert_commute. + * destruct (f z1); by simplify_option_eq. + + done. +Qed. + +Lemma map_mapM_option_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (f : A → option B) (m1 : M A) (m2 m2' : M B) + (i : K) (x : A) (x' : B) : + m1 !! i = None → + map_mapM f (<[i := x]>m1) = Some m2 → + ∃ x', f x = Some x' ∧ map_mapM f m1 = Some (delete i m2). +Proof. + intros Helem HmapM. + unfold map_mapM in HmapM. + rewrite map_fold_insert_L in HmapM. + - simplify_option_eq. + exists H15. + split; try done. + rewrite delete_insert. + apply Heqo. + apply map_mapM_dom_L in Heqo. + apply not_elem_of_dom in Helem. + apply not_elem_of_dom. + set_solver. + - intros. + destruct y; simplify_option_eq; try done. + destruct (f z2); simplify_option_eq. + + destruct (f z1); simplify_option_eq; try done. + f_equal. by apply insert_commute. + + destruct (f z1); by simplify_option_eq. + - done. +Qed. + +(** map_Forall2 *) + +Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B} + (R : A → B → Prop) := + map_relation (M := M) R (λ _, False) (λ _, False). + +Global Instance map_Forall2_dec `{FinMap K M} {A B} (R : A → B → Prop) + `{∀ a b, Decision (R a b)} : RelDecision (map_Forall2 (M := M) R). +Proof. apply map_relation_dec; intros; try done; apply False_dec. Qed. + +Lemma map_Forall2_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (m1 : M A) (m2 : M B) R i x y : + m1 !! i = None → + m2 !! i = None → + R x y → + map_Forall2 R m1 m2 → + map_Forall2 R (<[i := x]>m1) (<[i := y]>m2). +Proof. + unfold map_Forall2, map_relation, option_relation. + intros Him1 Him2 HR HForall2 j. + destruct (decide (i = j)). + + simplify_option_eq. by rewrite 2 lookup_insert. + + rewrite 2 lookup_insert_ne by done. apply HForall2. +Qed. + +Lemma map_Forall2_insert_weak `{FinMap K M} {A B} + (m1 : M A) (m2 : M B) R i x y : + R x y → + map_Forall2 R (delete i m1) (delete i m2) → + map_Forall2 R (<[i := x]>m1) (<[i := y]>m2). +Proof. + unfold map_Forall2, map_relation, option_relation. + intros HR HForall2 j. + destruct (decide (i = j)). + - simplify_option_eq. by rewrite 2 lookup_insert. + - rewrite 2 lookup_insert_ne by done. + rewrite <-lookup_delete_ne with (i := i) by done. + replace (m2 !! j) with (delete i m2 !! j); try by apply lookup_delete_ne. + apply HForall2. +Qed. + +Lemma map_Forall2_destruct `{FinMap K M} {A B} + (m1 : M A) (m2 : M B) R i x : + map_Forall2 R (<[i := x]>m1) m2 → + ∃ y m2', m2' !! i = None ∧ m2 = <[i := y]>m2'. +Proof. + intros HForall2. + unfold map_Forall2, map_relation, option_relation in HForall2. + pose proof (HForall2 i). clear HForall2. + case_match. + - case_match; try done. + exists b, (delete i m2). + split. + * apply lookup_delete. + * by rewrite insert_delete_insert, insert_id. + - case_match; try done. + by rewrite lookup_insert in H8. +Qed. + +Lemma map_Forall2_insert_inv `{FinMap K M} {A B} + (m1 : M A) (m2 : M B) R i x y : + map_Forall2 R (<[i := x]>m1) (<[i := y]>m2) → + R x y ∧ map_Forall2 R (delete i m1) (delete i m2). +Proof. + intros HForall2. + unfold map_Forall2, map_relation, option_relation in HForall2. + pose proof (HForall2 i). + case_match. + - case_match; try done. + rewrite lookup_insert in H8. rewrite lookup_insert in H9. + simplify_eq /=. split; try done. + unfold map_Forall2, map_relation, option_relation. + intros j. + destruct (decide (i = j)). + + simplify_option_eq. + case_match. + * by rewrite lookup_delete in H8. + * case_match; [|done]. + by rewrite lookup_delete in H9. + + case_match; case_match; + rewrite lookup_delete_ne in H8 by done; + rewrite lookup_delete_ne in H9 by done; + pose proof (HForall2 j); + case_match; case_match; try done; + rewrite lookup_insert_ne in H11 by done; + rewrite lookup_insert_ne in H12 by done; + by simplify_eq /=. + - by rewrite lookup_insert in H8. +Qed. + +Lemma map_Forall2_insert_inv_strict `{FinMap K M} {A B} + (m1 : M A) (m2 : M B) R i x y : + m1 !! i = None → + m2 !! i = None → + map_Forall2 R (<[i := x]>m1) (<[i := y]>m2) → + R x y ∧ map_Forall2 R m1 m2. +Proof. + intros Him1 Him2 HForall2. + apply map_Forall2_insert_inv in HForall2 as [HPixy HForall2]. + split; try done. + apply delete_notin in Him1, Him2. + by rewrite Him1, Him2 in HForall2. +Qed. + +Lemma map_Forall2_dom_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (R : A → B → Prop) (m1 : M A) (m2 : M B) : + map_Forall2 R m1 m2 → dom m1 = dom m2. +Proof. + revert m2. + induction m1 using map_ind; intros m2. + - intros HForall2. + destruct m2 using map_ind; [set_solver|]. + unfold map_Forall2, map_relation, option_relation in HForall2. + pose proof (HForall2 i). by rewrite lookup_empty, lookup_insert in H15. + - intros HForall2. + apply map_Forall2_destruct in HForall2 as Hm2. + destruct Hm2 as [y [m2' [Hm21 Hm22]]]. simplify_eq /=. + apply map_Forall2_insert_inv_strict in HForall2 as [_ HForall2]; try done. + set_solver. +Qed. + +Lemma map_Forall2_empty_l_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (R : A → B → Prop) (m2 : M B) : + map_Forall2 R ∅ m2 → m2 = ∅. +Proof. + intros HForall2. + apply map_Forall2_dom_L in HForall2 as Hdom. + rewrite dom_empty_L in Hdom. + symmetry in Hdom. + by apply dom_empty_inv_L in Hdom. +Qed. + +Lemma map_Forall2_empty_r_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (R : A → B → Prop) (m1 : M A) : + map_Forall2 R m1 ∅ → m1 = ∅. +Proof. + intros HForall2. + apply map_Forall2_dom_L in HForall2 as Hdom. + rewrite dom_empty_L in Hdom. + by apply dom_empty_inv_L in Hdom. +Qed. + +Lemma map_Forall2_empty `{FinMap K M} {A B} (R : A → B → Prop): + map_Forall2 R (∅ : M A) (∅ : M B). +Proof. + unfold map_Forall2, map_relation. + intros i. by rewrite 2 lookup_empty. +Qed. + +Lemma map_Forall2_impl_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (R1 R2 : A → B → Prop) : + (∀ a b, R1 a b → R2 a b) → + ∀ (m1 : M A) (m2 : M B), + map_Forall2 R1 m1 m2 → map_Forall2 R2 m1 m2. +Proof. + intros HR1R2 ?? HForall2. + unfold map_Forall2, map_relation, option_relation in *. + intros j. pose proof (HForall2 j). clear HForall2. + case_match; case_match; try done. + by apply HR1R2. +Qed. + +Lemma map_Forall2_fmap_r_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B C} + (P : A → C → Prop) (m1 : M A) (m2 : M B) (f : B → C) : + map_Forall2 P m1 (f <$> m2) → map_Forall2 (λ l r, P l (f r)) m1 m2. +Proof. + intros HForall2. + unfold map_Forall2, map_relation, option_relation in *. + intros j. pose proof (HForall2 j). clear HForall2. + case_match; case_match; try done; case_match; + rewrite lookup_fmap in H16; rewrite H17 in H16; by simplify_eq/=. +Qed. + +Lemma map_Forall2_eq_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} + (m1 m2 : M A) : + m1 = m2 ↔ map_Forall2 (=) m1 m2. +Proof. + split; revert m2. + - induction m1 using map_ind; intros m2 Heq; inv Heq. + + apply map_Forall2_empty. + + apply map_Forall2_insert_L; try done. by apply IHm1. + - induction m1 using map_ind; intros m2 HForall2. + + by apply map_Forall2_empty_l_L in HForall2. + + apply map_Forall2_destruct in HForall2 as Hm. + destruct Hm as [y [m2' [Him2' Heqm2]]]. subst. + apply map_Forall2_insert_inv in HForall2 as [Heqxy HForall2]. + rewrite 2 delete_notin in HForall2 by done. + apply IHm1 in HForall2. by subst. +Qed. + +Lemma map_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} + (i : K) (x1 x2 : A) (m1 m2 : M A) : + x1 = x2 → + delete i m1 = delete i m2 → + <[i := x1]>m1 = <[i := x2]>m2. +Proof. + intros Heq Hdel. + apply map_Forall2_eq_L. + eapply map_Forall2_insert_weak; [done|]. + by apply map_Forall2_eq_L. +Qed. + +Lemma map_insert_rev_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} + (i : K) (x1 x2 : A) (m1 m2 : M A) : + <[i := x1]>m1 = <[i := x2]>m2 → x1 = x2 ∧ delete i m1 = delete i m2. +Proof. + intros Heq. apply map_Forall2_eq_L in Heq. + apply map_Forall2_insert_inv in Heq as [Heq1 Heq2]. + by apply map_Forall2_eq_L in Heq2. +Qed. + +Lemma map_insert_rev_1_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} + (i : K) (x1 x2 : A) (m1 m2 : M A) : + <[i := x1]>m1 = <[i := x2]>m2 → x1 = x2. +Proof. apply map_insert_rev_L. Qed. + +Lemma map_insert_rev_2_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} + (i : K) (x1 x2 : A) (m1 m2 : M A) : + <[i := x1]>m1 = <[i := x2]>m2 → delete i m1 = delete i m2. +Proof. apply map_insert_rev_L. Qed. + +Lemma map_Forall2_alt_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (R : A → B → Prop) (m1 : M A) (m2 : M B) : + map_Forall2 R m1 m2 ↔ + dom m1 = dom m2 ∧ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → R x y. +Proof. + split. + - intros HForall2. + split. + + by apply map_Forall2_dom_L in HForall2. + + intros i x y Him1 Him2. + unfold map_Forall2, map_relation, option_relation in HForall2. + pose proof (HForall2 i). clear HForall2. + by simplify_option_eq. + - intros [Hdom HForall2]. + unfold map_Forall2, map_relation, option_relation. + intros j. + case_match; case_match; try done. + + by eapply HForall2. + + apply mk_is_Some in H14. + apply not_elem_of_dom in H15. + apply elem_of_dom in H14. + set_solver. + + apply not_elem_of_dom in H14. + apply mk_is_Some in H15. + apply elem_of_dom in H15. + set_solver. +Qed. + +(** Relation between map_mapM and map_Forall2 *) + +Lemma map_mapM_Some_1_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (f : A → option B) (m1 : M A) (m2 : M B) : + map_mapM f m1 = Some m2 → map_Forall2 (λ x y, f x = Some y) m1 m2. +Proof. + revert m1 m2 f. + induction m1 using map_ind. + - intros m2 f Hmap_mapM. + unfold map_mapM in Hmap_mapM. + rewrite map_fold_empty in Hmap_mapM. + simplify_option_eq. apply map_Forall2_empty. + - intros m2 f Hmap_mapM. + csimpl in Hmap_mapM. + unfold map_mapM in Hmap_mapM. + csimpl in Hmap_mapM. + rewrite map_fold_insert_L in Hmap_mapM. + + simplify_option_eq. + apply IHm1 in Heqo. + apply map_Forall2_insert_L; try done. + apply not_elem_of_dom in H14. + apply not_elem_of_dom. + apply map_Forall2_dom_L in Heqo. + set_solver. + + intros. + destruct y; simplify_option_eq; try done. + destruct (f z2); simplify_option_eq. + * destruct (f z1); simplify_option_eq; try done. + f_equal. by apply insert_commute. + * destruct (f z1); by simplify_option_eq. + + done. +Qed. + +Lemma map_mapM_Some_2_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (f : A → option B) (m1 : M A) (m2 : M B) : + map_Forall2 (λ x y, f x = Some y) m1 m2 → map_mapM f m1 = Some m2. +Proof. + revert m2. + induction m1 using map_ind; intros m2 HForall2. + - unfold map_mapM. rewrite map_fold_empty. + apply map_Forall2_empty_l_L in HForall2. + by simplify_eq. + - destruct (map_Forall2_destruct _ _ _ _ _ HForall2) as + [y [m2' [HForall21 HForall22]]]. subst. + destruct (map_Forall2_insert_inv_strict _ _ _ _ _ _ H14 HForall21 HForall2) as + [Hfy HForall22]. + apply IHm1 in HForall22. + unfold map_mapM. + rewrite map_fold_insert_L; try by simplify_option_eq. + intros. + destruct y0; simplify_option_eq; try done. + destruct (f z2); simplify_option_eq. + * destruct (f z1); simplify_option_eq; try done. + f_equal. by apply insert_commute. + * destruct (f z1); by simplify_option_eq. +Qed. + +Lemma map_mapM_Some_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} + (f : A → option B) (m1 : M A) (m2 : M B) : + map_mapM f m1 = Some m2 ↔ map_Forall2 (λ x y, f x = Some y) m1 m2. +Proof. split; [apply map_mapM_Some_1_L | apply map_mapM_Some_2_L]. Qed. diff --git a/matching.v b/matching.v new file mode 100644 index 0000000..494bb92 --- /dev/null +++ b/matching.v @@ -0,0 +1,609 @@ +Require Import Coq.Strings.Ascii. +Require Import Coq.Strings.String. +Require Import Coq.NArith.BinNat. +From stdpp Require Import fin_sets gmap option. +From mininix Require Import expr maptools. + +Open Scope string_scope. +Open Scope N_scope. +Open Scope Z_scope. +Open Scope nat_scope. + +Reserved Notation "bs '~' m '~>' brs" (at level 55). + +Inductive matches_r : gmap string expr → matcher → gmap string b_rhs -> Prop := + | E_MatchEmpty strict : ∅ ~ M_Matcher ∅ strict ~> ∅ + | E_MatchAny bs : bs ~ M_Matcher ∅ false ~> ∅ + | E_MatchMandatory bs x e m bs' strict : + bs !! x = None → + m !! x = None → + delete x bs ~ M_Matcher m strict ~> bs' → + <[x := e]>bs ~ M_Matcher (<[x := M_Mandatory]>m) strict + ~> <[x := B_Nonrec e]>bs' + | E_MatchOptAvail bs x d e m bs' strict : + bs !! x = None → + m !! x = None → + delete x bs ~ M_Matcher m strict ~> bs' → + <[x := d]>bs ~ M_Matcher (<[x := M_Optional e]>m) strict + ~> <[x := B_Nonrec d]>bs' + | E_MatchOptDefault bs x e m bs' strict : + bs !! x = None → + m !! x = None → + bs ~ M_Matcher m strict ~> bs' → + bs ~ M_Matcher (<[x := M_Optional e]>m) strict ~> <[x := B_Rec e]>bs' +where "bs ~ m ~> brs" := (matches_r bs m brs). + +Definition map_foldM `{Countable K} `{FinMap K M} `{MBind F} `{MRet F} {A B} + (f : K → A → B → F B) (init : B) (m : M A) : F B := + map_fold (λ i x acc, acc ≫= f i x) (mret init) m. + +Definition matches_aux_f (x : string) (rhs : m_rhs) + (acc : option (gmap string expr * gmap string b_rhs)) := + acc ← acc; + let (bs, brs) := (acc : gmap string expr * gmap string b_rhs) in + match rhs with + | M_Mandatory => + e ← bs !! x; + Some (bs, <[x := B_Nonrec e]>brs) + | M_Optional e => + match bs !! x with + | Some e' => Some (bs, <[x := B_Nonrec e']>brs) + | None => Some (bs, <[x := B_Rec e]>brs) + end + end. + +Definition matches_aux (ms : gmap string m_rhs) (bs : gmap string expr) : + option (gmap string expr * gmap string b_rhs) := + map_fold matches_aux_f (Some (bs, ∅)) ms. + +Definition matches (m : matcher) (bs : gmap string expr) : + option (gmap string b_rhs) := + match m with + | M_Matcher ms strict => + guard (strict → dom bs ⊆ matcher_keys m);; + snd <$> matches_aux ms bs + end. + +(* Copied from stdpp and changed so that the value types + of m1 and m2 are decoupled *) +Lemma dom_subseteq_size' `{FinMapDom K M D} {A B} (m1 : M A) (m2 : M B) : + dom m2 ⊆ dom m1 → size m2 ≤ size m1. +Proof. + revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hdom. + { rewrite map_size_empty. lia. } + rewrite dom_insert in Hdom. + assert (i ∉ dom m2) by (by apply not_elem_of_dom). + assert (i ∈ dom m1) as [x' Hx']%elem_of_dom by set_solver. + rewrite <-(insert_delete m1 i x') by done. + rewrite !map_size_insert_None, <-Nat.succ_le_mono + by (by rewrite ?lookup_delete). + apply IH. rewrite dom_delete. set_solver. +Qed. + +Lemma dom_empty_subset `{Countable K} `{FinMapDom K M D} {A B} (m : M A) : + dom m ⊆ dom (∅ : M B) → m = ∅. +Proof. + intros Hdom. + apply dom_subseteq_size' in Hdom. + rewrite map_size_empty in Hdom. + inv Hdom. + by apply map_size_empty_inv. +Qed. + +Lemma matches_aux_empty bs : matches_aux ∅ bs = Some (bs, ∅). +Proof. done. Qed. + +Lemma matches_aux_f_comm (x : string) (rhs : m_rhs) (m : gmap string m_rhs) + (y z : string) (rhs1 rhs2 : m_rhs) + (acc : option (gmap string expr * gmap string b_rhs)) : + m !! x = None → y ≠ z → + <[x:=rhs]> m !! y = Some rhs1 → + <[x:=rhs]> m !! z = Some rhs2 → + matches_aux_f y rhs1 (matches_aux_f z rhs2 acc) = + matches_aux_f z rhs2 (matches_aux_f y rhs1 acc). +Proof. + intros Hxm Hyz Hym Hzm. + unfold matches_aux_f. + destruct acc. + repeat (simplify_option_eq || done || + destruct (g !! y) eqn:Egy || destruct (g !! z) eqn:Egz || + case_match || rewrite insert_commute). done. +Qed. + +Lemma matches_aux_insert m bs x rhs : + m !! x = None → + matches_aux (<[x := rhs]>m) bs = matches_aux_f x rhs (matches_aux m bs). +Proof. + intros Hnotin. unfold matches_aux. + rewrite map_fold_insert_L; try done. + clear bs. + intros y z rhs1 rhs2 acc Hyz Hym Hzm. + by eapply matches_aux_f_comm. +Qed. + +Lemma matches_aux_bs m bs bs' brs : + matches_aux m bs = Some (bs', brs) → bs = bs'. +Proof. + revert bs bs' brs. + induction m using map_ind; intros bs bs' brs Hmatches. + - rewrite matches_aux_empty in Hmatches. congruence. + - rewrite matches_aux_insert in Hmatches; try done. + unfold matches_aux_f in Hmatches. + simplify_option_eq. + destruct H0. + case_match; try case_match; + simplify_option_eq; by apply IHm with (brs := g0). +Qed. + +Lemma matches_aux_impl m bs brs x e : + m !! x = None → + bs !! x = None → + matches_aux m (<[x := e]>bs) = Some (<[x := e]>bs, brs) → + matches_aux m bs = Some (bs, brs). +Proof. + intros Hxm Hxbs Hmatches. + revert bs brs Hxm Hxbs Hmatches. + induction m using map_ind; intros bs brs Hxm Hxbs Hmatches. + - rewrite matches_aux_empty. + rewrite matches_aux_empty in Hmatches. + by simplify_option_eq. + - rewrite matches_aux_insert in Hmatches by done. + rewrite matches_aux_insert by done. + apply lookup_insert_None in Hxm as [Hxm1 Hxm2]. + unfold matches_aux_f in Hmatches. simplify_option_eq. + destruct H0. case_match. + + simplify_option_eq. + rewrite lookup_insert_ne in Heqo0 by done. + pose proof (IHm bs g0 Hxm1 Hxbs Heqo). + rewrite H1. by simplify_option_eq. + + case_match; simplify_option_eq; + rewrite lookup_insert_ne in H1 by done; + pose proof (IHm bs g0 Hxm1 Hxbs Heqo); + rewrite H0; by simplify_option_eq. +Qed. + +Lemma matches_aux_impl_2 m bs brs x e : + m !! x = None → + bs !! x = None → + matches_aux m bs = Some (bs, brs) → + matches_aux m (<[x := e]>bs) = Some (<[x := e]>bs, brs). +Proof. + intros Hxm Hxbs Hmatches. + revert bs brs Hxm Hxbs Hmatches. + induction m using map_ind; intros bs brs Hxm Hxbs Hmatches. + - rewrite matches_aux_empty. + rewrite matches_aux_empty in Hmatches. + by simplify_option_eq. + - rewrite matches_aux_insert in Hmatches by done. + rewrite matches_aux_insert by done. + apply lookup_insert_None in Hxm as [Hxm1 Hxm2]. + unfold matches_aux_f in Hmatches. simplify_option_eq. + destruct H0. case_match. + + simplify_option_eq. + rewrite <-lookup_insert_ne with (i := x) (x := e) in Heqo0 by done. + pose proof (IHm bs g0 Hxm1 Hxbs Heqo). + rewrite H1. by simplify_option_eq. + + case_match; simplify_option_eq; + rewrite <-lookup_insert_ne with (i := x) (x := e) in H1 by done; + pose proof (IHm bs g0 Hxm1 Hxbs Heqo); + rewrite H0; by simplify_option_eq. +Qed. + +Lemma matches_aux_dom m bs brs : + matches_aux m bs = Some (bs, brs) → dom m = dom brs. +Proof. + revert bs brs. + induction m using map_ind; intros bs brs Hmatches. + - rewrite matches_aux_empty in Hmatches. by simplify_eq. + - rewrite matches_aux_insert in Hmatches by done. + unfold matches_aux_f in Hmatches. simplify_option_eq. destruct H0. + case_match; try case_match; + simplify_option_eq; apply IHm in Heqo; set_solver. +Qed. + +Lemma matches_aux_inv m bs brs x e : + m !! x = None → bs !! x = None → brs !! x = None → + matches_aux (<[x := M_Mandatory]>m) (<[x := e]>bs) = + Some (<[x := e]>bs, <[x := B_Nonrec e]>brs) → + matches_aux m bs = Some (bs, brs). +Proof. + intros Hxm Hxbs Hxbrs Hmatches. + rewrite matches_aux_insert in Hmatches by done. + unfold matches_aux_f in Hmatches. simplify_option_eq. + destruct H. simplify_option_eq. + rewrite lookup_insert in Heqo0. simplify_option_eq. + apply matches_aux_impl in Heqo; try done. + simplify_option_eq. + apply matches_aux_dom in Heqo as Hdom. + rewrite Heqo. do 2 f_equal. + assert (g0 !! x = None). + { apply not_elem_of_dom in Hxm. + rewrite Hdom in Hxm. + by apply not_elem_of_dom. } + replace g0 with (delete x (<[x:=B_Nonrec H]> g0)); + try by rewrite delete_insert. + replace brs with (delete x (<[x:=B_Nonrec H]> brs)); + try by rewrite delete_insert. + by rewrite H1. +Qed. + +Lemma disjoint_union_subseteq_l `{FinSet A C} `{!LeibnizEquiv C} (X Y Z : C) : + X ## Y → X ## Z → X ∪ Y ⊆ X ∪ Z → Y ⊆ Z. +Proof. + revert Y Z. + induction X using set_ind_L; intros Y Z Hdisj1 Hdisj2 Hsubs. + - by do 2 rewrite union_empty_l_L in Hsubs. + - do 2 rewrite <-union_assoc_L in Hsubs. + apply IHX; set_solver. +Qed. + +Lemma singleton_notin_union_disjoint `{FinMapDom K M D} {A} (m : M A) (i : K) : + m !! i = None → + {[i]} ## dom m. +Proof. + intros Hlookup. apply disjoint_singleton_l. + by apply not_elem_of_dom in Hlookup. +Qed. + +Lemma matches_step bs brs m strict x : + matches (M_Matcher (<[x := M_Mandatory]>m) strict) bs = Some brs → + ∃ e, bs !! x = Some e ∧ brs !! x = Some (B_Nonrec e). +Proof. + intros Hmatches. + destruct (decide (is_Some (bs !! x))). + - destruct i. exists x0. split; [done|]. + unfold matches in Hmatches. + destruct strict; simplify_option_eq. + + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m)) + in Heqo0; try by rewrite insert_delete_insert. + rewrite matches_aux_insert in Heqo0 by apply lookup_delete. + unfold matches_aux_f in Heqo0. simplify_option_eq. + destruct H3. simplify_option_eq. + apply matches_aux_bs in Heqo as Hdom. simplify_option_eq. + apply lookup_insert. + + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m)) + in Heqo; try by rewrite insert_delete_insert. + rewrite matches_aux_insert in Heqo by apply lookup_delete. + unfold matches_aux_f in Heqo. simplify_option_eq. + destruct H1. simplify_option_eq. + apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq. + apply lookup_insert. + - unfold matches in Hmatches. + destruct strict; simplify_option_eq. + + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m)) + in Heqo0; try by rewrite insert_delete_insert. + rewrite matches_aux_insert in Heqo0 by apply lookup_delete. + unfold matches_aux_f in Heqo0. simplify_option_eq. + destruct H2. simplify_option_eq. + apply matches_aux_bs in Heqo as Hdom. simplify_option_eq. + rewrite Heqo1 in n. + exfalso. by apply n. + + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m)) + in Heqo; try by rewrite insert_delete_insert. + rewrite matches_aux_insert in Heqo by apply lookup_delete. + unfold matches_aux_f in Heqo. simplify_option_eq. + destruct H0. simplify_option_eq. + apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq. + rewrite Heqo1 in n. + exfalso. by apply n. +Qed. + +Lemma matches_step' bs brs m strict x : + matches (M_Matcher (<[x := M_Mandatory]>m) strict) bs = Some brs → + ∃ e bs' brs', + bs' !! x = None ∧ bs = <[x := e]>bs' ∧ + brs' !! x = None ∧ brs = <[x := B_Nonrec e]>brs'. +Proof. + intros Hmatches. + apply matches_step in Hmatches as He. + destruct He as [e [He1 He2]]. + exists e, (delete x bs), (delete x brs). + split_and!; by apply lookup_delete || rewrite insert_delete. +Qed. + +Lemma matches_opt_step bs brs m strict x d : + matches (M_Matcher (<[x := M_Optional d]>m) strict) bs = Some brs → + (∃ e, bs !! x = Some e ∧ brs !! x = Some (B_Nonrec e)) ∨ + bs !! x = None ∧ brs !! x = Some (B_Rec d). +Proof. + intros Hmatches. + destruct (decide (is_Some (bs !! x))). + - destruct i. left. exists x0. split; [done|]. + unfold matches in Hmatches. + destruct strict; simplify_option_eq. + + replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m)) + in Heqo0; try by rewrite insert_delete_insert. + rewrite matches_aux_insert in Heqo0 by apply lookup_delete. + unfold matches_aux_f in Heqo0. simplify_option_eq. + destruct H3. simplify_option_eq. + apply matches_aux_bs in Heqo as Hdom. simplify_option_eq. + apply lookup_insert. + + replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m)) + in Heqo; try by rewrite insert_delete_insert. + rewrite matches_aux_insert in Heqo by apply lookup_delete. + unfold matches_aux_f in Heqo. simplify_option_eq. + destruct H1. simplify_option_eq. + apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq. + apply lookup_insert. + - unfold matches in Hmatches. + destruct strict; simplify_option_eq. + + right. apply eq_None_not_Some in n. split; [done|]. + destruct H0. simplify_option_eq. + apply matches_aux_bs in Heqo0 as Hbs. subst. + replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m)) + in Heqo0; try by rewrite insert_delete_insert. + rewrite matches_aux_insert in Heqo0 by apply lookup_delete. + unfold matches_aux_f in Heqo0. simplify_option_eq. + destruct H0. simplify_option_eq. + apply matches_aux_bs in Heqo as Hdom. simplify_option_eq. + apply lookup_insert. + + right. apply eq_None_not_Some in n. split; [done|]. + destruct H. simplify_option_eq. + apply matches_aux_bs in Heqo as Hbs. subst. + replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m)) + in Heqo; try by rewrite insert_delete_insert. + rewrite matches_aux_insert in Heqo by apply lookup_delete. + unfold matches_aux_f in Heqo. simplify_option_eq. + destruct H. simplify_option_eq. + apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq. + apply lookup_insert. +Qed. + +Lemma matches_opt_step' bs brs m strict x d : + matches (M_Matcher (<[x := M_Optional d]>m) strict) bs = Some brs → + (∃ e bs' brs', + bs' !! x = None ∧ bs = <[x := e]>bs' ∧ + brs' !! x = None ∧ brs = <[x := B_Nonrec e]>brs') ∨ + (∃ brs', + bs !! x = None ∧ brs' !! x = None ∧ + brs = <[x := B_Rec d]>brs'). +Proof. + intros Hmatches. + apply matches_opt_step in Hmatches as He. + destruct He as [He|He]. + - destruct He as [e [He1 He2]]. left. + exists e, (delete x bs), (delete x brs). + split; try split; try split. + + apply lookup_delete. + + by rewrite insert_delete. + + apply lookup_delete. + + by rewrite insert_delete. + - destruct He as [He1 He2]. right. + exists (delete x brs). split; try split; try done. + + apply lookup_delete. + + by rewrite insert_delete. +Qed. + +Lemma matches_inv m bs brs strict x e : + m !! x = None → bs !! x = None → brs !! x = None → + matches (M_Matcher (<[x := M_Mandatory]>m) strict) (<[x := e]>bs) = + Some (<[x := B_Nonrec e]>brs) → + matches (M_Matcher m strict) bs = Some brs. +Proof. + intros Hxm Hxbs Hxbrs Hmatch. + destruct strict. + - simplify_option_eq. + + destruct H0. apply matches_aux_bs in Heqo0 as Hbs. + simplify_option_eq. by erewrite matches_aux_inv. + + exfalso. apply H2. + repeat rewrite dom_insert in H1. + assert ({[x]} ## dom bs). { by apply singleton_notin_union_disjoint. } + assert ({[x]} ## dom m). { by apply singleton_notin_union_disjoint. } + by apply disjoint_union_subseteq_l with (X := {[x]}). + - simplify_option_eq. + destruct H. apply matches_aux_bs in Heqo as Hbs. + simplify_option_eq. by erewrite matches_aux_inv. +Qed. + +Lemma matches_aux_avail_inv m bs brs x d e : + m !! x = None → bs !! x = None → brs !! x = None → + matches_aux (<[x := M_Optional d]>m) (<[x := e]>bs) = + Some (<[x := e]>bs, <[x := B_Nonrec e]>brs) → + matches_aux m bs = Some (bs, brs). +Proof. + intros Hxm Hxbs Hxbrs Hmatches. + rewrite matches_aux_insert in Hmatches by done. + unfold matches_aux_f in Hmatches. simplify_option_eq. + destruct H. simplify_option_eq. + apply matches_aux_bs in Heqo as Hbs. subst. + rewrite lookup_insert in Hmatches. simplify_option_eq. + apply matches_aux_impl in Heqo; try done. + simplify_option_eq. + apply matches_aux_dom in Heqo as Hdom. + rewrite Heqo. do 2 f_equal. + assert (g0 !! x = None). + { apply not_elem_of_dom in Hxm. + rewrite Hdom in Hxm. + by apply not_elem_of_dom. } + replace g0 with (delete x (<[x:=B_Nonrec e]> g0)); + try by rewrite delete_insert. + replace brs with (delete x (<[x:=B_Nonrec e]> brs)); + try by rewrite delete_insert. + by rewrite Hmatches. +Qed. + +Lemma matches_avail_inv m bs brs strict x d e : + m !! x = None → bs !! x = None → brs !! x = None → + matches (M_Matcher (<[x := M_Optional d]>m) strict) (<[x := e]>bs) = + Some (<[x := B_Nonrec e]>brs) → + matches (M_Matcher m strict) bs = Some brs. +Proof. + intros Hxm Hxbs Hxbrs Hmatch. + destruct strict. + - simplify_option_eq. + + destruct H0. apply matches_aux_bs in Heqo0 as Hbs. + simplify_option_eq. by erewrite matches_aux_avail_inv. + + exfalso. apply H2. + repeat rewrite dom_insert in H1. + assert ({[x]} ## dom bs). { by apply singleton_notin_union_disjoint. } + assert ({[x]} ## dom m). { by apply singleton_notin_union_disjoint. } + by apply disjoint_union_subseteq_l with (X := {[x]}). + - simplify_option_eq. + destruct H. apply matches_aux_bs in Heqo as Hbs. + simplify_option_eq. by erewrite matches_aux_avail_inv. +Qed. + +Lemma matches_aux_default_inv m bs brs x e : + m !! x = None → bs !! x = None → brs !! x = None → + matches_aux (<[x := M_Optional e]>m) bs = + Some (bs, <[x := B_Rec e]>brs) → + matches_aux m bs = Some (bs, brs). +Proof. + intros Hxm Hxbs Hxbrs Hmatches. + rewrite matches_aux_insert in Hmatches by done. + unfold matches_aux_f in Hmatches. simplify_option_eq. + destruct H. simplify_option_eq. + apply matches_aux_bs in Heqo as Hbs. subst. + rewrite Hxbs in Hmatches. simplify_option_eq. + apply matches_aux_dom in Heqo as Hdom. + do 2 f_equal. + assert (g0 !! x = None). + { apply not_elem_of_dom in Hxm. + rewrite Hdom in Hxm. + by apply not_elem_of_dom. } + replace g0 with (delete x (<[x:=B_Rec e]> g0)); + try by rewrite delete_insert. + replace brs with (delete x (<[x:=B_Rec e]> brs)); + try by rewrite delete_insert. + by rewrite Hmatches. +Qed. + +Lemma matches_default_inv m bs brs strict x e : + m !! x = None → bs !! x = None → brs !! x = None → + matches (M_Matcher (<[x := M_Optional e]>m) strict) bs = + Some (<[x := B_Rec e]>brs) → + matches (M_Matcher m strict) bs = Some brs. +Proof. + intros Hxm Hxbs Hxbrs Hmatch. + destruct strict. + - simplify_option_eq. + + destruct H0. apply matches_aux_bs in Heqo0 as Hbs. + simplify_option_eq. by erewrite matches_aux_default_inv. + + exfalso. apply H2. + rewrite dom_insert in H1. + assert ({[x]} ## dom bs). { by apply singleton_notin_union_disjoint. } + assert ({[x]} ## dom m). { by apply singleton_notin_union_disjoint. } + apply disjoint_union_subseteq_l with (X := {[x]}); set_solver. + - simplify_option_eq. + destruct H. apply matches_aux_bs in Heqo as Hbs. + simplify_option_eq. by erewrite matches_aux_default_inv. +Qed. + +Theorem matches_sound m bs brs : matches m bs = Some brs → bs ~ m ~> brs. +Proof. + intros Hmatches. + destruct m. + revert strict bs brs Hmatches. + induction ms using map_ind; intros strict bs brs Hmatches. + - destruct strict; simplify_option_eq. + + apply dom_empty_subset in H0. simplify_eq. + constructor. + + constructor. + - destruct x. + + apply matches_step' in Hmatches as He. + destruct He as [e [bs' [brs' [Hbs'1 [Hbs'2 [Hbrs'1 Hbrs'2]]]]]]. + subst. constructor; try done. + rewrite delete_notin by done. + apply IHms. + by apply matches_inv in Hmatches. + + apply matches_opt_step' in Hmatches as He. destruct He as [He|He]. + * destruct He as [d [bs' [brs' [Hibs' [Hbs' [Hibrs' Hbrs']]]]]]. + subst. constructor; try done. + rewrite delete_notin by done. + apply IHms. + by apply matches_avail_inv in Hmatches. + * destruct He as [brs' [Hibs [Hibrs' Hbrs']]]. + subst. constructor; try done. + apply IHms. + by apply matches_default_inv in Hmatches. +Qed. + +Theorem matches_complete m bs brs : bs ~ m ~> brs → matches m bs = Some brs. +Proof. + intros Hbs. + induction Hbs. + - unfold matches. by simplify_option_eq. + - unfold matches. by simplify_option_eq. + - unfold matches in *. destruct strict. + + simplify_option_eq. + * simplify_option_eq. destruct H2. simplify_option_eq. + apply fmap_Some. exists (<[x := e]>bs, <[x := B_Nonrec e]>g0). + split; [|done]. + rewrite matches_aux_insert by done. + apply matches_aux_bs in Heqo0 as Hbs'. simplify_option_eq. + apply matches_aux_impl_2 with (x := x) (e := e) in Heqo0; + [| done | apply lookup_delete]. + replace bs with (delete x bs); try by apply delete_notin. + unfold matches_aux_f. + simplify_option_eq. apply bind_Some. exists e. + split; [apply lookup_insert | done]. + * exfalso. apply H4. + replace bs with (delete x bs); try by apply delete_notin. + apply map_dom_delete_insert_subseteq_L. + set_solver. + + simplify_option_eq. destruct H1. simplify_option_eq. + apply fmap_Some. exists (<[x := e]>bs, <[x := B_Nonrec e]>g0). + split; [|done]. + rewrite matches_aux_insert by done. + apply matches_aux_bs in Heqo as Hbs'. simplify_option_eq. + apply matches_aux_impl_2 with (x := x) (e := e) in Heqo; + [| done | apply lookup_delete]. + replace bs with (delete x bs); try by apply delete_notin. + unfold matches_aux_f. + simplify_option_eq. apply bind_Some. exists e. + split; [apply lookup_insert | done]. + - unfold matches in *. destruct strict. + + simplify_option_eq. + * simplify_option_eq. destruct H2. simplify_option_eq. + apply fmap_Some. exists (<[x := d]>bs, <[x := B_Nonrec d]>g0). + split; [|done]. + rewrite matches_aux_insert by done. + apply matches_aux_bs in Heqo0 as Hbs'. simplify_option_eq. + apply matches_aux_impl_2 with (x := x) (e := d) in Heqo0; + [| done | apply lookup_delete]. + replace bs with (delete x bs); try by apply delete_notin. + unfold matches_aux_f. + simplify_option_eq. case_match. + -- rewrite lookup_insert in H2. congruence. + -- by rewrite lookup_insert in H2. + * exfalso. apply H4. + replace bs with (delete x bs); try by apply delete_notin. + apply map_dom_delete_insert_subseteq_L. + set_solver. + + simplify_option_eq. destruct H1. simplify_option_eq. + apply fmap_Some. exists (<[x := d]>bs, <[x := B_Nonrec d]>g0). + split; [|done]. + rewrite matches_aux_insert by done. + apply matches_aux_bs in Heqo as Hbs'. simplify_option_eq. + apply matches_aux_impl_2 with (x := x) (e := d) in Heqo; + [| done | apply lookup_delete]. + replace bs with (delete x bs); try by apply delete_notin. + unfold matches_aux_f. + simplify_option_eq. case_match. + * rewrite lookup_insert in H1. congruence. + * by rewrite lookup_insert in H1. + - unfold matches in *. destruct strict. + + simplify_option_eq. + * simplify_option_eq. destruct H2. simplify_option_eq. + apply fmap_Some. exists (bs, <[x := B_Rec e]>g0). + split; [|done]. + rewrite matches_aux_insert by done. + apply matches_aux_bs in Heqo0 as Hbs'. simplify_option_eq. + unfold matches_aux_f. + by simplify_option_eq. + * exfalso. apply H4. set_solver. + + simplify_option_eq. destruct H1. simplify_option_eq. + apply fmap_Some. exists (bs, <[x := B_Rec e]>g0). + split; [|done]. + rewrite matches_aux_insert by done. + apply matches_aux_bs in Heqo as Hbs'. simplify_option_eq. + unfold matches_aux_f. + by simplify_option_eq. +Qed. + +Theorem matches_correct m bs brs : matches m bs = Some brs ↔ bs ~ m ~> brs. +Proof. split; [apply matches_sound | apply matches_complete]. Qed. + +Theorem matches_deterministic m bs brs1 brs2 : + bs ~ m ~> brs1 → bs ~ m ~> brs2 → brs1 = brs2. +Proof. intros H1 H2. apply matches_correct in H1, H2. congruence. Qed. diff --git a/relations.v b/relations.v new file mode 100644 index 0000000..9bfb7e6 --- /dev/null +++ b/relations.v @@ -0,0 +1,73 @@ +From stdpp Require Import relations. + +Definition deterministic {A} (R : relation A) := + ∀ x y1 y2, R x y1 → R x y2 → y1 = y2. + +(* As in Baader and Nipkow (1998): *) +(* y is a normal form of x if x -->* y and y is in normal form. *) +Definition is_nf_of `(R : relation A) x y := (rtc R x y) ∧ nf R y. + +(** The reflexive closure. *) +Inductive rc {A} (R : relation A) : relation A := + | rc_refl x : rc R x x + | rc_once x y : R x y → rc R x y. + +Hint Constructors rc : core. + +(* Baader and Nipkow, Definition 2.7.3. *) +Definition strongly_confluent {A} (R : relation A) := + ∀ x y1 y2, R x y1 → R x y2 → ∃ z, rtc R y1 z ∧ rc R y2 z. + +(* Baader and Nipkow, Definition 2.1.4. *) +Definition semi_confluent {A} (R : relation A) := + ∀ x y1 y2, R x y1 → rtc R x y2 → ∃ z, rtc R y1 z ∧ rtc R y2 z. + +(* Lemma 2.7.4 from Baader and Nipkow *) +Lemma strong__semi_confluence {A} (R : relation A) : + strongly_confluent R → semi_confluent R. +Proof. + intros Hstrc. + unfold strongly_confluent in Hstrc. + unfold semi_confluent. + intros x1 y1 xn Hxy1 [steps Hsteps] % rtc_nsteps. + revert x1 y1 xn Hxy1 Hsteps. + induction steps; intros x1 y1 xn Hxy1 Hsteps. + - inv Hsteps. exists y1. + split. + + apply rtc_refl. + + by apply rtc_once. + - inv Hsteps as [|? ? x2 ? Hx1x2 Hsteps']. + destruct (Hstrc x1 y1 x2 Hxy1 Hx1x2) as [y2 [Hy21 Hy22]]. + inv Hy22. + + exists xn. split; [|done]. + apply rtc_transitive with (y := y2); [done|]. + rewrite rtc_nsteps. by exists steps. + + destruct (IHsteps x2 y2 xn H Hsteps') as [yn [Hy2yn Hxnyn]]. + exists yn. split; [|done]. + by apply rtc_transitive with (y := y2). +Qed. + +(* Copied from stdpp, originates from Baader and Nipkow (1998) *) +Definition cr {A} (R : relation A) := + ∀ x y, rtsc R x y → ∃ z, rtc R x z ∧ rtc R y z. + +(* Part of Lemma 2.1.5 from Baader and Nipkow (1998) *) +Lemma semi_confluence__cr {A} (R : relation A) : + semi_confluent R → cr R. +Proof. + intros Hsc. + unfold semi_confluent in Hsc. + unfold cr. + intros x y [steps Hsteps] % rtc_nsteps. + revert x y Hsteps. + induction steps; intros x y Hsteps. + - inv Hsteps. by exists y. + - inv Hsteps. rename x into y', y into x, y0 into y. + apply IHsteps in H1 as H1'. destruct H1' as [z [Hz1 Hz2]]. + destruct H0. + + exists z. split; [|done]. + by apply rtc_l with (y := y). + + destruct (Hsc y y' z H Hz1) as [z' [Hz'1 Hz'2]]. + exists z'. split; [done|]. + by apply rtc_transitive with (y := z). +Qed. diff --git a/sem.v b/sem.v new file mode 100644 index 0000000..6560b82 --- /dev/null +++ b/sem.v @@ -0,0 +1,167 @@ +Require Import Coq.Strings.String. +From stdpp Require Import gmap. +From mininix Require Import binop expr matching relations. + +Definition attrset := is_Some ∘ maybe V_Attrset. + +Reserved Infix "-->base" (right associativity, at level 55). + +Inductive base_step : expr → expr → Prop := + | E_Force (sv : strong_value) : + X_Force sv -->base sv + | E_Closed e : + X_Closed e -->base e + | E_Placeholder x e : + X_Placeholder x e -->base e + | E_MSelect bs x ys : + X_Select (V_Attrset bs) (nonempty_cons x ys) -->base + X_Select (X_Select (V_Attrset bs) (nonempty_singleton x)) ys + | E_Select e bs x : + X_Select (V_Attrset (<[x := e]>bs)) (nonempty_singleton x) -->base e + | E_SelectOr bs x e : + X_SelectOr (V_Attrset bs) (nonempty_singleton x) e -->base + X_Cond (X_HasAttr (V_Attrset bs) x) + (* if true *) + (X_Select (V_Attrset bs) (nonempty_singleton x)) + (* if false *) + e + | E_MSelectOr bs x ys e : + X_SelectOr (V_Attrset bs) (nonempty_cons x ys) e -->base + X_Cond (X_HasAttr (V_Attrset bs) x) + (* if true *) + (X_SelectOr + (X_Select (V_Attrset bs) (nonempty_singleton x)) + ys e) + (* if false *) + e + | E_Rec bs : + X_Attrset bs -->base V_Attrset (rec_subst bs) + | E_Let e bs : + X_LetBinding bs e -->base subst (closed (rec_subst bs)) e + | E_With e bs : + X_Incl (V_Attrset bs) e -->base subst (placeholders bs) e + | E_WithNoAttrset v1 e2 : + ¬ attrset v1 → + X_Incl v1 e2 -->base e2 + | E_ApplySimple x e1 e2 : + X_Apply (V_Fn x e1) e2 -->base subst {[x := X_Closed e2]} e1 + | E_ApplyAttrset m e bs bs' : + bs ~ m ~> bs' → + X_Apply (V_AttrsetFn m e) (V_Attrset bs) -->base + X_LetBinding bs' e + | E_ApplyFunctor e1 e2 bs : + X_Apply (V_Attrset (<["__functor" := e2]>bs)) e1 -->base + X_Apply (X_Apply e2 (V_Attrset (<["__functor" := e2]>bs))) e1 + | E_IfTrue e2 e3 : + X_Cond true e2 e3 -->base e2 + | E_IfFalse e2 e3 : + X_Cond false e2 e3 -->base e3 + | E_Op op v1 v2 u : + v1 ⟦op⟧ v2 -⊚-> u → + X_Op op v1 v2 -->base u + | E_OpHasAttrTrue bs x : + is_Some (bs !! x) → + X_HasAttr (V_Attrset bs) x -->base true + | E_OpHasAttrFalse bs x : + bs !! x = None → + X_HasAttr (V_Attrset bs) x -->base false + | E_OpHasAttrNoAttrset v x : + ¬ attrset v → + X_HasAttr v x -->base false + | E_Assert e2 : + X_Assert true e2 -->base e2 +where "e -->base e'" := (base_step e e'). + +Notation "e '-->base*' e'" := (rtc base_step e e') + (right associativity, at level 55). + +Hint Constructors base_step : core. + +Variant is_ctx_item : bool → bool → (expr → expr) → Prop := + | IsCtxItem_Select uf_ext xs : + is_ctx_item uf_ext false (λ e1, X_Select e1 xs) + | IsCtxItem_SelectOr uf_ext xs e2 : + is_ctx_item uf_ext false (λ e1, X_SelectOr e1 xs e2) + | IsCtxItem_Incl uf_ext e2 : + is_ctx_item uf_ext false (λ e1, X_Incl e1 e2) + | IsCtxItem_ApplyL uf_ext e2 : + is_ctx_item uf_ext false (λ e1, X_Apply e1 e2) + | IsCtxItem_ApplyAttrsetR uf_ext m e1 : + is_ctx_item uf_ext false (λ e2, X_Apply (V_AttrsetFn m e1) e2) + | IsCtxItem_CondL uf_ext e2 e3 : + is_ctx_item uf_ext false (λ e1, X_Cond e1 e2 e3) + | IsCtxItem_AssertL uf_ext e2 : + is_ctx_item uf_ext false (λ e1, X_Assert e1 e2) + | IsCtxItem_OpL uf_ext op e2 : + is_ctx_item uf_ext false (λ e1, X_Op op e1 e2) + | IsCtxItem_OpR uf_ext op v1 : + is_ctx_item uf_ext false (λ e2, X_Op op (X_V v1) e2) + | IsCtxItem_OpHasAttrL uf_ext x : + is_ctx_item uf_ext false (λ e, X_HasAttr e x) + | IsCtxItem_Force uf_ext : + is_ctx_item uf_ext true (λ e, X_Force e) + | IsCtxItem_ForceAttrset bs x : + is_ctx_item true true (λ e, X_V (V_Attrset (<[x := e]>bs))). + +Hint Constructors is_ctx_item : core. + +Inductive is_ctx : bool → bool → (expr → expr) → Prop := + | IsCtx_Id uf : is_ctx uf uf id + | IsCtx_Compose E1 E2 uf_int uf_aux uf_ext : + is_ctx_item uf_ext uf_aux E1 → + is_ctx uf_aux uf_int E2 → + is_ctx uf_ext uf_int (E1 ∘ E2). + +Hint Constructors is_ctx : core. + +(* /--> This is required because the standard library definition of "-->" + | (in Coq.Classes.Morphisms, for `respectful`) defines that this operator + | uses right associativity. Our definition must match exactly, as Coq + | will give an error otherwise. + \-------------------------------------\ + | | *) +Reserved Infix "-->" (right associativity, at level 55). + +Variant step : expr → expr → Prop := + E_Ctx e1 e2 E uf_int : + is_ctx false uf_int E → + e1 -->base e2 → + E e1 --> E e2 +where "e --> e'" := (step e e'). + +Hint Constructors step : core. + +Notation "e '-->*' e'" := (rtc step e e') (right associativity, at level 55). + +(** Theories for contexts *) + +Lemma is_ctx_once uf_ext uf_int E : + is_ctx_item uf_ext uf_int E → is_ctx uf_ext uf_int E. +Proof. intros. eapply IsCtx_Compose; [done | constructor]. Qed. + +Lemma is_ctx_item_ext_imp E uf_int : + is_ctx_item false uf_int E → is_ctx_item true uf_int E. +Proof. intros H. inv H; constructor. Qed. + +Lemma is_ctx_ext_imp E1 E2 uf_aux uf_int : + is_ctx_item false uf_aux E1 → + is_ctx uf_aux uf_int E2 → + is_ctx true uf_int (E1 ∘ E2). +Proof. + intros H1 H2. + revert E1 H1. + induction H2; intros. + - inv H1; eapply IsCtx_Compose; constructor. + - eapply IsCtx_Compose. + + by apply is_ctx_item_ext_imp in H1. + + by eapply IsCtx_Compose. +Qed. + +Lemma is_ctx_uf_false_impl_true E uf_int : + is_ctx false uf_int E → + is_ctx true uf_int E ∨ E = id. +Proof. + intros Hctx. inv Hctx. + - by right. + - left. eapply is_ctx_ext_imp; [apply H | apply H0]. +Qed. diff --git a/semprop.v b/semprop.v new file mode 100644 index 0000000..3af718d --- /dev/null +++ b/semprop.v @@ -0,0 +1,426 @@ +Require Import Coq.Strings.String. +From stdpp Require Import gmap option tactics. +From mininix Require Import binop expr maptools matching relations sem. + +Lemma ctx_item_inj E uf_ext uf_int : + is_ctx_item uf_ext uf_int E → + Inj (=) (=) E. +Proof. + intros Hctx. + destruct Hctx; intros e1' e2' Hinj; try congruence. + injection Hinj as Hinj. + by apply map_insert_rev_1_L in Hinj. +Qed. + +Global Instance id_inj {A} : Inj (=) (=) (@id A). +Proof. by unfold Inj. Qed. + +Lemma ctx_inj E uf_ext uf_int : + is_ctx uf_ext uf_int E → + Inj (=) (=) E. +Proof. + intros Hctx. + induction Hctx. + - apply id_inj. + - apply ctx_item_inj in H. + by apply compose_inj with (=). +Qed. + +Lemma base_step_deterministic : deterministic base_step. +Proof. + unfold deterministic. + intros e0 e1 e2 H1 H2. + inv H1; inv H2; try done. + - destruct ys, ys0. by simplify_eq/=. + - destruct ys. by simplify_eq/=. + - destruct ys. by simplify_eq/=. + - apply map_insert_inv in H0. by destruct H0. + - destruct ys. by simplify_eq/=. + - destruct ys. by simplify_eq/=. + - destruct ys, ys0. by simplify_eq/=. + - exfalso. apply H3. by exists bs. + - exfalso. apply H. by exists bs. + - f_equal. by eapply matches_deterministic. + - apply map_insert_inv in H0 as [H01 H02]. + by simplify_eq /=. + - f_equal. by eapply binop_deterministic. + - rewrite H4 in H. by apply is_Some_None in H. + - exfalso. apply H4. by exists bs. + - rewrite H in H4. by apply is_Some_None in H4. + - exfalso. apply H. by exists bs. +Qed. + +Reserved Notation "e '-/' uf '/->' e'" (right associativity, at level 55). + +Inductive fstep : bool → expr → expr → Prop := + | F_Ctx e1 e2 E uf_ext uf_int : + is_ctx uf_ext uf_int E → + e1 -->base e2 → + E e1 -/uf_ext/-> E e2 +where "e -/ uf /-> e'" := (fstep uf e e'). + +Hint Constructors fstep : core. + +Lemma ufstep e e' : e -/false/-> e' ↔ e --> e'. +Proof. split; intros; inv H; by econstructor. Qed. + +Lemma fstep_strongly_confluent_aux x uf y1 y2 : + x -/uf/-> y1 → + x -/uf/-> y2 → + y1 = y2 ∨ ∃ z, y1 -/uf/-> z ∧ y2 -/uf/-> z. +Proof. + intros Hstep1 Hstep2. + inv Hstep1 as [b11 b12 E1 uf_int uf_int1 Hctx1 Hbase1]. + inv Hstep2 as [b21 b22 E2 uf_int uf_int2 Hctx2 Hbase2]. + revert b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H0. + induction Hctx1 as [|E1 E0]; + intros b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H2; inv Hctx2. + - (* L: id, R: id *) left. by eapply base_step_deterministic. + - (* L: id, R: ∘ *) simplify_eq/=. + inv H. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H. + * inv H0. + -- inv Hbase2. + -- inv H1. inv H. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H. + * inv H0. + -- inv Hbase2. + -- inv H. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H. + * inv H0. + -- inv Hbase2. + -- inv H1. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H. + * inv H0. + -- inv Hbase2. + -- inv H1. + * inv H0. + -- inv Hbase2. + -- inv H1. inv H. + + inv Hbase1. + inv H0. + * inv Hbase2. + * inv H. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H. + * inv H0. + -- inv Hbase2. + -- inv H. + + inv Hbase1. + inv H0. + * inv Hbase2. + * inv H. + + inv Hbase1. + inv H0. + * inv Hbase2. + * inv H. + + inv Hbase1. + inv H0. + * inv Hbase2. + * inv H. + + inv Hbase1. + * inv H0. + -- inv Hbase2. + -- inv H1. + * inv H0. + -- inv Hbase2. + -- inv H1. + * inv H0. + -- inv Hbase2. + -- inv H1. + + inv Hbase1. + inv H0. + * inv Hbase2. + * inv H. + simplify_option_eq. + destruct sv; try discriminate. + exfalso. clear uf. simplify_option_eq. + apply fmap_insert_lookup in H1. simplify_option_eq. + revert bs0 x H H1 Heqo. + induction H2; intros bs0 x H' H1 Heqo. + -- inv Hbase2. + -- simplify_option_eq. + inv H. destruct H'; try discriminate. + inv H1. apply fmap_insert_lookup in H0. simplify_option_eq. + by eapply IHis_ctx. + + inv Hbase1. + - (* L: ∘, R: id *) + simplify_eq/=. + inv H. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. inv H. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. inv H. + + inv Hbase2. + inv Hctx1. + * inv Hbase1. + * inv H. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + * inv Hctx1. + -- inv Hbase1. + -- inv H. + + inv Hbase2. + inv Hctx1. + * inv Hbase1. + * inv H. + + inv Hbase2. + inv Hctx1. + * inv Hbase1. + * inv H. + + inv Hbase2. + inv Hctx1. + * inv Hbase1. + * inv H. + + inv Hbase2. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. + * inv Hctx1. + -- inv Hbase1. + -- inv H0. + + inv Hbase2. + inv Hctx1. + * inv Hbase1. + * clear IHHctx1. + inv H. + simplify_option_eq. + destruct sv; try discriminate. + exfalso. simplify_option_eq. + apply fmap_insert_lookup in H0. simplify_option_eq. + revert bs0 x H H0 Heqo. + induction H1; intros bs0 x H' H0 Heqo. + -- inv Hbase1. + -- simplify_option_eq. + inv H. destruct H'; try discriminate. + inv H0. apply fmap_insert_lookup in H2. simplify_option_eq. + eapply IHis_ctx. + ++ apply H2. + ++ apply Heqo0. + + inv Hbase2. + - (* L: ∘, R: ∘ *) + simplify_option_eq. + inv H; inv H0. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Select z xs). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e, X_Select e xs) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_SelectOr z xs e2). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_SelectOr e1 xs e2) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Incl z e2). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_Incl e1 e2) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Apply z e2). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_Apply e1 e2) ∘ E); try done; + by eapply IsCtx_Compose. + + inv Hctx1; simplify_option_eq. + * inv Hbase1. + * inv H. + + inv H1; simplify_option_eq. + * inv Hbase2. + * inv H. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H0) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Apply (V_AttrsetFn m e1) z). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e2, X_Apply (V_AttrsetFn m e1) e2) ∘ E); + try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Cond z e2 e3). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_Cond e1 e2 e3) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Assert z e2). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_Assert e1 e2) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Op op z e2). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e1, X_Op op e1 e2) ∘ E); try done; + by eapply IsCtx_Compose. + + inv Hctx1; simplify_option_eq. + * inv Hbase1. + * inv H0. + + inv H1; simplify_option_eq. + * inv Hbase2. + * inv H0. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H0) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Op op v1 z). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e2, X_Op op v1 e2) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_HasAttr z x). + split; [inv IHz1 | inv IHz2]; + eapply F_Ctx with (E := (λ e, X_HasAttr e x) ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2) + as [IH | [z [IHz1 IHz2]]]. + * left. congruence. + * right. exists (X_Force z). + split. + -- inv IHz1. + (* apply is_ctx_uf_false_impl_true in H0 as []. *) + eapply F_Ctx with (E := X_Force ∘ E); try done; + by eapply IsCtx_Compose. + -- inv IHz2. + eapply F_Ctx with (E := X_Force ∘ E); try done; + by eapply IsCtx_Compose. + + destruct (decide (x0 = x)). + * simplify_option_eq. + apply map_insert_rev_L in H2 as [H21 H22]. + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H21) + as [IH | [z [IHz1 IHz2]]]. + -- left. rewrite IH. do 2 f_equal. + by apply map_insert_L. + -- right. exists (V_Attrset (<[x := z]>bs)). + split. + ++ inv IHz1. + eapply F_Ctx + with (E := (λ e, X_V $ V_Attrset (<[x := e]>bs)) ∘ E); try done. + by eapply IsCtx_Compose. + ++ inv IHz2. + rewrite (map_insert_L _ _ _ _ _ (eq_refl (E e1)) H22). + eapply F_Ctx + with (E := (λ e, X_V $ V_Attrset (<[x := e]>bs)) ∘ E); try done. + by eapply IsCtx_Compose. + * simplify_option_eq. + right. exists (V_Attrset (<[x := E0 b12]>(<[x0 := E4 b22]>bs))). + split. + -- apply map_insert_ne_inv in H2 as H3; try done. + destruct H3. + replace bs with (<[x0 := E4 b21]>bs) at 1; try by rewrite insert_id. + setoid_rewrite insert_commute; try by congruence. + eapply F_Ctx + with (E := (λ e, X_V $ V_Attrset + (<[x0 := e]>(<[x := E0 b12]> bs))) ∘ E4). + ++ by eapply IsCtx_Compose. + ++ done. + -- apply map_insert_ne_inv in H2 as H3; try done. + destruct H3 as [H31 [H32 H33]]. + replace bs0 with (<[x := E0 b11]>bs0) at 1; + try by rewrite insert_id. + rewrite insert_commute; try by congruence. + replace (<[x:=E0 b11]> (<[x0:=E4 b22]> bs0)) + with (<[x:=E0 b11]> (<[x0:=E4 b22]> bs)). + 2: { + rewrite <-insert_delete_insert. + setoid_rewrite <-insert_delete_insert at 2. + rewrite delete_insert_ne by congruence. + rewrite delete_commute. rewrite <-H33. + rewrite insert_delete_insert. + rewrite <-delete_insert_ne by congruence. + by rewrite insert_delete_insert. + } + eapply F_Ctx with (E := (λ e, X_V $ V_Attrset + (<[x := e]>(<[x0 := E4 b22]>bs))) ∘ E0). + ++ by eapply IsCtx_Compose. + ++ done. +Qed. + +Lemma step_strongly_confluent_aux x y1 y2 : + x --> y1 → + x --> y2 → + y1 = y2 ∨ ∃ z, y1 --> z ∧ y2 --> z. +Proof. + intros Hstep1 Hstep2. + apply ufstep in Hstep1, Hstep2. + destruct (fstep_strongly_confluent_aux _ _ _ _ Hstep1 Hstep2) as [|[?[]]]. + - by left. + - right. exists x0. split; by apply ufstep. +Qed. + +Theorem step_strongly_confluent : strongly_confluent step. +Proof. + intros x y1 y2 Hy1 Hy2. + destruct (step_strongly_confluent_aux x y1 y2 Hy1 Hy2) as [|[z [Hz1 Hz2]]]. + - exists y1. by subst. + - exists z. split. + + by apply rtc_once. + + by apply rc_once. +Qed. + +Lemma step_semi_confluent : semi_confluent step. +Proof. apply strong__semi_confluence. apply step_strongly_confluent. Qed. + +Lemma step_cr : cr step. +Proof. apply semi_confluence__cr. apply step_semi_confluent. Qed. + +Theorem step_confluent : confluent step. +Proof. apply confluent_alt. apply step_cr. Qed. diff --git a/shared.v b/shared.v new file mode 100644 index 0000000..8e9484f --- /dev/null +++ b/shared.v @@ -0,0 +1,66 @@ +Require Import Coq.NArith.BinNat. +Require Import Coq.Strings.Ascii. +Require Import Coq.Strings.String. +From stdpp Require Import fin_sets gmap option. +From mininix Require Import expr maptools. + +Open Scope string_scope. +Open Scope N_scope. +Open Scope Z_scope. +Open Scope nat_scope. + +Definition nonrecs : gmap string b_rhs → gmap string expr := + omap (λ b, match b with B_Nonrec e => Some e | _ => None end). + +Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs. +Proof. + induction bs using map_ind. + - done. + - unfold nonrecs. + rewrite fmap_insert. + rewrite omap_insert_Some with (y := x); try done. + by f_equal. +Qed. + +Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs. +Proof. + unfold rec_subst. + rewrite <-map_fmap_compose. + unfold compose. + by rewrite map_fmap_id. +Qed. + +Definition ascii_ltb (c1 c2 : ascii) : bool := + bool_decide (N_of_ascii c1 < N_of_ascii c2)%N. + +Fixpoint string_lt (s1 s2 : string) : bool := + match s1, s2 with + | _, EmptyString => false + | EmptyString, String _ _ => true + | String c1 s1', String c2 s2' => ascii_ltb c1 c2 || string_lt s1' s2' + end. + +Fixpoint expr_eq (e1 e2 : expr) : bool := + match e1, e2 with + | V_Null, V_Null => false + | V_Bool b1, V_Bool b2 => bool_decide (b1 = b2) + | V_Int n1, V_Int n2 => bool_decide (n1 = n2) + | V_Str s1, V_Str s2 => bool_decide (s1 = s2) + | V_Attrset bs1, V_Attrset bs2 => bool_decide (dom bs1 = dom bs2) && + map_fold (λ x e1' acc, match bs2 !! x with + | None => false + | Some e2' => acc && expr_eq e1' e2' + end) true bs1 + | _, _ => false + end. + +Definition prelude : gmap string expr := + {[ "true" := X_V true; + "false" := X_V false; + "null" := X_V V_Null; + "builtins" := X_Attrset + {[ "true" := B_Nonrec true; + "false" := B_Nonrec false; + "null" := B_Nonrec V_Null + ]} + ]}. diff --git a/sound.v b/sound.v new file mode 100644 index 0000000..761d7ad --- /dev/null +++ b/sound.v @@ -0,0 +1,630 @@ +Require Import Coq.Strings.String. +From stdpp Require Import base gmap relations tactics. +From mininix Require Import + binop expr interpreter maptools matching relations sem. + +Lemma strong_value_stuck sv : ¬ ∃ e, expr_from_strong_value sv --> e. +Proof. + intros []. destruct sv; inv H; inv H1; + simplify_option_eq; (try inv H2); inv H. +Qed. + +Lemma strong_value_stuck_rtc sv e: + expr_from_strong_value sv -->* e → + e = expr_from_strong_value sv. +Proof. + intros. inv H. + - reflexivity. + - exfalso. apply strong_value_stuck with (sv := sv). by exists y. +Qed. + +Lemma force__strong_value (e : expr) (v : value) : + X_Force e -->* v → + ∃ sv, v = value_from_strong_value sv. +Proof. + intros [n Hsteps] % rtc_nsteps. + revert e v Hsteps. + induction n; intros e v Hsteps; inv Hsteps. + inv H0. inv H2; simplify_eq/=. + - inv H3. + exists sv. + apply rtc_nsteps_2 in H1. + apply strong_value_stuck_rtc in H1. + unfold expr_from_strong_value, compose in H1. + congruence. + - inv H0. + destruct (IHn _ _ H1) as [sv Hsv]. + by exists sv. +Qed. + +Lemma forall2_force__strong_values es (vs : gmap string value) : + map_Forall2 (λ e v', X_Force e -->* X_V v') es vs → + ∃ svs, vs = value_from_strong_value <$> svs. +Proof. + revert vs. + induction es using map_ind; intros vs HForall2. + - apply map_Forall2_empty_l_L in HForall2. by exists ∅. + - destruct (map_Forall2_destruct _ _ _ _ _ HForall2) + as [v [m2' [Him2' Heqvs]]]. simplify_eq/=. + apply map_Forall2_insert_inv_strict in HForall2 + as [Hstep HForall2]; try done. + apply IHes in HForall2 as [svs Hsvs]. simplify_eq/=. + apply force__strong_value in Hstep as [sv Hsv]. simplify_eq/=. + exists (<[i := sv]>svs). by rewrite fmap_insert. +Qed. + +Lemma force_strong_value_forall2_impl es (svs : gmap string strong_value) : + map_Forall2 (λ e v', X_Force e -->* X_V v') + es (value_from_strong_value <$> svs) → + map_Forall2 (λ e sv', X_Force e -->* expr_from_strong_value sv') es svs. +Proof. apply map_Forall2_fmap_r_L. Qed. + +Lemma force_map_fmap_union_insert (sws : gmap string strong_value) es k e sv : + X_Force e -->* expr_from_strong_value sv → + X_Force (X_V (V_Attrset (<[k := e]>es ∪ + (expr_from_strong_value <$> sws)))) -->* + X_Force (X_V (V_Attrset (<[k := expr_from_strong_value sv]>es ∪ + (expr_from_strong_value <$> sws)))). +Proof. + intros [n Hsteps] % rtc_nsteps. + revert sws es k e Hsteps. + induction n; intros sws es k e Hsteps. + - inv Hsteps. + - inv Hsteps. + inv H0. + inv H2. + + inv H3. inv H1. + * simplify_option_eq. unfold expr_from_strong_value, compose. + by rewrite H4. + * edestruct strong_value_stuck. exists y. done. + + inv H0. simplify_option_eq. + apply rtc_transitive + with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪ + (expr_from_strong_value <$> sws))))). + * do 2 rewrite <-insert_union_l. + apply rtc_once. + eapply E_Ctx + with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪ + (expr_from_strong_value <$> sws)))))). + -- eapply IsCtx_Compose. + ++ constructor. + ++ eapply IsCtx_Compose + with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪ + (expr_from_strong_value <$> sws)))))). + ** constructor. + ** done. + -- done. + * by apply IHn. +Qed. + +Lemma insert_union_fmap__union_fmap_insert {A B} (f : A → B) i x + (m1 : gmap string B) (m2 : gmap string A) : + m1 !! i = None → + <[i := f x]>m1 ∪ (f <$> m2) = m1 ∪ (f <$> <[i := x]>m2). +Proof. + intros Him1. + rewrite fmap_insert. + rewrite <-insert_union_l. + by rewrite <-insert_union_r. +Qed. + +Lemma fmap_insert_union__fmap_union_insert {A B} (f : A → B) i x + (m1 : gmap string A) (m2 : gmap string A) : + m1 !! i = None → + f <$> <[i := x]>m1 ∪ m2 = f <$> m1 ∪ <[i := x]>m2. +Proof. + intros Him1. + do 2 rewrite map_fmap_union. + rewrite 2 fmap_insert. + rewrite <-insert_union_l. + rewrite <-insert_union_r; try done. + rewrite lookup_fmap. + by rewrite Him1. +Qed. + +Lemma force_map_fmap_union (sws svs : gmap string strong_value) es : + map_Forall2 (λ e sv, X_Force e -->* expr_from_strong_value sv) es svs → + X_Force (X_V (V_Attrset (es ∪ (expr_from_strong_value <$> sws)))) -->* + X_Force (X_V (V_Attrset (expr_from_strong_value <$> svs ∪ sws))). +Proof. + revert sws svs. + induction es using map_ind; intros sws svs HForall2. + - apply map_Forall2_empty_l_L in HForall2. + subst. by do 2 rewrite map_empty_union. + - apply map_Forall2_destruct in HForall2 as HForall2'. + destruct HForall2' as [sv [svs' [Him2' Heqm2']]]. subst. + apply map_Forall2_insert_inv_strict + in HForall2 as [HForall21 HForall22]; try done. + apply rtc_transitive with (X_Force + (X_V (V_Attrset (<[i := expr_from_strong_value sv]> m ∪ + (expr_from_strong_value <$> sws))))). + + by apply force_map_fmap_union_insert. + + rewrite insert_union_fmap__union_fmap_insert by done. + rewrite fmap_insert_union__fmap_union_insert by done. + by apply IHes. +Qed. + +(* See 194+2024-0525-2305 for proof sketch *) +Lemma force_map_fmap (svs : gmap string strong_value) (es : gmap string expr) : + map_Forall2 (λ e sv, X_Force e -->* expr_from_strong_value sv) es svs → + X_Force (X_V (V_Attrset es)) -->* + X_Force (X_V (V_Attrset (expr_from_strong_value <$> svs))). +Proof. + pose proof (force_map_fmap_union ∅ svs es). + rewrite fmap_empty in H. by do 2 rewrite map_union_empty in H. +Qed. + +Lemma id_compose_l {A B} (f : A → B) : id ∘ f = f. +Proof. done. Qed. + +Lemma is_ctx_trans uf_ext uf_aux uf_int E1 E2 : + is_ctx uf_ext uf_aux E1 → + is_ctx uf_aux uf_int E2 → + is_ctx uf_ext uf_int (E1 ∘ E2). +Proof. + intros. + induction H. + - induction H0. + + apply IsCtx_Id. + + rewrite id_compose_l. + by apply IsCtx_Compose with uf_aux. + - apply IHis_ctx in H0. + replace (E1 ∘ E0 ∘ E2) with (E1 ∘ (E0 ∘ E2)) by done. + by apply IsCtx_Compose with uf_aux. +Qed. + +Lemma ctx_mstep e e' E : + e -->* e' → is_ctx false false E → E e -->* E e'. +Proof. + intros. + induction H. + - apply rtc_refl. + - inv H. + pose proof (is_ctx_trans false false uf_int E E0 H0 H2). + eapply rtc_l. + + replace (E (E0 e1)) with ((E ∘ E0) e1) by done. + eapply E_Ctx; [apply H | apply H3]. + + assumption. +Qed. + +Definition is_nonempty_ctx (uf_ext uf_int : bool) (E : expr → expr) := + ∃ E1 E2 uf_aux, + is_ctx_item uf_ext uf_aux E1 ∧ + is_ctx uf_aux uf_int E2 ∧ E = E1 ∘ E2. + +Lemma nonempty_ctx_mstep e e' uf_int E : + e -->* e' → is_nonempty_ctx false uf_int E → E e -->* E e'. +Proof. + intros Hmstep Hctx. + destruct Hctx as [E1 [E2 [uf_aux [Hctx1 [Hctx2 Hctx3]]]]]. + simplify_option_eq. + induction Hmstep. + + apply rtc_refl. + + apply rtc_l with (y := (E1 ∘ E2) y). + * inv H. + destruct (is_ctx_uf_false_impl_true E uf_int0 H0). + +++ apply E_Ctx with (E := E1 ∘ (E2 ∘ E)) (uf_int := uf_int0). + ++ eapply IsCtx_Compose. + ** apply Hctx1. + ** eapply is_ctx_trans. + --- apply Hctx2. + --- destruct uf_int; assumption. + ++ assumption. + +++ apply E_Ctx with (E := E1 ∘ (E2 ∘ E)) (uf_int := uf_int). + ++ eapply IsCtx_Compose. + ** apply Hctx1. + ** eapply is_ctx_trans; simplify_option_eq. + --- apply Hctx2. + --- constructor. + ++ assumption. + * apply IHHmstep. +Qed. + +Lemma force_strong_value (sv : strong_value) : + X_Force sv -->* sv. +Proof. + destruct sv using strong_value_ind'; + apply rtc_once; eapply E_Ctx with (E := id); constructor. +Qed. + +Lemma id_compose_r {A B} (f : A → B) : f ∘ id = f. +Proof. done. Qed. + +Lemma force_idempotent e (v' : value) : + X_Force e -->* v' → + X_Force (X_Force e) -->* v'. +Proof. + intros H. + destruct (force__strong_value _ _ H) as [sv Hsv]. subst. + apply rtc_transitive with (y := X_Force sv). + * eapply nonempty_ctx_mstep; try assumption. + rewrite <-id_compose_r. + exists X_Force, id, true. + repeat (split || constructor || done). + * apply force_strong_value. +Qed. + +(* Conditional force *) +Definition cforce (uf : bool) e := if uf then X_Force e else e. + +Lemma cforce_strong_value uf (sv : strong_value) : + cforce uf sv -->* sv. +Proof. destruct uf; try done. apply force_strong_value. Qed. + +Theorem eval_sound_strong n uf e v' : + eval n uf e = Some v' → + cforce uf e -->* v'. +Proof. + revert uf e v'. + induction n; intros uf e v' Heval. + - discriminate. + - destruct e; rewrite eval_S in Heval; simplify_option_eq; try done. + + (* X_V *) + case_match; simplify_option_eq. + * (* V_Bool *) + replace (V_Bool p) with (value_from_strong_value (SV_Bool p)) by done. + apply cforce_strong_value. + * (* V_Null *) + replace V_Null with (value_from_strong_value SV_Null) by done. + apply cforce_strong_value. + * (* V_Int *) + replace (V_Int n0) with (value_from_strong_value (SV_Int n0)) by done. + apply cforce_strong_value. + * (* V_Str *) + replace (V_Str s) with (value_from_strong_value (SV_Str s)) by done. + apply cforce_strong_value. + * (* V_Fn *) + replace (V_Fn x e) with (value_from_strong_value (SV_Fn x e)) by done. + apply cforce_strong_value. + * (* V_AttrsetFn *) + replace (V_AttrsetFn m e) + with (value_from_strong_value (SV_AttrsetFn m e)) by done. + apply cforce_strong_value. + * (* V_Attrset *) + case_match; simplify_option_eq; try done. + apply map_mapM_Some_L in Heqo. simplify_option_eq. + eapply map_Forall2_impl_L in Heqo. 2: { intros a b. apply IHn. } + destruct (forall2_force__strong_values _ _ Heqo). subst. + apply force_strong_value_forall2_impl in Heqo. + rewrite <-map_fmap_compose. fold expr_from_strong_value. + apply force_map_fmap in Heqo. + apply rtc_transitive + with (y := X_Force (X_V (V_Attrset (expr_from_strong_value <$> x)))); + try done. + apply rtc_once. + eapply E_Ctx with (E := id); [constructor|]. + replace (X_V (V_Attrset (expr_from_strong_value <$> x))) + with (expr_from_strong_value (SV_Attrset x)) by reflexivity. + apply E_Force. + + (* X_Attrset *) + apply IHn in Heval. + apply rtc_transitive with (y := cforce uf (V_Attrset (rec_subst bs))); + [|done]. + destruct uf; simplify_eq/=. + -- eapply nonempty_ctx_mstep with (E := X_Force). + ++ by eapply rtc_once, E_Ctx with (E := id). + ++ by exists X_Force, id, true. + -- apply rtc_once. by eapply E_Ctx with (E := id). + + (* X_LetBinding *) + apply IHn in Heval. + apply rtc_transitive + with (y := cforce uf (subst (closed (rec_subst bs)) e)); [|done]. + destruct uf; simplify_eq/=. + -- eapply nonempty_ctx_mstep with (E := X_Force). + ++ by eapply rtc_once, E_Ctx with (E := id). + ++ by exists X_Force, id, true. + -- apply rtc_once. by eapply E_Ctx with (E := id). + + (* X_Select *) + case_match. simplify_option_eq. + apply IHn in Heqo. simplify_eq/=. + apply rtc_transitive with (y := cforce uf + (X_Select (V_Attrset H0) (Ne_Cons head tail))). + -- apply ctx_mstep + with (E := cforce uf ∘ (λ e, X_Select e (Ne_Cons head tail))). + ++ done. + ++ destruct uf; simplify_option_eq. + ** eapply IsCtx_Compose; [constructor | by apply is_ctx_once]. + ** apply is_ctx_once. unfold compose. by simpl. + -- case_match; apply IHn in Heval. + ++ apply rtc_transitive with (y := cforce uf H); [|done]. + apply rtc_once. + eapply E_Ctx. + ** destruct uf; [by apply is_ctx_once | done]. + ** by replace H0 with (<[head := H]>H0); [|apply insert_id]. + ++ apply rtc_transitive + with (y := cforce uf (X_Select H (Ne_Cons s l))); [|done]. + ** eapply rtc_l. + --- eapply E_Ctx. + +++ destruct uf; [by apply is_ctx_once | done]. + +++ replace (Ne_Cons head (s :: l)) + with (nonempty_cons head (Ne_Cons s l)) by done. + apply E_MSelect. + --- eapply rtc_once. + eapply E_Ctx + with (E := cforce uf ∘ (λ e, X_Select e (Ne_Cons s l))). + +++ destruct uf. + *** eapply IsCtx_Compose; [done | by apply is_ctx_once]. + *** apply is_ctx_once. unfold compose. by simpl. + +++ by replace H0 + with (<[head := H]>H0); [|apply insert_id]. + + (* X_SelectOr *) + case_match. simplify_option_eq. + apply IHn in Heqo. simplify_eq/=. + apply rtc_transitive + with (y := cforce uf (X_SelectOr (V_Attrset H0) (Ne_Cons head tail) e2)). + -- apply ctx_mstep + with (E := cforce uf ∘ (λ e, X_SelectOr e (Ne_Cons head tail) e2)). + ++ done. + ++ destruct uf; simplify_option_eq. + ** eapply IsCtx_Compose; [constructor | by apply is_ctx_once]. + ** apply is_ctx_once. unfold compose. by simpl. + -- case_match; try case_match; apply IHn in Heval. + ++ apply rtc_transitive with (y := cforce uf e); [|done]. + eapply rtc_l. + ** eapply E_Ctx. + --- destruct uf; [by apply is_ctx_once | done]. + --- replace (Ne_Cons head []) with (nonempty_singleton head) + by done. constructor. + ** eapply rtc_l. + --- eapply E_Ctx with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)). + +++ destruct uf; simplify_option_eq. + *** eapply IsCtx_Compose; + [constructor | by apply is_ctx_once]. + *** apply is_ctx_once. unfold compose. by simpl. + +++ by apply E_OpHasAttrTrue. + --- simplify_eq/=. + eapply rtc_l. + +++ eapply E_Ctx with (E := cforce uf). + *** destruct uf; [by apply is_ctx_once | done]. + *** apply E_IfTrue. + +++ eapply rtc_once. + eapply E_Ctx with (E := cforce uf). + *** destruct uf; [by apply is_ctx_once | done]. + *** by replace H0 with (<[head := e]>H0); + [|apply insert_id]. + ++ apply rtc_transitive + with (y := cforce uf (X_SelectOr e (Ne_Cons s l) e2)); [|done]. + eapply rtc_l. + ** eapply E_Ctx. + --- destruct uf; [by apply is_ctx_once | done]. + --- replace (Ne_Cons head (s :: l)) + with (nonempty_cons head (Ne_Cons s l)) by done. + constructor. + ** eapply rtc_l. + --- eapply E_Ctx with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)). + +++ destruct uf; simplify_option_eq. + *** eapply IsCtx_Compose; + [constructor | by apply is_ctx_once]. + *** apply is_ctx_once. unfold compose. by simpl. + +++ by apply E_OpHasAttrTrue. + --- simplify_eq/=. + eapply rtc_l. + +++ eapply E_Ctx with (E := cforce uf). + *** destruct uf; [by apply is_ctx_once | done]. + *** apply E_IfTrue. + +++ eapply rtc_once. + eapply E_Ctx + with (E := cforce uf ∘ λ e1, + X_SelectOr e1 (Ne_Cons s l) e2). + *** destruct uf; simplify_option_eq. + ---- eapply IsCtx_Compose; + [constructor | by apply is_ctx_once]. + ---- apply is_ctx_once. unfold compose. by simpl. + *** by replace H0 with (<[head := e]>H0); + [|apply insert_id]. + ++ apply rtc_transitive with (y := cforce uf e2); [|done]. + destruct tail. + ** eapply rtc_l. + --- eapply E_Ctx. + +++ destruct uf; [by apply is_ctx_once | done]. + +++ replace (Ne_Cons head []) + with (nonempty_singleton head) by done. + constructor. + --- eapply rtc_l. + +++ eapply E_Ctx + with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)). + *** destruct uf; simplify_option_eq. + ---- eapply IsCtx_Compose; + [constructor | by apply is_ctx_once]. + ---- apply is_ctx_once. unfold compose. by simpl. + *** by apply E_OpHasAttrFalse. + +++ simplify_eq/=. + eapply rtc_once. + eapply E_Ctx with (E := cforce uf). + *** destruct uf; [by apply is_ctx_once | done]. + *** apply E_IfFalse. + ** eapply rtc_l. + --- eapply E_Ctx. + +++ destruct uf; [by apply is_ctx_once | done]. + +++ replace (Ne_Cons head (s :: tail)) + with (nonempty_cons head (Ne_Cons s tail)) by done. + constructor. + --- eapply rtc_l. + +++ eapply E_Ctx + with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)). + *** destruct uf; simplify_option_eq. + ---- eapply IsCtx_Compose; + [constructor | by apply is_ctx_once]. + ---- apply is_ctx_once. unfold compose. by simpl. + *** by apply E_OpHasAttrFalse. + +++ simplify_eq/=. + eapply rtc_once. + eapply E_Ctx with (E := cforce uf). + *** destruct uf; [by apply is_ctx_once | done]. + *** apply E_IfFalse. + + (* X_Apply *) + case_match; simplify_option_eq; apply IHn in Heqo, Heval. + * (* Basic lambda abstraction *) + apply rtc_transitive with (y := cforce uf (X_Apply (V_Fn x e) e2)). + -- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2); + [done|]. + destruct uf. + ++ by eapply IsCtx_Compose; [|apply is_ctx_once]. + ++ apply is_ctx_once. unfold compose. by simpl. + -- apply rtc_transitive + with (y := cforce uf (subst {[x := X_Closed e2]} e)); [|done]. + eapply rtc_once. + eapply E_Ctx. + ++ destruct uf; [by apply is_ctx_once | done]. + ++ by constructor. + * (* Pattern-matching function *) + apply rtc_transitive + with (y := cforce uf (X_Apply (V_AttrsetFn m e) e2)). + -- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2); + [done|]. + destruct uf. + ++ by eapply IsCtx_Compose; [|apply is_ctx_once]. + ++ apply is_ctx_once. unfold compose. by simpl. + -- apply rtc_transitive + with (y := cforce uf (X_Apply (V_AttrsetFn m e) (V_Attrset H0))). + ++ apply ctx_mstep + with (E := cforce uf ∘ λ e2, X_Apply (V_AttrsetFn m e) e2). + ** by apply IHn in Heqo0. + ** destruct uf. + --- by eapply IsCtx_Compose; [|apply is_ctx_once]. + --- apply is_ctx_once. unfold compose. by simpl. + ++ apply rtc_transitive with (y := cforce uf (X_LetBinding H e)); + [|done]. + eapply rtc_once. + eapply E_Ctx. + ** destruct uf; [by apply is_ctx_once | done]. + ** apply matches_sound in Heqo1. by constructor. + * (* __functor *) + apply rtc_transitive with (y := cforce uf (X_Apply (V_Attrset bs) e2)). + -- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2); + [done|]. + destruct uf. + ++ by eapply IsCtx_Compose; [|apply is_ctx_once]. + ++ apply is_ctx_once. unfold compose. by simpl. + -- apply rtc_transitive + with (y := cforce uf (X_Apply (X_Apply H (V_Attrset bs)) e2)); + [|done]. + eapply rtc_once. + eapply E_Ctx. + ++ destruct uf; [by apply is_ctx_once | done]. + ++ by replace bs with (<["__functor" := H]>bs); [|apply insert_id]. + + (* X_Cond *) + simplify_option_eq. + apply IHn in Heqo, Heval. + apply rtc_transitive with (y := cforce uf (X_Cond (V_Bool H0) e2 e3)). + * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Cond e1 e2 e3); [done|]. + destruct uf. + -- by eapply IsCtx_Compose; [|apply is_ctx_once]. + -- apply is_ctx_once. unfold compose. by simpl. + * destruct H0; eapply rtc_l; try done; eapply E_Ctx; try done; + by destruct uf; [apply is_ctx_once|]. + + (* X_Incl *) + apply IHn in Heqo. + apply rtc_transitive with (y := cforce uf (X_Incl H e2)). + * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Incl e1 e2). + -- done. + -- destruct uf. + ++ eapply IsCtx_Compose; [done | by apply is_ctx_once]. + ++ unfold compose. apply is_ctx_once. by simpl. + * destruct (decide (attrset H)). + -- destruct H; inv a. simplify_option_eq. apply IHn in Heval. + eapply rtc_l; [|done]. + eapply E_Ctx. + ++ destruct uf; [by apply is_ctx_once | done]. + ++ apply E_With. + -- destruct H; + try (eapply rtc_l; + [ eapply E_Ctx; + [ destruct uf; [by apply is_ctx_once | done] + | by apply E_WithNoAttrset ] + | by apply IHn in Heval ]). + destruct n0. by exists bs. + + (* X_Assert *) + apply IHn in Heqo. + apply rtc_transitive with (y := cforce uf (X_Assert H e2)). + * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Assert e1 e2); [done|]. + destruct uf. + -- by eapply IsCtx_Compose; [|apply is_ctx_once]. + -- unfold compose. apply is_ctx_once. by simpl. + * destruct H; try discriminate. destruct p; try discriminate. + apply IHn in Heval. eapply rtc_l; [|done]. + eapply E_Ctx; [|done]. + by destruct uf; [apply is_ctx_once|]. + + (* X_Binop *) + apply IHn in Heqo, Heqo0. + apply rtc_transitive with (y := cforce uf (X_Op op (X_V H) e2)). + * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Op op e1 e2). + -- done. + -- destruct uf. + ++ eapply IsCtx_Compose; [done | by apply is_ctx_once]. + ++ unfold compose. apply is_ctx_once. by simpl. + * apply rtc_transitive with (y := cforce uf (X_Op op (X_V H) (X_V H0))). + -- apply ctx_mstep with (E := cforce uf ∘ λ e2, X_Op op (X_V H) e2). + ++ done. + ++ destruct uf. + ** eapply IsCtx_Compose; [done | by apply is_ctx_once]. + ** unfold compose. apply is_ctx_once. by simpl. + -- eapply rtc_l. + ++ eapply E_Ctx with (E := cforce uf). + ** destruct uf; [by apply is_ctx_once | done]. + ** apply E_Op. by apply binop_eval_sound. + ++ by apply IHn. + + (* X_HasAttr *) + apply IHn in Heqo. + apply rtc_transitive with (y := cforce uf (X_HasAttr H x)). + * apply ctx_mstep with (E := cforce uf ∘ λ e, X_HasAttr e x); [done|]. + destruct uf. + -- by eapply IsCtx_Compose; [|apply is_ctx_once]. + -- unfold compose. apply is_ctx_once. by simpl. + * destruct (decide (attrset H)). + -- case_match; inv a. simplify_option_eq. + apply rtc_transitive + with (y := cforce uf (bool_decide (is_Some (x0 !! x)))). + ++ apply rtc_once. eapply E_Ctx. + ** destruct uf; [by apply is_ctx_once | done]. + ** destruct (decide (is_Some (x0 !! x))). + --- rewrite bool_decide_true by done. by constructor. + --- rewrite bool_decide_false by done. constructor. + by apply eq_None_not_Some in n0. + ++ destruct uf; [|done]. + apply rtc_once. simpl. + replace (V_Bool (bool_decide (is_Some (x0 !! x)))) + with (value_from_strong_value + (SV_Bool (bool_decide (is_Some (x0 !! x))))) + by done. + by eapply E_Ctx with (E := id). + -- apply rtc_transitive with (y := cforce uf false). + ++ apply rtc_once. eapply E_Ctx. + ** destruct uf; [by apply is_ctx_once | done]. + ** by constructor. + ++ assert (Hforce : cforce true false -->* false). + { apply rtc_once. + simpl. + replace (V_Bool false) + with (value_from_strong_value (SV_Bool false)) by done. + eapply E_Ctx with (E := id); done. } + destruct H; try (by destruct uf; [apply Hforce | done]). + exfalso. apply n0. by exists bs. + + (* X_Force *) + apply IHn in Heval. clear IHn n. + destruct uf; try done. simplify_eq/=. + by apply force_idempotent. + + (* X_Closed *) + apply IHn in Heval. + eapply rtc_l; [|done]. + eapply E_Ctx; [|done]. + * by destruct uf; [apply is_ctx_once|]. + + (* X_Placeholder *) + apply IHn in Heval. clear IHn n. + destruct uf; simplify_eq/=; eapply rtc_l; try done. + -- eapply E_Ctx with (E := X_Force); [by apply is_ctx_once | done]. + -- by eapply E_Ctx with (E := id). +Qed. + +Lemma value_stuck v : ¬ ∃ e', X_V v --> e'. +Proof. + induction v; intros [e' He']; inversion He'; + subst; (inv H0; [inv H1 | inv H2]). +Qed. + +Theorem eval_sound_weak e v' n : eval n false e = Some v' → is_nf_of step e v'. +Proof. + intros Heval. + pose proof (eval_sound_strong _ _ _ _ Heval). + split; [done | apply value_stuck]. +Qed. -- cgit v1.2.3