From 285fc8bab221d010ff2c425dc79f9ff4cc4704ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Tue, 9 Jun 2026 21:37:17 +0200 Subject: [PATCH 01/11] Engine: define NoPriority Semantics --- Engine/NoPrioSemantics.v | 75 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 Engine/NoPrioSemantics.v diff --git a/Engine/NoPrioSemantics.v b/Engine/NoPrioSemantics.v new file mode 100644 index 0000000..f9edc6b --- /dev/null +++ b/Engine/NoPrioSemantics.v @@ -0,0 +1,75 @@ +From Stdlib Require Import List Lia. +Import ListNotations. + +From Linden Require Import Regex Chars Groups. +From Linden Require Import Tree Semantics PikeSubset. +From Warblre Require Import Base RegExpRecord. +From Linden Require Import StrictSuffix. +From Linden Require Import FunctionalSemantics. +From Linden Require Import ComputeIsTree. +From Linden Require Import Parameters. + + +(* A rephrasing of the semantics, where priority does not matter *) +(* It's a relation about leaves, not necessarily the first one *) +(* There are no actions, the shape of the regex determines the relation *) + +Section NoPrioSemantics. + Context {params: LindenParameters}. + Context (rer: RegExpRecord). + + Inductive noprio: input -> group_map -> regex -> input -> group_map -> Prop := + | np_eps: + forall inp gm, + noprio inp gm Epsilon inp gm + | np_char: + forall inp gm cd c nextinp + (READ: read_char rer cd inp forward = Some (c, nextinp)), + noprio inp gm (Regex.Character cd) nextinp gm + | np_disj_left: + forall inp gm r1 r2 nextinp nextgm + (LEFT: noprio inp gm r1 nextinp nextgm), + noprio inp gm (Disjunction r1 r2) nextinp nextgm + | np_disj_right: + forall inp gm r1 r2 nextinp nextgm + (RIGHT: noprio inp gm r2 nextinp nextgm), + noprio inp gm (Disjunction r1 r2) nextinp nextgm + | np_seq: + forall inp0 gm0 r1 r2 inp1 gm1 inp2 gm2 + (SEQ1: noprio inp0 gm0 r1 inp1 gm1) + (SEQ2: noprio inp1 gm1 r2 inp2 gm2), + noprio inp0 gm0 (Sequence r1 r2) inp2 gm2 + | np_quant_forced: + forall inp0 gm0 r gidl min delta greedy inp1 gm1 inp2 gm2 + (RESET: gidl = def_groups r) + (ITER: noprio inp0 (GroupMap.reset gidl gm0) r inp1 gm1) + (LOOP: noprio inp1 gm1 (Quantified greedy min delta r) inp2 gm2), + noprio inp0 gm0 (Quantified greedy (S min) delta r) inp2 gm2 + | np_quant_done: + forall inp gm r greedy, + noprio inp gm (Quantified greedy 0 (NoI.N 0) r) inp gm + | np_quant_free: + forall inp0 gm0 r greedy delta gidl inp1 gm1 inp2 gm2 + (RESET: gidl = def_groups r) + (ITER: noprio inp0 (GroupMap.reset gidl gm0) r inp1 gm1) + (PROGRESS: strict_suffix inp1 inp0 forward) + (LOOP: noprio inp1 gm1 (Quantified greedy 0 delta r) inp2 gm2), + noprio inp0 gm0 (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp2 gm2 + | np_group: + forall inp gm r gid nextinp nextgm + (GROUP: noprio inp (GroupMap.open (idx inp) gid gm) r nextinp nextgm), + noprio inp gm (Group gid r) nextinp (GroupMap.close (idx nextinp) gid nextgm) + | np_anchor: + forall inp gm a + (ANCHOR: anchor_satisfied rer a inp = true), + noprio inp gm (Anchor a) inp gm. + + (* LATER: there will be an issue if we want to add negative lookarounds: strict positivity *) + (* We might want to declare an oracle version of this, since this reversal is used in engines when we already know about the values of deeper lookarounds. *) + + + (** * NoPrio Tree Equivalence *) + + (* TODO *) + +End NoPrioSemantics. From b2b2c42ebf9db8cc74736857e7d72fb4ee3c607b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Tue, 9 Jun 2026 23:44:30 +0200 Subject: [PATCH 02/11] Engine: prove that noprio implies being a leaf --- Engine/NoPrioSemantics.v | 135 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 133 insertions(+), 2 deletions(-) diff --git a/Engine/NoPrioSemantics.v b/Engine/NoPrioSemantics.v index f9edc6b..c1814ee 100644 --- a/Engine/NoPrioSemantics.v +++ b/Engine/NoPrioSemantics.v @@ -8,6 +8,7 @@ From Linden Require Import StrictSuffix. From Linden Require Import FunctionalSemantics. From Linden Require Import ComputeIsTree. From Linden Require Import Parameters. +From Linden Require Import FlatMap Equivalence FunctionalUtils. (* A rephrasing of the semantics, where priority does not matter *) @@ -55,6 +56,9 @@ Section NoPrioSemantics. (PROGRESS: strict_suffix inp1 inp0 forward) (LOOP: noprio inp1 gm1 (Quantified greedy 0 delta r) inp2 gm2), noprio inp0 gm0 (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp2 gm2 + | np_quant_skip: + forall inp gm r greedy delta, + noprio inp gm (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp gm | np_group: forall inp gm r gid nextinp nextgm (GROUP: noprio inp (GroupMap.open (idx inp) gid gm) r nextinp nextgm), @@ -69,7 +73,134 @@ Section NoPrioSemantics. (** * NoPrio Tree Equivalence *) - - (* TODO *) + Lemma two_app: + forall A (a1 a2:A), [a1; a2] = [a1] ++ [a2]. + Proof. auto. Qed. + + Lemma three_app: + forall A (a1 a2 a3:A), [a1; a2; a3] = [a1] ++ [a2] ++ [a3]. + Proof. auto. Qed. + + (* If we can find a leaf in the tree of the first list of actions, + then a leaf in the tree of the second list, + then that final leaf is a leaf of the tree of the concatenation *) + Lemma in_leaves_app: + forall inp0 gm0 inp1 gm1 inp2 gm2 a1 a2 t1 t2 t12 + (TREE12: is_tree rer (a1 ++ a2) inp0 gm0 forward t12) + (TREE1: is_tree rer a1 inp0 gm0 forward t1) + (TREE2: is_tree rer a2 inp1 gm1 forward t2) + (IN1: In (inp1,gm1) (tree_leaves t1 gm0 inp0 forward)) + (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 forward)), + In (inp2, gm2) (tree_leaves t12 gm0 inp0 forward). + Proof. + intros inp0 gm0 inp1 gm1 inp2 gm2 a1 a2 t1 t2 t12 TREE12 TREE1 TREE2 IN1 IN2. + specialize (leaves_concat _ _ _ _ _ _ _ _ TREE12 TREE1) as FM. + assert (ACT: act_from_leaf rer a2 forward (inp1, gm1) (tree_leaves t2 gm1 inp1 forward)). + { constructor. simpl. auto. } + specialize (FlatMap_in _ _ _ _ _ (act_from_leaf_determ _ _ _) FM IN1 ACT) as FM_IN. + rewrite Forall_forall in FM_IN. + apply FM_IN. auto. + Qed. + + Lemma in_leaves_app3: + forall inp0 gm0 inp1 gm1 inp2 gm2 inp3 gm3 a1 a2 a3 t1 t2 t3 t123 + (TREE123: is_tree rer (a1 ++ a2 ++ a3) inp0 gm0 forward t123) + (TREE1: is_tree rer a1 inp0 gm0 forward t1) + (TREE2: is_tree rer a2 inp1 gm1 forward t2) + (TREE3: is_tree rer a3 inp2 gm2 forward t3) + (IN1: In (inp1,gm1) (tree_leaves t1 gm0 inp0 forward)) + (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 forward)) + (IN3: In (inp3, gm3) (tree_leaves t3 gm2 inp2 forward)), + In (inp3, gm3) (tree_leaves t123 gm0 inp0 forward). + Proof. + intros inp0 gm0 inp1 gm1 inp2 gm2 inp3 gm3 a1 a2 a3 t1 t2 t3 t123 TREE123 TREE1 TREE2 TREE3 IN1 IN2 IN3. + specialize (is_tree_productivity rer (a2 ++ a3) inp1 gm1 forward) as [t23 TREE23]. + assert (IN23: In (inp3, gm3) (tree_leaves t23 gm1 inp1 forward)). + { apply (in_leaves_app _ _ _ _ _ _ _ _ _ _ _ TREE23 TREE2 TREE3 IN2 IN3). } + apply (in_leaves_app _ _ _ _ _ _ _ _ _ _ _ TREE123 TREE1 TREE23 IN1 IN23). + Qed. + + (* all leaves obtained from noprio are leaves of the backtracking tree *) + Theorem noprio_is_leaf: + forall r inp gm t leafinp leafgm + (TREE: is_tree rer [Areg r] inp gm forward t), + noprio inp gm r leafinp leafgm -> + In (leafinp, leafgm) (tree_leaves t gm inp forward). + Proof. + intros r inp gm t leafinp leafgm TREE NP. + generalize dependent t. + induction NP; intros. + - inversion TREE; subst. inversion ISTREE; subst. + simpl. auto. + - inversion TREE; subst; + rewrite READ0 in READ; inversion READ; subst. + inversion TREECONT; subst. simpl. + apply read_char_success_advance in READ0. + unfold advance_input'. rewrite READ0. auto. + - inversion TREE; subst. apply IHNP in ISTREE1. + simpl. apply in_or_app. auto. + - inversion TREE; subst. apply IHNP in ISTREE2. + simpl. apply in_or_app. auto. + - inversion TREE; subst. + simpl in CONT. rewrite two_app in CONT. + specialize (is_tree_productivity rer [Areg r1] inp0 gm0 forward) as [t1 HT1]. + specialize (is_tree_productivity rer [Areg r2] inp1 gm1 forward) as [t2 HT2]. + eapply in_leaves_app; eauto. + - inversion TREE; subst. + rewrite two_app in ISTREE1. + specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm0) forward) as [t1 HT1]. + specialize (is_tree_productivity rer [Areg (Quantified greedy min delta r)] inp1 gm1 forward) as [t2 HT2]. + assert (IN1: In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm0) inp0 forward)). + { apply IHNP1. auto. } + assert (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 forward)). + { apply IHNP2. auto. } + eapply (in_leaves_app _ _ _ _ inp2 gm2 _ _ _ _ _ ISTREE1 HT1 HT2 IN1 IN2); eauto. + - inversion TREE; subst. + + inversion SKIP; subst. simpl. auto. + + destruct plus; inversion H1. + - inversion TREE; subst. + { destruct delta; inversion H1. } + assert (DP: plus = delta). + { destruct plus; destruct delta; auto; inversion H1; auto. } + subst. clear H1. clear SKIP. + specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm0) forward) as [t1 HT1]. + specialize (is_tree_productivity rer [Acheck inp0] inp1 gm1 forward) as [t2 HT2]. + specialize (is_tree_productivity rer [Areg (Quantified greedy 0 delta r)] inp1 gm1 forward) as [t3 HT3]. + assert (IN1: In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm0) inp0 forward)). + { apply IHNP1. auto. } + assert (IN2: In (inp1, gm1) (tree_leaves t2 gm1 inp1 forward)). + { inversion HT2; subst. + - inversion TREECONT; subst. simpl. auto. + - apply CHECKFAIL in PROGRESS. inversion PROGRESS. (* we know progress happened *) + } + assert (IN3: In (inp2, gm2) (tree_leaves t3 gm1 inp1 forward)). + { apply IHNP2. auto. } + rewrite three_app in ISTREE1. + destruct greedy; simpl. + + apply in_or_app. left. + eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). + + apply in_or_app. right. + eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). + - inversion TREE; subst. + { destruct delta; inversion H1. } + inversion SKIP. subst. + destruct greedy; simpl; auto. + apply in_or_app; simpl; auto. + - inversion TREE; subst. + rewrite two_app in TREECONT. + specialize (is_tree_productivity rer [Areg r] inp (GroupMap.open (idx inp) gid gm) forward) as [t1 HT1]. + specialize (is_tree_productivity rer [Aclose gid] nextinp nextgm forward) as [t2 HT2]. + assert (IN1: In (nextinp, nextgm) (tree_leaves t1 (GroupMap.open (idx inp) gid gm) inp forward)). + { apply IHNP. auto. } + assert (IN2: In (nextinp, GroupMap.close (idx nextinp) gid nextgm) (tree_leaves t2 nextgm nextinp forward)). + { inversion HT2. subst. inversion TREECONT0. subst. simpl. auto. } + eapply (in_leaves_app _ _ _ _ nextinp (GroupMap.close (idx nextinp) gid nextgm) _ _ _ _ _ TREECONT HT1 HT2 IN1 IN2); eauto. + - inversion TREE; subst; + rewrite ANCHOR0 in ANCHOR; inversion ANCHOR. + inversion TREECONT; subst. simpl. auto. + Qed. + + (* LATER: other direction *) + End NoPrioSemantics. From 315521af757a83e6781818eddd45afdf041e3147 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Wed, 10 Jun 2026 13:23:29 +0200 Subject: [PATCH 03/11] Engine: finish the proof of equivalence between nopriority semantics and leaves of tree semantics --- Engine/NoPrioSemantics.v | 108 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 107 insertions(+), 1 deletion(-) diff --git a/Engine/NoPrioSemantics.v b/Engine/NoPrioSemantics.v index c1814ee..e9c3a38 100644 --- a/Engine/NoPrioSemantics.v +++ b/Engine/NoPrioSemantics.v @@ -201,6 +201,112 @@ Section NoPrioSemantics. inversion TREECONT; subst. simpl. auto. Qed. - (* LATER: other direction *) + (* Other direction: generalizing the noprio semantics to actions *) + + Inductive noprio_action: input -> group_map -> action -> input -> group_map -> Prop := + | np_regex: + forall inp gm r nextinp nextgm + (NP: noprio inp gm r nextinp nextgm), + noprio_action inp gm (Areg r) nextinp nextgm + | np_close: + forall inp gm gid, + noprio_action inp gm (Aclose gid) inp (GroupMap.close (idx inp) gid gm) + | np_check: + forall inp gm inpcheck + (PROGRESS: strict_suffix inp inpcheck forward), + noprio_action inp gm (Acheck inpcheck) inp gm. + + Inductive noprio_list: input -> group_map -> list action -> input -> group_map -> Prop := + | np_nil: + forall inp gm, + noprio_list inp gm [] inp gm + | np_cons: + forall inp0 gm0 a inp1 gm1 l inp2 gm2 + (NP_A: noprio_action inp0 gm0 a inp1 gm1) + (NP_L: noprio_list inp1 gm1 l inp2 gm2), + noprio_list inp0 gm0 (a::l) inp2 gm2. + + Lemma is_tree_action_noprio: + forall inp0 gm0 l t inp1 gm1 + (SUBSET: pike_actions l) + (TREE: is_tree rer l inp0 gm0 forward t) + (LEAF: In (inp1, gm1) (tree_leaves t gm0 inp0 forward)), + noprio_list inp0 gm0 l inp1 gm1. + Proof. + intros inp0 gm0 l t inp1 gm1 SUBSET TREE LEAF. + remember forward as dir. + induction TREE; simpl in LEAF; subst; + try solve [inversion LEAF]; pike_subset. + - destruct LEAF as [LEAF|LEAF]; inversion LEAF; subst. constructor. + - repeat (econstructor; eauto). + - repeat (econstructor; eauto). + - repeat (econstructor; eauto). + - econstructor; eauto. + 2: { apply read_char_success_advance in READ as ADV. + unfold advance_input' in LEAF. rewrite ADV in LEAF. eauto. } + repeat (econstructor; eauto). + - apply in_app_or in LEAF as [LEAF|LEAF]. + + assert (noprio_list inp gm (Areg r1::cont) inp1 gm1). + { apply IHTREE1; auto. pike_subset. } + inversion H; subst. inversion NP_A. repeat (econstructor; eauto). + + assert (noprio_list inp gm (Areg r2::cont) inp1 gm1). + { apply IHTREE2; auto. pike_subset. } + inversion H; subst. inversion NP_A. solve[repeat (econstructor; eauto)]. + - simpl in IHTREE. + assert (noprio_list inp gm (Areg r1 :: Areg r2 :: cont) inp1 gm1). + { apply IHTREE; auto. pike_subset. } + inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; subst. + repeat (econstructor; eauto). + - specialize (IHTREE H2 (eq_refl _) LEAF). + repeat econstructor; eauto. + - destruct plus; inversion H3; subst. + specialize (IHTREE2 H2 (eq_refl _)). + assert (In (inp1,gm1) (tree_leaves titer (GroupMap.reset (def_groups r1) gm) inp forward) \/ + In (inp1,gm1) (tree_leaves tskip gm inp forward)) as [LEAFSKIP|LEAFITER]. + { destruct greedy; simpl in LEAF; apply in_app_or in LEAF; auto. + destruct LEAF; auto. } + (* skip *) + 2: { econstructor; eauto. econstructor; eauto. apply np_quant_skip. } + (* iter *) + assert (noprio_list inp (GroupMap.reset (def_groups r1) gm) (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 +∞ r1) :: cont) inp1 gm1). + { apply IHTREE1; auto. pike_subset. } + inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; inversion NP_L0; inversion NP_A1; subst. + repeat (econstructor; eauto). + - destruct plus; inversion H3. subst. + specialize (IHTREE2 H2 (eq_refl _)). + assert (In (inp1,gm1) (tree_leaves titer (GroupMap.reset (def_groups r1) gm) inp forward) \/ + In (inp1,gm1) (tree_leaves tskip gm inp forward)) as [LEAFSKIP|LEAFITER]. + { destruct greedy; simpl in LEAF; apply in_app_or in LEAF; auto. + destruct LEAF; auto. } + (* skip *) + 2: { econstructor; eauto. econstructor; eauto. apply np_quant_skip. } + (* iter *) + assert (noprio_list inp (GroupMap.reset (def_groups r1) gm) (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 (NoI.N 0) r1) :: cont) inp1 gm1). + { apply IHTREE1; auto. pike_subset. } + inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; inversion NP_L0; inversion NP_A1; subst. + repeat (econstructor; eauto). + - destruct plus; inversion H3. + - assert (noprio_list inp (GroupMap.open (idx inp) gid gm) (Areg r1 :: Aclose gid :: cont) inp1 gm1). + { apply IHTREE; auto. pike_subset. } + inversion H; inversion NP_A; inversion NP_L; inversion NP_A0; subst. + repeat (econstructor; eauto). + - specialize (IHTREE H2 (eq_refl _) LEAF). + repeat (econstructor; eauto). + Qed. + + (* For the Pike Subset, the NoPrio Semantics exactly coincides with leaves of the Tree Semantics *) + Theorem noprio_eq_is_leaf: + forall r inp gm t leafinp leafgm + (SUBSET: pike_regex r) + (TREE: is_tree rer [Areg r] inp gm forward t), + noprio inp gm r leafinp leafgm <-> + In (leafinp, leafgm) (tree_leaves t gm inp forward). + Proof. + intros r inp gm t leafinp leafgm SUBSET TREE. split. + - apply noprio_is_leaf. auto. + - intros. eapply is_tree_action_noprio in TREE; eauto. + 2: pike_subset. + inversion TREE; inversion NP_A; inversion NP_L; subst. auto. + Qed. End NoPrioSemantics. From 4d7dc471f520c37c121f2a8c123137ed401f3aa8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Wed, 10 Jun 2026 16:42:02 +0200 Subject: [PATCH 04/11] Engine: add direction to NoPriority semantics --- Engine/NoPrioSemantics.v | 265 +++++++++++++++++++++------------------ 1 file changed, 140 insertions(+), 125 deletions(-) diff --git a/Engine/NoPrioSemantics.v b/Engine/NoPrioSemantics.v index e9c3a38..5676a75 100644 --- a/Engine/NoPrioSemantics.v +++ b/Engine/NoPrioSemantics.v @@ -19,54 +19,59 @@ Section NoPrioSemantics. Context {params: LindenParameters}. Context (rer: RegExpRecord). - Inductive noprio: input -> group_map -> regex -> input -> group_map -> Prop := + Inductive noprio: Direction -> input -> group_map -> regex -> input -> group_map -> Prop := | np_eps: - forall inp gm, - noprio inp gm Epsilon inp gm + forall dir inp gm, + noprio dir inp gm Epsilon inp gm | np_char: - forall inp gm cd c nextinp - (READ: read_char rer cd inp forward = Some (c, nextinp)), - noprio inp gm (Regex.Character cd) nextinp gm + forall dir inp gm cd c nextinp + (READ: read_char rer cd inp dir = Some (c, nextinp)), + noprio dir inp gm (Regex.Character cd) nextinp gm | np_disj_left: - forall inp gm r1 r2 nextinp nextgm - (LEFT: noprio inp gm r1 nextinp nextgm), - noprio inp gm (Disjunction r1 r2) nextinp nextgm + forall dir inp gm r1 r2 nextinp nextgm + (LEFT: noprio dir inp gm r1 nextinp nextgm), + noprio dir inp gm (Disjunction r1 r2) nextinp nextgm | np_disj_right: - forall inp gm r1 r2 nextinp nextgm - (RIGHT: noprio inp gm r2 nextinp nextgm), - noprio inp gm (Disjunction r1 r2) nextinp nextgm - | np_seq: + forall dir inp gm r1 r2 nextinp nextgm + (RIGHT: noprio dir inp gm r2 nextinp nextgm), + noprio dir inp gm (Disjunction r1 r2) nextinp nextgm + | np_seq_forward: forall inp0 gm0 r1 r2 inp1 gm1 inp2 gm2 - (SEQ1: noprio inp0 gm0 r1 inp1 gm1) - (SEQ2: noprio inp1 gm1 r2 inp2 gm2), - noprio inp0 gm0 (Sequence r1 r2) inp2 gm2 + (SEQ1: noprio forward inp0 gm0 r1 inp1 gm1) + (SEQ2: noprio forward inp1 gm1 r2 inp2 gm2), + noprio forward inp0 gm0 (Sequence r1 r2) inp2 gm2 + | np_seq_backward: + forall inp0 gm0 r1 r2 inp1 gm1 inp2 gm2 + (SEQ1: noprio backward inp0 gm0 r2 inp1 gm1) + (SEQ2: noprio backward inp1 gm1 r1 inp2 gm2), + noprio backward inp0 gm0 (Sequence r1 r2) inp2 gm2 | np_quant_forced: - forall inp0 gm0 r gidl min delta greedy inp1 gm1 inp2 gm2 + forall dir inp0 gm0 r gidl min delta greedy inp1 gm1 inp2 gm2 (RESET: gidl = def_groups r) - (ITER: noprio inp0 (GroupMap.reset gidl gm0) r inp1 gm1) - (LOOP: noprio inp1 gm1 (Quantified greedy min delta r) inp2 gm2), - noprio inp0 gm0 (Quantified greedy (S min) delta r) inp2 gm2 + (ITER: noprio dir inp0 (GroupMap.reset gidl gm0) r inp1 gm1) + (LOOP: noprio dir inp1 gm1 (Quantified greedy min delta r) inp2 gm2), + noprio dir inp0 gm0 (Quantified greedy (S min) delta r) inp2 gm2 | np_quant_done: - forall inp gm r greedy, - noprio inp gm (Quantified greedy 0 (NoI.N 0) r) inp gm + forall dir inp gm r greedy, + noprio dir inp gm (Quantified greedy 0 (NoI.N 0) r) inp gm | np_quant_free: - forall inp0 gm0 r greedy delta gidl inp1 gm1 inp2 gm2 + forall dir inp0 gm0 r greedy delta gidl inp1 gm1 inp2 gm2 (RESET: gidl = def_groups r) - (ITER: noprio inp0 (GroupMap.reset gidl gm0) r inp1 gm1) - (PROGRESS: strict_suffix inp1 inp0 forward) - (LOOP: noprio inp1 gm1 (Quantified greedy 0 delta r) inp2 gm2), - noprio inp0 gm0 (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp2 gm2 + (ITER: noprio dir inp0 (GroupMap.reset gidl gm0) r inp1 gm1) + (PROGRESS: strict_suffix inp1 inp0 dir) + (LOOP: noprio dir inp1 gm1 (Quantified greedy 0 delta r) inp2 gm2), + noprio dir inp0 gm0 (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp2 gm2 | np_quant_skip: - forall inp gm r greedy delta, - noprio inp gm (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp gm + forall dir inp gm r greedy delta, + noprio dir inp gm (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp gm | np_group: - forall inp gm r gid nextinp nextgm - (GROUP: noprio inp (GroupMap.open (idx inp) gid gm) r nextinp nextgm), - noprio inp gm (Group gid r) nextinp (GroupMap.close (idx nextinp) gid nextgm) + forall dir inp gm r gid nextinp nextgm + (GROUP: noprio dir inp (GroupMap.open (idx inp) gid gm) r nextinp nextgm), + noprio dir inp gm (Group gid r) nextinp (GroupMap.close (idx nextinp) gid nextgm) | np_anchor: - forall inp gm a + forall dir inp gm a (ANCHOR: anchor_satisfied rer a inp = true), - noprio inp gm (Anchor a) inp gm. + noprio dir inp gm (Anchor a) inp gm. (* LATER: there will be an issue if we want to add negative lookarounds: strict positivity *) (* We might want to declare an oracle version of this, since this reversal is used in engines when we already know about the values of deeper lookarounds. *) @@ -86,17 +91,17 @@ Section NoPrioSemantics. then a leaf in the tree of the second list, then that final leaf is a leaf of the tree of the concatenation *) Lemma in_leaves_app: - forall inp0 gm0 inp1 gm1 inp2 gm2 a1 a2 t1 t2 t12 - (TREE12: is_tree rer (a1 ++ a2) inp0 gm0 forward t12) - (TREE1: is_tree rer a1 inp0 gm0 forward t1) - (TREE2: is_tree rer a2 inp1 gm1 forward t2) - (IN1: In (inp1,gm1) (tree_leaves t1 gm0 inp0 forward)) - (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 forward)), - In (inp2, gm2) (tree_leaves t12 gm0 inp0 forward). + forall dir inp0 gm0 inp1 gm1 inp2 gm2 a1 a2 t1 t2 t12 + (TREE12: is_tree rer (a1 ++ a2) inp0 gm0 dir t12) + (TREE1: is_tree rer a1 inp0 gm0 dir t1) + (TREE2: is_tree rer a2 inp1 gm1 dir t2) + (IN1: In (inp1,gm1) (tree_leaves t1 gm0 inp0 dir)) + (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 dir)), + In (inp2, gm2) (tree_leaves t12 gm0 inp0 dir). Proof. - intros inp0 gm0 inp1 gm1 inp2 gm2 a1 a2 t1 t2 t12 TREE12 TREE1 TREE2 IN1 IN2. + intros dir inp0 gm0 inp1 gm1 inp2 gm2 a1 a2 t1 t2 t12 TREE12 TREE1 TREE2 IN1 IN2. specialize (leaves_concat _ _ _ _ _ _ _ _ TREE12 TREE1) as FM. - assert (ACT: act_from_leaf rer a2 forward (inp1, gm1) (tree_leaves t2 gm1 inp1 forward)). + assert (ACT: act_from_leaf rer a2 dir (inp1, gm1) (tree_leaves t2 gm1 inp1 dir)). { constructor. simpl. auto. } specialize (FlatMap_in _ _ _ _ _ (act_from_leaf_determ _ _ _) FM IN1 ACT) as FM_IN. rewrite Forall_forall in FM_IN. @@ -104,31 +109,31 @@ Section NoPrioSemantics. Qed. Lemma in_leaves_app3: - forall inp0 gm0 inp1 gm1 inp2 gm2 inp3 gm3 a1 a2 a3 t1 t2 t3 t123 - (TREE123: is_tree rer (a1 ++ a2 ++ a3) inp0 gm0 forward t123) - (TREE1: is_tree rer a1 inp0 gm0 forward t1) - (TREE2: is_tree rer a2 inp1 gm1 forward t2) - (TREE3: is_tree rer a3 inp2 gm2 forward t3) - (IN1: In (inp1,gm1) (tree_leaves t1 gm0 inp0 forward)) - (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 forward)) - (IN3: In (inp3, gm3) (tree_leaves t3 gm2 inp2 forward)), - In (inp3, gm3) (tree_leaves t123 gm0 inp0 forward). + forall dir inp0 gm0 inp1 gm1 inp2 gm2 inp3 gm3 a1 a2 a3 t1 t2 t3 t123 + (TREE123: is_tree rer (a1 ++ a2 ++ a3) inp0 gm0 dir t123) + (TREE1: is_tree rer a1 inp0 gm0 dir t1) + (TREE2: is_tree rer a2 inp1 gm1 dir t2) + (TREE3: is_tree rer a3 inp2 gm2 dir t3) + (IN1: In (inp1,gm1) (tree_leaves t1 gm0 inp0 dir)) + (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 dir)) + (IN3: In (inp3, gm3) (tree_leaves t3 gm2 inp2 dir)), + In (inp3, gm3) (tree_leaves t123 gm0 inp0 dir). Proof. - intros inp0 gm0 inp1 gm1 inp2 gm2 inp3 gm3 a1 a2 a3 t1 t2 t3 t123 TREE123 TREE1 TREE2 TREE3 IN1 IN2 IN3. - specialize (is_tree_productivity rer (a2 ++ a3) inp1 gm1 forward) as [t23 TREE23]. - assert (IN23: In (inp3, gm3) (tree_leaves t23 gm1 inp1 forward)). - { apply (in_leaves_app _ _ _ _ _ _ _ _ _ _ _ TREE23 TREE2 TREE3 IN2 IN3). } - apply (in_leaves_app _ _ _ _ _ _ _ _ _ _ _ TREE123 TREE1 TREE23 IN1 IN23). + intros dir inp0 gm0 inp1 gm1 inp2 gm2 inp3 gm3 a1 a2 a3 t1 t2 t3 t123 TREE123 TREE1 TREE2 TREE3 IN1 IN2 IN3. + specialize (is_tree_productivity rer (a2 ++ a3) inp1 gm1 dir) as [t23 TREE23]. + assert (IN23: In (inp3, gm3) (tree_leaves t23 gm1 inp1 dir)). + { apply (in_leaves_app _ _ _ _ _ _ _ _ _ _ _ _ TREE23 TREE2 TREE3 IN2 IN3). } + apply (in_leaves_app _ _ _ _ _ _ _ _ _ _ _ _ TREE123 TREE1 TREE23 IN1 IN23). Qed. (* all leaves obtained from noprio are leaves of the backtracking tree *) Theorem noprio_is_leaf: - forall r inp gm t leafinp leafgm - (TREE: is_tree rer [Areg r] inp gm forward t), - noprio inp gm r leafinp leafgm -> - In (leafinp, leafgm) (tree_leaves t gm inp forward). + forall dir r inp gm t leafinp leafgm + (TREE: is_tree rer [Areg r] inp gm dir t), + noprio dir inp gm r leafinp leafgm -> + In (leafinp, leafgm) (tree_leaves t gm inp dir). Proof. - intros r inp gm t leafinp leafgm TREE NP. + intros dir r inp gm t leafinp leafgm TREE NP. generalize dependent t. induction NP; intros. - inversion TREE; subst. inversion ISTREE; subst. @@ -147,15 +152,20 @@ Section NoPrioSemantics. specialize (is_tree_productivity rer [Areg r1] inp0 gm0 forward) as [t1 HT1]. specialize (is_tree_productivity rer [Areg r2] inp1 gm1 forward) as [t2 HT2]. eapply in_leaves_app; eauto. + - inversion TREE; subst. + simpl in CONT. rewrite two_app in CONT. + specialize (is_tree_productivity rer [Areg r2] inp0 gm0 backward) as [t1 HT1]. + specialize (is_tree_productivity rer [Areg r1] inp1 gm1 backward) as [t2 HT2]. + eapply in_leaves_app; eauto. - inversion TREE; subst. rewrite two_app in ISTREE1. - specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm0) forward) as [t1 HT1]. - specialize (is_tree_productivity rer [Areg (Quantified greedy min delta r)] inp1 gm1 forward) as [t2 HT2]. - assert (IN1: In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm0) inp0 forward)). + specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm0) dir) as [t1 HT1]. + specialize (is_tree_productivity rer [Areg (Quantified greedy min delta r)] inp1 gm1 dir) as [t2 HT2]. + assert (IN1: In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm0) inp0 dir)). { apply IHNP1. auto. } - assert (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 forward)). + assert (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 dir)). { apply IHNP2. auto. } - eapply (in_leaves_app _ _ _ _ inp2 gm2 _ _ _ _ _ ISTREE1 HT1 HT2 IN1 IN2); eauto. + eapply (in_leaves_app _ _ _ _ _ inp2 gm2 _ _ _ _ _ ISTREE1 HT1 HT2 IN1 IN2); eauto. - inversion TREE; subst. + inversion SKIP; subst. simpl. auto. + destruct plus; inversion H1. @@ -164,24 +174,24 @@ Section NoPrioSemantics. assert (DP: plus = delta). { destruct plus; destruct delta; auto; inversion H1; auto. } subst. clear H1. clear SKIP. - specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm0) forward) as [t1 HT1]. - specialize (is_tree_productivity rer [Acheck inp0] inp1 gm1 forward) as [t2 HT2]. - specialize (is_tree_productivity rer [Areg (Quantified greedy 0 delta r)] inp1 gm1 forward) as [t3 HT3]. - assert (IN1: In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm0) inp0 forward)). + specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm0) dir) as [t1 HT1]. + specialize (is_tree_productivity rer [Acheck inp0] inp1 gm1 dir) as [t2 HT2]. + specialize (is_tree_productivity rer [Areg (Quantified greedy 0 delta r)] inp1 gm1 dir) as [t3 HT3]. + assert (IN1: In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm0) inp0 dir)). { apply IHNP1. auto. } - assert (IN2: In (inp1, gm1) (tree_leaves t2 gm1 inp1 forward)). + assert (IN2: In (inp1, gm1) (tree_leaves t2 gm1 inp1 dir)). { inversion HT2; subst. - inversion TREECONT; subst. simpl. auto. - apply CHECKFAIL in PROGRESS. inversion PROGRESS. (* we know progress happened *) } - assert (IN3: In (inp2, gm2) (tree_leaves t3 gm1 inp1 forward)). + assert (IN3: In (inp2, gm2) (tree_leaves t3 gm1 inp1 dir)). { apply IHNP2. auto. } rewrite three_app in ISTREE1. destruct greedy; simpl. + apply in_or_app. left. - eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). + eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). + apply in_or_app. right. - eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). + eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). - inversion TREE; subst. { destruct delta; inversion H1. } inversion SKIP. subst. @@ -189,13 +199,13 @@ Section NoPrioSemantics. apply in_or_app; simpl; auto. - inversion TREE; subst. rewrite two_app in TREECONT. - specialize (is_tree_productivity rer [Areg r] inp (GroupMap.open (idx inp) gid gm) forward) as [t1 HT1]. - specialize (is_tree_productivity rer [Aclose gid] nextinp nextgm forward) as [t2 HT2]. - assert (IN1: In (nextinp, nextgm) (tree_leaves t1 (GroupMap.open (idx inp) gid gm) inp forward)). + specialize (is_tree_productivity rer [Areg r] inp (GroupMap.open (idx inp) gid gm) dir) as [t1 HT1]. + specialize (is_tree_productivity rer [Aclose gid] nextinp nextgm dir) as [t2 HT2]. + assert (IN1: In (nextinp, nextgm) (tree_leaves t1 (GroupMap.open (idx inp) gid gm) inp dir)). { apply IHNP. auto. } - assert (IN2: In (nextinp, GroupMap.close (idx nextinp) gid nextgm) (tree_leaves t2 nextgm nextinp forward)). + assert (IN2: In (nextinp, GroupMap.close (idx nextinp) gid nextgm) (tree_leaves t2 nextgm nextinp dir)). { inversion HT2. subst. inversion TREECONT0. subst. simpl. auto. } - eapply (in_leaves_app _ _ _ _ nextinp (GroupMap.close (idx nextinp) gid nextgm) _ _ _ _ _ TREECONT HT1 HT2 IN1 IN2); eauto. + eapply (in_leaves_app _ _ _ _ _ nextinp (GroupMap.close (idx nextinp) gid nextgm) _ _ _ _ _ TREECONT HT1 HT2 IN1 IN2); eauto. - inversion TREE; subst; rewrite ANCHOR0 in ANCHOR; inversion ANCHOR. inversion TREECONT; subst. simpl. auto. @@ -203,38 +213,37 @@ Section NoPrioSemantics. (* Other direction: generalizing the noprio semantics to actions *) - Inductive noprio_action: input -> group_map -> action -> input -> group_map -> Prop := + Inductive noprio_action: Direction -> input -> group_map -> action -> input -> group_map -> Prop := | np_regex: - forall inp gm r nextinp nextgm - (NP: noprio inp gm r nextinp nextgm), - noprio_action inp gm (Areg r) nextinp nextgm + forall dir inp gm r nextinp nextgm + (NP: noprio dir inp gm r nextinp nextgm), + noprio_action dir inp gm (Areg r) nextinp nextgm | np_close: - forall inp gm gid, - noprio_action inp gm (Aclose gid) inp (GroupMap.close (idx inp) gid gm) + forall dir inp gm gid, + noprio_action dir inp gm (Aclose gid) inp (GroupMap.close (idx inp) gid gm) | np_check: - forall inp gm inpcheck - (PROGRESS: strict_suffix inp inpcheck forward), - noprio_action inp gm (Acheck inpcheck) inp gm. + forall dir inp gm inpcheck + (PROGRESS: strict_suffix inp inpcheck dir), + noprio_action dir inp gm (Acheck inpcheck) inp gm. - Inductive noprio_list: input -> group_map -> list action -> input -> group_map -> Prop := + Inductive noprio_list: Direction -> input -> group_map -> list action -> input -> group_map -> Prop := | np_nil: - forall inp gm, - noprio_list inp gm [] inp gm + forall dir inp gm, + noprio_list dir inp gm [] inp gm | np_cons: - forall inp0 gm0 a inp1 gm1 l inp2 gm2 - (NP_A: noprio_action inp0 gm0 a inp1 gm1) - (NP_L: noprio_list inp1 gm1 l inp2 gm2), - noprio_list inp0 gm0 (a::l) inp2 gm2. + forall dir inp0 gm0 a inp1 gm1 l inp2 gm2 + (NP_A: noprio_action dir inp0 gm0 a inp1 gm1) + (NP_L: noprio_list dir inp1 gm1 l inp2 gm2), + noprio_list dir inp0 gm0 (a::l) inp2 gm2. Lemma is_tree_action_noprio: - forall inp0 gm0 l t inp1 gm1 + forall dir inp0 gm0 l t inp1 gm1 (SUBSET: pike_actions l) - (TREE: is_tree rer l inp0 gm0 forward t) - (LEAF: In (inp1, gm1) (tree_leaves t gm0 inp0 forward)), - noprio_list inp0 gm0 l inp1 gm1. + (TREE: is_tree rer l inp0 gm0 dir t) + (LEAF: In (inp1, gm1) (tree_leaves t gm0 inp0 dir)), + noprio_list dir inp0 gm0 l inp1 gm1. Proof. - intros inp0 gm0 l t inp1 gm1 SUBSET TREE LEAF. - remember forward as dir. + intros dir inp0 gm0 l t inp1 gm1 SUBSET TREE LEAF. induction TREE; simpl in LEAF; subst; try solve [inversion LEAF]; pike_subset. - destruct LEAF as [LEAF|LEAF]; inversion LEAF; subst. constructor. @@ -246,63 +255,69 @@ Section NoPrioSemantics. unfold advance_input' in LEAF. rewrite ADV in LEAF. eauto. } repeat (econstructor; eauto). - apply in_app_or in LEAF as [LEAF|LEAF]. - + assert (noprio_list inp gm (Areg r1::cont) inp1 gm1). + + assert (noprio_list dir inp gm (Areg r1::cont) inp1 gm1). { apply IHTREE1; auto. pike_subset. } inversion H; subst. inversion NP_A. repeat (econstructor; eauto). - + assert (noprio_list inp gm (Areg r2::cont) inp1 gm1). + + assert (noprio_list dir inp gm (Areg r2::cont) inp1 gm1). { apply IHTREE2; auto. pike_subset. } inversion H; subst. inversion NP_A. solve[repeat (econstructor; eauto)]. - - simpl in IHTREE. - assert (noprio_list inp gm (Areg r1 :: Areg r2 :: cont) inp1 gm1). - { apply IHTREE; auto. pike_subset. } - inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; subst. - repeat (econstructor; eauto). - - specialize (IHTREE H2 (eq_refl _) LEAF). + - destruct dir. + + simpl in IHTREE. + assert (noprio_list forward inp gm (Areg r1 :: Areg r2 :: cont) inp1 gm1). + { apply IHTREE; auto. pike_subset. } + inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; subst. + repeat (econstructor; eauto). + + simpl in IHTREE. + assert (noprio_list backward inp gm (Areg r2 :: Areg r1 :: cont) inp1 gm1). + { apply IHTREE; auto. pike_subset. } + inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; subst. + repeat (econstructor; eauto). + - specialize (IHTREE H2 LEAF). repeat econstructor; eauto. - destruct plus; inversion H3; subst. - specialize (IHTREE2 H2 (eq_refl _)). - assert (In (inp1,gm1) (tree_leaves titer (GroupMap.reset (def_groups r1) gm) inp forward) \/ - In (inp1,gm1) (tree_leaves tskip gm inp forward)) as [LEAFSKIP|LEAFITER]. + specialize (IHTREE2 H2). + assert (In (inp1,gm1) (tree_leaves titer (GroupMap.reset (def_groups r1) gm) inp dir) \/ + In (inp1,gm1) (tree_leaves tskip gm inp dir)) as [LEAFSKIP|LEAFITER]. { destruct greedy; simpl in LEAF; apply in_app_or in LEAF; auto. destruct LEAF; auto. } (* skip *) 2: { econstructor; eauto. econstructor; eauto. apply np_quant_skip. } (* iter *) - assert (noprio_list inp (GroupMap.reset (def_groups r1) gm) (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 +∞ r1) :: cont) inp1 gm1). + assert (noprio_list dir inp (GroupMap.reset (def_groups r1) gm) (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 +∞ r1) :: cont) inp1 gm1). { apply IHTREE1; auto. pike_subset. } inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; inversion NP_L0; inversion NP_A1; subst. repeat (econstructor; eauto). - destruct plus; inversion H3. subst. - specialize (IHTREE2 H2 (eq_refl _)). - assert (In (inp1,gm1) (tree_leaves titer (GroupMap.reset (def_groups r1) gm) inp forward) \/ - In (inp1,gm1) (tree_leaves tskip gm inp forward)) as [LEAFSKIP|LEAFITER]. + specialize (IHTREE2 H2). + assert (In (inp1,gm1) (tree_leaves titer (GroupMap.reset (def_groups r1) gm) inp dir) \/ + In (inp1,gm1) (tree_leaves tskip gm inp dir)) as [LEAFSKIP|LEAFITER]. { destruct greedy; simpl in LEAF; apply in_app_or in LEAF; auto. destruct LEAF; auto. } (* skip *) 2: { econstructor; eauto. econstructor; eauto. apply np_quant_skip. } (* iter *) - assert (noprio_list inp (GroupMap.reset (def_groups r1) gm) (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 (NoI.N 0) r1) :: cont) inp1 gm1). + assert (noprio_list dir inp (GroupMap.reset (def_groups r1) gm) (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 (NoI.N 0) r1) :: cont) inp1 gm1). { apply IHTREE1; auto. pike_subset. } inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; inversion NP_L0; inversion NP_A1; subst. repeat (econstructor; eauto). - destruct plus; inversion H3. - - assert (noprio_list inp (GroupMap.open (idx inp) gid gm) (Areg r1 :: Aclose gid :: cont) inp1 gm1). + - assert (noprio_list dir inp (GroupMap.open (idx inp) gid gm) (Areg r1 :: Aclose gid :: cont) inp1 gm1). { apply IHTREE; auto. pike_subset. } inversion H; inversion NP_A; inversion NP_L; inversion NP_A0; subst. repeat (econstructor; eauto). - - specialize (IHTREE H2 (eq_refl _) LEAF). + - specialize (IHTREE H2 LEAF). repeat (econstructor; eauto). Qed. (* For the Pike Subset, the NoPrio Semantics exactly coincides with leaves of the Tree Semantics *) Theorem noprio_eq_is_leaf: - forall r inp gm t leafinp leafgm + forall dir r inp gm t leafinp leafgm (SUBSET: pike_regex r) - (TREE: is_tree rer [Areg r] inp gm forward t), - noprio inp gm r leafinp leafgm <-> - In (leafinp, leafgm) (tree_leaves t gm inp forward). + (TREE: is_tree rer [Areg r] inp gm dir t), + noprio dir inp gm r leafinp leafgm <-> + In (leafinp, leafgm) (tree_leaves t gm inp dir). Proof. - intros r inp gm t leafinp leafgm SUBSET TREE. split. + intros dir r inp gm t leafinp leafgm SUBSET TREE. split. - apply noprio_is_leaf. auto. - intros. eapply is_tree_action_noprio in TREE; eauto. 2: pike_subset. From 39a7becba4e2fb80e7eeefb2437b48f40185dee8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Thu, 11 Jun 2026 15:10:24 +0200 Subject: [PATCH 05/11] Engine: start experiment with reversal property --- Engine/NoPrioSemantics.v | 131 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 131 insertions(+) diff --git a/Engine/NoPrioSemantics.v b/Engine/NoPrioSemantics.v index 5676a75..b34292d 100644 --- a/Engine/NoPrioSemantics.v +++ b/Engine/NoPrioSemantics.v @@ -76,7 +76,45 @@ Section NoPrioSemantics. (* LATER: there will be an issue if we want to add negative lookarounds: strict positivity *) (* We might want to declare an oracle version of this, since this reversal is used in engines when we already know about the values of deeper lookarounds. *) + (** * Properties *) + (* group map irrelevance *) + Theorem noprio_gm_irrel: + forall dir inp0 gm0 r inp1 gm1 gm0' + (NP: noprio dir inp0 gm0 r inp1 gm1), + exists gm1', noprio dir inp0 gm0' r inp1 gm1'. + Proof. + intros dir inp0 gm0 r inp1 gm1 gm0' NP. + generalize dependent gm0'. + induction NP; intros. + - repeat (econstructor; eauto). + - repeat (econstructor; eauto). + - destruct (IHNP gm0') as [gm1' IH]. + repeat (econstructor; eauto). + - destruct (IHNP gm0') as [gm1' IH]. + solve[repeat (econstructor; eauto)]. + - destruct (IHNP1 gm0') as [gm1' IH1]. + destruct (IHNP2 gm1') as [gm2' IH2]. + repeat (econstructor; eauto). + - destruct (IHNP1 gm0') as [gm1' IH1]. + destruct (IHNP2 gm1') as [gm2' IH2]. + repeat (econstructor; eauto). + - destruct (IHNP1 (GroupMap.reset gidl gm0')) as [gm1' IH1]. + destruct (IHNP2 gm1') as [gm2' IH2]. + repeat (econstructor; eauto). + - repeat (econstructor; eauto). + - destruct (IHNP1 (GroupMap.reset gidl gm0')) as [gm1' IH1]. + destruct (IHNP2 gm1') as [gm2' IH2]. + repeat (econstructor; eauto). + - eexists. apply np_quant_skip. + - destruct (IHNP (GroupMap.open (idx inp) gid gm0')) as [gm1' IH]. + repeat (econstructor; eauto). + - repeat (econstructor; eauto). + Qed. + + (* TODO: can we consider removing gm entirely? + We don't have backreferences, and we use it for reversal, the resulting group maps make no sense anyway. *) + (** * NoPrio Tree Equivalence *) Lemma two_app: @@ -323,5 +361,98 @@ Section NoPrioSemantics. 2: pike_subset. inversion TREE; inversion NP_A; inversion NP_L; subst. auto. Qed. + + (** * Reversal Property *) + + Definition reverse (d:Direction): Direction := + match d with + | forward => backward + | backward => forward + end. + + Lemma read_char_reverse: + forall cd inp dir c nextinp, + read_char rer cd inp dir = Some (c, nextinp) -> + read_char rer cd nextinp (reverse dir) = Some (c, inp). + Proof. + intros cd [next1 pref1] dir c [next2 pref2] H. + destruct dir; simpl; simpl in H. + - destruct next1; inversion H. + destruct (char_match) eqn:CM; inversion H. subst. + rewrite CM. auto. + - destruct pref1; inversion H. + destruct (char_match) eqn:CM; inversion H. subst. + rewrite CM. auto. + Qed. + + Theorem noprio_reversal: + forall dir r inp1 inp2 gma gmb + (NP1: noprio dir inp1 gma r inp2 gmb), + forall gmc, exists gmd, noprio (reverse dir) inp2 gmc r inp1 gmd. + Proof. + intros dir r. + induction r; intros. + - inversion NP1. subst. repeat (econstructor; eauto). + - inversion NP1. subst. + apply read_char_reverse in READ as REV. + repeat (econstructor; eauto). + - inversion NP1; subst. + + eapply IHr1 in LEFT as [gmd H]. repeat (econstructor; eauto). + + eapply IHr2 in RIGHT as [gmd H]. solve[repeat (econstructor; eauto)]. + - inversion NP1; subst; simpl in *. + + apply IHr2 with (gmc:=gmc) in SEQ2 as [gmd H2]. + apply IHr1 with (gmc:=gmd) in SEQ1 as H1. destruct H1 as [gme H1]. + (* ah! why doesn't the intro pattern work here? *) + repeat (econstructor; eauto). + + apply IHr1 with (gmc:=gmc) in SEQ2 as [gmd H2]. + apply IHr2 with (gmc:=gmd) in SEQ1 as H1. destruct H1 as [gme H1]. + repeat (econstructor; eauto). + - inversion NP1; subst. + + (* forced *) + (* induction over r fails: r{min} is not a subregex of r{min+1} *) + admit. + + (* done *) + repeat (econstructor; eauto). + + (* free *) + admit. + + (* skip *) + exists gmc. apply np_quant_skip. + - inversion NP1. + - inversion NP1. subst. + eapply IHr in GROUP as [gmd H]. + repeat (econstructor; eauto). + - inversion NP1. subst. + repeat (econstructor; eauto). + - inversion NP1. + Abort. + + + Theorem noprio_reversal: + forall dir r inp1 inp2 gma gmb + (NP1: noprio dir inp1 gma r inp2 gmb), + forall gmc, exists gmd, noprio (reverse dir) inp2 gmc r inp1 gmd. + Proof. + intros dir r inp1 inp2 gma gmb NP1 gmc. + generalize dependent gmc. induction NP1; intros. + - repeat (econstructor; eauto). + - apply read_char_reverse in READ as REV. + destruct dir; simpl; exists gmc; econstructor; eauto. + - destruct (IHNP1 gmc) as [gmd H]. eexists. apply np_disj_left. eauto. + - destruct (IHNP1 gmc) as [gmd H]. eexists. apply np_disj_right. eauto. + - destruct (IHNP1_2 gmc) as [gmd H2]. destruct (IHNP1_1 gmd) as [gme H1]. + repeat (econstructor; eauto). + - destruct (IHNP1_2 gmc) as [gmd H1]. destruct (IHNP1_1 gmd) as [gme H2]. + repeat (econstructor; eauto). + - admit. + (* does not work: in one direction we do r and then r{min} + in the other we also do r and then r{min}, but we would like them switched to apply IH. + One solution would be to prove that for noprio, r.r{} is equivalent to r{}.r *) + - repeat (econstructor; eauto). + - admit. + - eexists. eapply np_quant_skip. + - destruct (IHNP1 (GroupMap.open (idx nextinp) gid gmc)) as [gmd H1]. + repeat (econstructor; eauto). + - repeat (econstructor; eauto). + Admitted. End NoPrioSemantics. From c288698b8204896963950c4215be5cae6d819dec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Thu, 11 Jun 2026 15:10:44 +0200 Subject: [PATCH 06/11] Engine: new version of the nopriority semantics without group maps --- Engine/NoPrioSemantics2.v | 380 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 380 insertions(+) create mode 100644 Engine/NoPrioSemantics2.v diff --git a/Engine/NoPrioSemantics2.v b/Engine/NoPrioSemantics2.v new file mode 100644 index 0000000..97fae50 --- /dev/null +++ b/Engine/NoPrioSemantics2.v @@ -0,0 +1,380 @@ +From Stdlib Require Import List Lia. +Import ListNotations. + +From Linden Require Import Regex Chars Groups. +From Linden Require Import Tree Semantics PikeSubset. +From Warblre Require Import Base RegExpRecord. +From Linden Require Import StrictSuffix. +From Linden Require Import FunctionalSemantics. +From Linden Require Import ComputeIsTree. +From Linden Require Import Parameters. +From Linden Require Import FlatMap Equivalence FunctionalUtils. + + +(* A rephrasing of the semantics, where priority does not matter *) +(* It's a relation about leaves, not necessarily the first one *) +(* There are no actions, the shape of the regex determines the relation *) +(* For this version, we don't veen consider group_maps (although we could compute them along the way) + Because for the reversal property we don't need them. *) + +Section NoPrioSemantics. + Context {params: LindenParameters}. + Context (rer: RegExpRecord). + + Inductive noprio: Direction -> input -> regex -> input -> Prop := + | np_eps: + forall dir inp, + noprio dir inp Epsilon inp + | np_char: + forall dir inp cd c nextinp + (READ: read_char rer cd inp dir = Some (c, nextinp)), + noprio dir inp (Regex.Character cd) nextinp + | np_disj_left: + forall dir inp r1 r2 nextinp + (LEFT: noprio dir inp r1 nextinp), + noprio dir inp (Disjunction r1 r2) nextinp + | np_disj_right: + forall dir inp r1 r2 nextinp + (RIGHT: noprio dir inp r2 nextinp), + noprio dir inp (Disjunction r1 r2) nextinp + | np_seq_forward: + forall inp0 r1 r2 inp1 inp2 + (SEQ1: noprio forward inp0 r1 inp1) + (SEQ2: noprio forward inp1 r2 inp2), + noprio forward inp0 (Sequence r1 r2) inp2 + | np_seq_backward: + forall inp0 r1 r2 inp1 inp2 + (SEQ1: noprio backward inp0 r2 inp1) + (SEQ2: noprio backward inp1 r1 inp2), + noprio backward inp0 (Sequence r1 r2) inp2 + | np_quant_forced: + forall dir inp0 r gidl min delta greedy inp1 inp2 + (RESET: gidl = def_groups r) + (ITER: noprio dir inp0 r inp1) + (LOOP: noprio dir inp1 (Quantified greedy min delta r) inp2), + noprio dir inp0 (Quantified greedy (S min) delta r) inp2 + | np_quant_done: + forall dir inp r greedy, + noprio dir inp (Quantified greedy 0 (NoI.N 0) r) inp + | np_quant_free: + forall dir inp0 r greedy delta gidl inp1 inp2 + (RESET: gidl = def_groups r) + (ITER: noprio dir inp0 r inp1) + (PROGRESS: strict_suffix inp1 inp0 dir) + (LOOP: noprio dir inp1 (Quantified greedy 0 delta r) inp2), + noprio dir inp0 (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp2 + | np_quant_skip: + forall dir inp r greedy delta, + noprio dir inp (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp + | np_group: + forall dir inp r gid nextinp + (GROUP: noprio dir inp r nextinp), + noprio dir inp (Group gid r) nextinp + | np_anchor: + forall dir inp a + (ANCHOR: anchor_satisfied rer a inp = true), + noprio dir inp (Anchor a) inp. + + (* LATER: there will be an issue if we want to add negative lookarounds: strict positivity *) + (* We might want to declare an oracle version of this, since this reversal is used in engines when we already know about the values of deeper lookarounds. *) + + (** * NoPrio Tree Equivalence *) + + Lemma two_app: + forall A (a1 a2:A), [a1; a2] = [a1] ++ [a2]. + Proof. auto. Qed. + + Lemma three_app: + forall A (a1 a2 a3:A), [a1; a2; a3] = [a1] ++ [a2] ++ [a3]. + Proof. auto. Qed. + + (* If we can find a leaf in the tree of the first list of actions, + then a leaf in the tree of the second list, + then that final leaf is a leaf of the tree of the concatenation *) + Lemma in_leaves_app: + forall dir inp0 gm0 inp1 gm1 inp2 gm2 a1 a2 t1 t2 t12 + (TREE12: is_tree rer (a1 ++ a2) inp0 gm0 dir t12) + (TREE1: is_tree rer a1 inp0 gm0 dir t1) + (TREE2: is_tree rer a2 inp1 gm1 dir t2) + (IN1: In (inp1,gm1) (tree_leaves t1 gm0 inp0 dir)) + (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 dir)), + In (inp2, gm2) (tree_leaves t12 gm0 inp0 dir). + Proof. + intros dir inp0 gm0 inp1 gm1 inp2 gm2 a1 a2 t1 t2 t12 TREE12 TREE1 TREE2 IN1 IN2. + specialize (leaves_concat _ _ _ _ _ _ _ _ TREE12 TREE1) as FM. + assert (ACT: act_from_leaf rer a2 dir (inp1, gm1) (tree_leaves t2 gm1 inp1 dir)). + { constructor. simpl. auto. } + specialize (FlatMap_in _ _ _ _ _ (act_from_leaf_determ _ _ _) FM IN1 ACT) as FM_IN. + rewrite Forall_forall in FM_IN. + apply FM_IN. auto. + Qed. + + Lemma in_leaves_app3: + forall dir inp0 gm0 inp1 gm1 inp2 gm2 inp3 gm3 a1 a2 a3 t1 t2 t3 t123 + (TREE123: is_tree rer (a1 ++ a2 ++ a3) inp0 gm0 dir t123) + (TREE1: is_tree rer a1 inp0 gm0 dir t1) + (TREE2: is_tree rer a2 inp1 gm1 dir t2) + (TREE3: is_tree rer a3 inp2 gm2 dir t3) + (IN1: In (inp1,gm1) (tree_leaves t1 gm0 inp0 dir)) + (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 dir)) + (IN3: In (inp3, gm3) (tree_leaves t3 gm2 inp2 dir)), + In (inp3, gm3) (tree_leaves t123 gm0 inp0 dir). + Proof. + intros dir inp0 gm0 inp1 gm1 inp2 gm2 inp3 gm3 a1 a2 a3 t1 t2 t3 t123 TREE123 TREE1 TREE2 TREE3 IN1 IN2 IN3. + specialize (is_tree_productivity rer (a2 ++ a3) inp1 gm1 dir) as [t23 TREE23]. + assert (IN23: In (inp3, gm3) (tree_leaves t23 gm1 inp1 dir)). + { apply (in_leaves_app _ _ _ _ _ _ _ _ _ _ _ _ TREE23 TREE2 TREE3 IN2 IN3). } + apply (in_leaves_app _ _ _ _ _ _ _ _ _ _ _ _ TREE123 TREE1 TREE23 IN1 IN23). + Qed. + + (* all leaves obtained from noprio are leaves of the backtracking tree *) + Theorem noprio_is_leaf: + forall dir r inp gm t leafinp + (TREE: is_tree rer [Areg r] inp gm dir t), + noprio dir inp r leafinp -> + exists leafgm, In (leafinp, leafgm) (tree_leaves t gm inp dir). + Proof. + intros dir r inp gm t leafinp TREE NP. + generalize dependent t. generalize dependent gm. + induction NP; intros. + - inversion TREE; subst. inversion ISTREE; subst. + simpl. eauto. + - inversion TREE; subst; + rewrite READ0 in READ; inversion READ; subst. + inversion TREECONT; subst. simpl. + apply read_char_success_advance in READ0. + unfold advance_input'. rewrite READ0. eauto. + - inversion TREE; subst. apply IHNP in ISTREE1 as [leafgm IH1]. + simpl. eexists. apply in_or_app. eauto. + - inversion TREE; subst. apply IHNP in ISTREE2 as [leafgm IH2]. + simpl. eexists. apply in_or_app. eauto. + - inversion TREE; subst. + simpl in CONT. rewrite two_app in CONT. + specialize (is_tree_productivity rer [Areg r1] inp0 gm forward) as [t1 HT1]. + apply IHNP1 in HT1 as H. destruct H as [gm1 IN1]. + specialize (is_tree_productivity rer [Areg r2] inp1 gm1 forward) as [t2 HT2]. + apply IHNP2 in HT2 as H. destruct H as [gm2 IN2]. + eexists. eapply in_leaves_app; eauto. + - inversion TREE; subst. + simpl in CONT. rewrite two_app in CONT. + specialize (is_tree_productivity rer [Areg r2] inp0 gm backward) as [t2 HT2]. + apply IHNP1 in HT2 as H. destruct H as [gm2 IN2]. + specialize (is_tree_productivity rer [Areg r1] inp1 gm2 backward) as [t1 HT1]. + apply IHNP2 in HT1 as H. destruct H as [gm1 IN1]. + eexists. eapply in_leaves_app; eauto. + - inversion TREE; subst. + rewrite two_app in ISTREE1. + specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm) dir) as [t1 HT1]. + assert (IN1: exists gm1, In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm) inp0 dir)). + { apply IHNP1. auto. } destruct IN1 as [gm1 IN1]. + specialize (is_tree_productivity rer [Areg (Quantified greedy min delta r)] inp1 gm1 dir) as [t2 HT2]. + assert (IN2: exists gm2, In (inp2, gm2) (tree_leaves t2 gm1 inp1 dir)). + { apply IHNP2. auto. } destruct IN2 as [gm2 IN2]. + eexists. eapply (in_leaves_app _ _ _ _ _ inp2 gm2 _ _ _ _ _ ISTREE1 HT1 HT2 IN1 IN2); eauto. + - inversion TREE; subst. + + inversion SKIP; subst. simpl. eauto. + + destruct plus; inversion H1. + - inversion TREE; subst. + { destruct delta; inversion H1. } + assert (DP: plus = delta). + { destruct plus; destruct delta; auto; inversion H1; auto. } + subst. clear H1. clear SKIP. + specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm) dir) as [t1 HT1]. + assert (IN1: exists gm1, In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm) inp0 dir)). + { apply IHNP1. auto. } destruct IN1 as [gm1 IN1]. + specialize (is_tree_productivity rer [Acheck inp0] inp1 gm1 dir) as [t2 HT2]. + assert (IN2: In (inp1, gm1) (tree_leaves t2 gm1 inp1 dir)). + { inversion HT2; subst. + - inversion TREECONT; subst. simpl. auto. + - apply CHECKFAIL in PROGRESS. inversion PROGRESS. (* we know progress happened *) + } + specialize (is_tree_productivity rer [Areg (Quantified greedy 0 delta r)] inp1 gm1 dir) as [t3 HT3]. + assert (IN3: exists gm2, In (inp2, gm2) (tree_leaves t3 gm1 inp1 dir)). + { apply IHNP2. auto. } destruct IN3 as [gm2 IN3]. + rewrite three_app in ISTREE1. + destruct greedy; simpl. + + eexists. apply in_or_app. left. + eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). + + eexists. apply in_or_app. right. + eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). + - inversion TREE; subst. + { destruct delta; inversion H1. } + inversion SKIP. subst. + destruct greedy; simpl; eauto. + eexists. apply in_or_app; simpl; eauto. + - inversion TREE; subst. + rewrite two_app in TREECONT. + specialize (is_tree_productivity rer [Areg r] inp (GroupMap.open (idx inp) gid gm) dir) as [t1 HT1]. + assert (IN1: exists nextgm, In (nextinp, nextgm) (tree_leaves t1 (GroupMap.open (idx inp) gid gm) inp dir)). + { apply IHNP. auto. } destruct IN1 as [nextgm IN1]. + specialize (is_tree_productivity rer [Aclose gid] nextinp nextgm dir) as [t2 HT2]. + assert (IN2: In (nextinp, GroupMap.close (idx nextinp) gid nextgm) (tree_leaves t2 nextgm nextinp dir)). + { inversion HT2. subst. inversion TREECONT0. subst. simpl. auto. } + eexists. eapply (in_leaves_app _ _ _ _ _ nextinp (GroupMap.close (idx nextinp) gid nextgm) _ _ _ _ _ TREECONT HT1 HT2 IN1 IN2); eauto. + - inversion TREE; subst; + rewrite ANCHOR0 in ANCHOR; inversion ANCHOR. + inversion TREECONT; subst. simpl. eauto. + Qed. + + (* Other direction: generalizing the noprio semantics to actions *) + + Inductive noprio_action: Direction -> input -> action -> input -> Prop := + | np_regex: + forall dir inp r nextinp + (NP: noprio dir inp r nextinp), + noprio_action dir inp (Areg r) nextinp + | np_close: + forall dir inp gid, + noprio_action dir inp (Aclose gid) inp + | np_check: + forall dir inp inpcheck + (PROGRESS: strict_suffix inp inpcheck dir), + noprio_action dir inp (Acheck inpcheck) inp. + + Inductive noprio_list: Direction -> input -> list action -> input -> Prop := + | np_nil: + forall dir inp, + noprio_list dir inp [] inp + | np_cons: + forall dir inp0 a inp1 l inp2 + (NP_A: noprio_action dir inp0 a inp1) + (NP_L: noprio_list dir inp1 l inp2), + noprio_list dir inp0 (a::l) inp2. + + Lemma is_tree_action_noprio: + forall dir inp0 gm0 l t inp1 gm1 + (SUBSET: pike_actions l) + (TREE: is_tree rer l inp0 gm0 dir t) + (LEAF: In (inp1, gm1) (tree_leaves t gm0 inp0 dir)), + noprio_list dir inp0 l inp1. + Proof. + intros dir inp0 gm0 l t inp1 gm1 SUBSET TREE LEAF. + induction TREE; simpl in LEAF; subst; + try solve [inversion LEAF]; pike_subset. + - destruct LEAF as [LEAF|LEAF]; inversion LEAF; subst. constructor. + - repeat (econstructor; eauto). + - repeat (econstructor; eauto). + - repeat (econstructor; eauto). + - econstructor; eauto. + 2: { apply read_char_success_advance in READ as ADV. + unfold advance_input' in LEAF. rewrite ADV in LEAF. eauto. } + repeat (econstructor; eauto). + - apply in_app_or in LEAF as [LEAF|LEAF]. + + assert (noprio_list dir inp (Areg r1::cont) inp1). + { apply IHTREE1; auto. pike_subset. } + inversion H; subst. inversion NP_A. repeat (econstructor; eauto). + + assert (noprio_list dir inp (Areg r2::cont) inp1). + { apply IHTREE2; auto. pike_subset. } + inversion H; subst. inversion NP_A. solve[repeat (econstructor; eauto)]. + - destruct dir. + + simpl in IHTREE. + assert (noprio_list forward inp (Areg r1 :: Areg r2 :: cont) inp1). + { apply IHTREE; auto. pike_subset. } + inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; subst. + repeat (econstructor; eauto). + + simpl in IHTREE. + assert (noprio_list backward inp (Areg r2 :: Areg r1 :: cont) inp1). + { apply IHTREE; auto. pike_subset. } + inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; subst. + repeat (econstructor; eauto). + - specialize (IHTREE H2 LEAF). + repeat econstructor; eauto. + - destruct plus; inversion H3; subst. + specialize (IHTREE2 H2). + assert (In (inp1,gm1) (tree_leaves titer (GroupMap.reset (def_groups r1) gm) inp dir) \/ + In (inp1,gm1) (tree_leaves tskip gm inp dir)) as [LEAFSKIP|LEAFITER]. + { destruct greedy; simpl in LEAF; apply in_app_or in LEAF; auto. + destruct LEAF; auto. } + (* skip *) + 2: { econstructor; eauto. econstructor; eauto. apply np_quant_skip. } + (* iter *) + assert (noprio_list dir inp (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 +∞ r1) :: cont) inp1). + { apply IHTREE1; auto. pike_subset. } + inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; inversion NP_L0; inversion NP_A1; subst. + repeat (econstructor; eauto). + - destruct plus; inversion H3. subst. + specialize (IHTREE2 H2). + assert (In (inp1,gm1) (tree_leaves titer (GroupMap.reset (def_groups r1) gm) inp dir) \/ + In (inp1,gm1) (tree_leaves tskip gm inp dir)) as [LEAFSKIP|LEAFITER]. + { destruct greedy; simpl in LEAF; apply in_app_or in LEAF; auto. + destruct LEAF; auto. } + (* skip *) + 2: { econstructor; eauto. econstructor; eauto. apply np_quant_skip. } + (* iter *) + assert (noprio_list dir inp (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 (NoI.N 0) r1) :: cont) inp1). + { apply IHTREE1; auto. pike_subset. } + inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; inversion NP_L0; inversion NP_A1; subst. + repeat (econstructor; eauto). + - destruct plus; inversion H3. + - assert (noprio_list dir inp (Areg r1 :: Aclose gid :: cont) inp1). + { apply IHTREE; auto. pike_subset. } + inversion H; inversion NP_A; inversion NP_L; inversion NP_A0; subst. + repeat (econstructor; eauto). + - specialize (IHTREE H2 LEAF). + repeat (econstructor; eauto). + Qed. + + (* For the Pike Subset, the NoPrio Semantics exactly coincides with leaves of the Tree Semantics *) + Theorem noprio_eq_is_leaf: + forall dir r inp gm t leafinp + (SUBSET: pike_regex r) + (TREE: is_tree rer [Areg r] inp gm dir t), + noprio dir inp r leafinp <-> + exists leafgm, In (leafinp, leafgm) (tree_leaves t gm inp dir). + Proof. + intros dir r inp gm t leafinp SUBSET TREE. split. + - apply noprio_is_leaf. auto. + - intros [leafgm H]. eapply is_tree_action_noprio in TREE; eauto. + 2: pike_subset. + inversion TREE; inversion NP_A; inversion NP_L; subst. auto. + Qed. + + (** * Reversal Property *) + + Definition reverse (d:Direction): Direction := + match d with + | forward => backward + | backward => forward + end. + + Lemma read_char_reverse: + forall cd inp dir c nextinp, + read_char rer cd inp dir = Some (c, nextinp) -> + read_char rer cd nextinp (reverse dir) = Some (c, inp). + Proof. + intros cd [next1 pref1] dir c [next2 pref2] H. + destruct dir; simpl; simpl in H. + - destruct next1; inversion H. + destruct (char_match) eqn:CM; inversion H. subst. + rewrite CM. auto. + - destruct pref1; inversion H. + destruct (char_match) eqn:CM; inversion H. subst. + rewrite CM. auto. + Qed. + + Theorem noprio_reversal: + forall dir r inp1 inp2 + (NP1: noprio dir inp1 r inp2), + noprio (reverse dir) inp2 r inp1. + Proof. + intros dir r inp1 inp2 NP1. + induction NP1; intros. + - repeat (econstructor; eauto). + - apply read_char_reverse in READ as REV. + destruct dir; simpl; econstructor; eauto. + - repeat (econstructor; eauto). + - solve[repeat (econstructor; eauto)]. + - repeat (econstructor; eauto). + - repeat (econstructor; eauto). + - admit. + (* does not work: in one direction we do r and then r{min} + in the other we also do r and then r{min}, but we would like them switched to apply IH. + One solution would be to prove that for noprio, r.r{} is equivalent to r{}.r *) + - repeat (econstructor; eauto). + - admit. + - eapply np_quant_skip. + - repeat (econstructor; eauto). + - repeat (econstructor; eauto). + Admitted. + +End NoPrioSemantics. From 30d826dff7da9e4c4beab85a14330f9e332a9a39 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Fri, 12 Jun 2026 11:57:11 +0200 Subject: [PATCH 07/11] Engine: nopriority characterization of quantifiers as numbered iterations --- Engine/NoPrioSemantics2.v | 101 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 97 insertions(+), 4 deletions(-) diff --git a/Engine/NoPrioSemantics2.v b/Engine/NoPrioSemantics2.v index 97fae50..e320eae 100644 --- a/Engine/NoPrioSemantics2.v +++ b/Engine/NoPrioSemantics2.v @@ -48,8 +48,7 @@ Section NoPrioSemantics. (SEQ2: noprio backward inp1 r1 inp2), noprio backward inp0 (Sequence r1 r2) inp2 | np_quant_forced: - forall dir inp0 r gidl min delta greedy inp1 inp2 - (RESET: gidl = def_groups r) + forall dir inp0 r min delta greedy inp1 inp2 (ITER: noprio dir inp0 r inp1) (LOOP: noprio dir inp1 (Quantified greedy min delta r) inp2), noprio dir inp0 (Quantified greedy (S min) delta r) inp2 @@ -57,8 +56,7 @@ Section NoPrioSemantics. forall dir inp r greedy, noprio dir inp (Quantified greedy 0 (NoI.N 0) r) inp | np_quant_free: - forall dir inp0 r greedy delta gidl inp1 inp2 - (RESET: gidl = def_groups r) + forall dir inp0 r greedy delta inp1 inp2 (ITER: noprio dir inp0 r inp1) (PROGRESS: strict_suffix inp1 inp0 dir) (LOOP: noprio dir inp1 (Quantified greedy 0 delta r) inp2), @@ -329,6 +327,101 @@ Section NoPrioSemantics. inversion TREE; inversion NP_A; inversion NP_L; subst. auto. Qed. + (** * Quantifier Properties *) + + Lemma iteration_suffix: + forall dir r inp0 inp1 + (NP: noprio dir inp0 r inp1), + inp0 = inp1 \/ strict_suffix inp1 inp0 dir. + Proof. + intros dir r inp0 inp1 NP. induction NP; auto. + 1: { apply read_char_suffix in READ. auto. } + all: destruct IHNP1; destruct IHNP2; subst; auto; + right; eapply strict_suffix_trans; eauto. + Qed. + + (* In order to prove the reversal property, we characterize quantifiers in the nopriority semantics *) + + (* n iterations of a regex *) + Inductive iters : nat -> Direction -> input -> regex -> input -> Prop := + | iters_refl: + forall inp r dir, iters 0 dir inp r inp + | iters_next: + forall r n inp0 inp1 inp2 dir + (NEXT: noprio dir inp0 r inp1) + (ITERS: iters n dir inp1 r inp2), + iters (S n) dir inp0 r inp2. + + (* is n <= min + delta ? *) + Inductive smaller: nat -> nat -> non_neg_integer_or_inf -> Prop := + | smaller_nat: forall n min delta, + n <= min + delta -> + smaller n min (NoI.N delta) + | smaller_inf: forall n min, + smaller n min NoI.Inf. + + (* a characterization of quantifiers using numbered iterations *) + Lemma quant_iters: + forall r dir greedy inp0 inp1 min delta + (QUANT: noprio dir inp0 (Quantified greedy min delta r) inp1), + exists n, n >= min /\ smaller n min delta /\ iters n dir inp0 r inp1. + Proof. + intros r dir greedy inp0 inp1 min delta QUANT. + remember (Quantified greedy min delta r) as quant. + generalize dependent min. generalize dependent delta. + induction QUANT; intros; + inversion Heqquant; subst. + - clear IHQUANT1. + specialize (IHQUANT2 delta0 min (eq_refl _)) as [n [GE [LE IT]]]. + exists (S n). split; [lia|]. split. + { inversion LE; subst; constructor. lia. } + econstructor; eauto. + - exists 0. split; [lia|]. split; constructor; auto. + - clear IHQUANT1. specialize (IHQUANT2 delta 0 (eq_refl _)) as [n [GE [LE IT]]]. + exists (S n). split; [lia|]. split. + { inversion LE; subst; constructor. lia. } + econstructor; eauto. + - exists 0. split; [lia|]. split. + { destruct delta; constructor. lia. } + constructor. + Qed. + + Lemma iters_quant: + forall r dir greedy inp0 inp1 min delta n + (GE: n >= min) + (LE: smaller n min delta) + (ITERS: iters n dir inp0 r inp1), + noprio dir inp0 (Quantified greedy min delta r) inp1. + Proof. + intros r dir greedy inp0 inp1 min delta n GE LE ITERS. + generalize dependent min. generalize dependent delta. + induction ITERS; intros. + - destruct min; inversion GE. inversion LE; subst. + + destruct delta0. + * apply np_quant_done. + * replace (NoI.N (S delta0)) with (NoI.N 1 + NoI.N delta0)%NoI by auto. + apply np_quant_skip. + + replace NoI.Inf with (NoI.N 1 + NoI.Inf)%NoI by auto. + apply np_quant_skip. + - destruct min. + (* forced iteration *) + 2:{ eapply np_quant_forced; eauto. apply IHITERS. lia. + inversion LE; subst; constructor. lia. } + (* free iteration: cas analysis on if the first iteration did progress *) + apply iteration_suffix in NEXT as H. destruct H as [EQ|SUF]. + + (* first iteration didn't progress: we skip it in the quantifier *) + subst. apply IHITERS. lia. inversion LE; subst; constructor. lia. + + (* first iteration made progress: we can use it as a quantifier iteration *) + inversion LE; subst. + * destruct delta0; [lia|]. + replace (NoI.N (S delta0)) with (NoI.N 1 + NoI.N delta0)%NoI by auto. + eapply np_quant_free; eauto. apply IHITERS. lia. + constructor. lia. + * replace NoI.Inf with (NoI.N 1 + NoI.Inf)%NoI by auto. + eapply np_quant_free; eauto. apply IHITERS. lia. + constructor. + Qed. + (** * Reversal Property *) Definition reverse (d:Direction): Direction := From 74c18a279f6a6bcc7884c0fbfbc1f79f6e62187b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Fri, 12 Jun 2026 13:10:02 +0200 Subject: [PATCH 08/11] Engine: prove leaf reversal property --- Engine/NoPrioSemantics2.v | 48 ++++++++++++++++++++++++++++++++++----- 1 file changed, 42 insertions(+), 6 deletions(-) diff --git a/Engine/NoPrioSemantics2.v b/Engine/NoPrioSemantics2.v index e320eae..d19315c 100644 --- a/Engine/NoPrioSemantics2.v +++ b/Engine/NoPrioSemantics2.v @@ -421,6 +421,18 @@ Section NoPrioSemantics. eapply np_quant_free; eauto. apply IHITERS. lia. constructor. Qed. + + (* Adding an iteration at the end *) + Lemma add_iter_end: + forall dir r n inp0 inp1 inp2 + (ITERS: iters n dir inp0 r inp1) + (NEXT: noprio dir inp1 r inp2), + iters (S n) dir inp0 r inp2. + Proof. + intros. induction ITERS; repeat (econstructor; eauto). + Qed. + + (** * Reversal Property *) @@ -459,15 +471,39 @@ Section NoPrioSemantics. - solve[repeat (econstructor; eauto)]. - repeat (econstructor; eauto). - repeat (econstructor; eauto). - - admit. - (* does not work: in one direction we do r and then r{min} - in the other we also do r and then r{min}, but we would like them switched to apply IH. - One solution would be to prove that for noprio, r.r{} is equivalent to r{}.r *) + - apply quant_iters in IHNP1_2 as [n [GE [LE IT]]]. + apply iters_quant with (n:= S n); auto. lia. + { inversion LE; subst; constructor. lia. } + eapply add_iter_end; eauto. - repeat (econstructor; eauto). - - admit. + - apply quant_iters in IHNP1_2 as [n [GE [LE IT]]]. + apply iters_quant with (n:=S n); auto. + { inversion LE; subst; constructor. lia. } + eapply add_iter_end; eauto. - eapply np_quant_skip. - repeat (econstructor; eauto). - repeat (econstructor; eauto). - Admitted. + Qed. + + (** * Leaf Reversal Theorem *) + + (* We come back to is_tree semantics to prove the reversal property *) + Lemma leaf_reversal: + forall r dir inp1 inp2 gm2 t1 t2 + (SUBSET: pike_regex r) + (TREE1: is_tree rer [Areg r] inp1 GroupMap.empty dir t1) + (TREE2: is_tree rer [Areg r] inp2 GroupMap.empty (reverse dir) t2) + (IN: In (inp2, gm2) (tree_leaves t1 GroupMap.empty inp1 dir)), + exists gm1, In (inp1, gm1) (tree_leaves t2 GroupMap.empty inp2 (reverse dir)). + Proof. + intros r dir inp1 inp2 gm2 t1 t2 SUBSET TREE1 TREE2 IN. + assert (NP1: noprio dir inp1 r inp2). + { apply <- noprio_eq_is_leaf; eauto. } + apply noprio_reversal in NP1 as NP2. + assert (IN2: exists leafgm, In (inp1, leafgm) (tree_leaves t2 GroupMap.empty inp2 (reverse dir))). + { eapply noprio_eq_is_leaf; eauto. } + eauto. + Qed. + End NoPrioSemantics. From 3b9979f7072309238ba30d3cbe72dbb6f07ef5f3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Fri, 12 Jun 2026 13:10:42 +0200 Subject: [PATCH 09/11] Engine: Only use non-group-map Noprio semantics --- Engine/NoPrioSemantics.v | 465 ++++++++++++++++++---------------- Engine/NoPrioSemantics2.v | 509 -------------------------------------- 2 files changed, 258 insertions(+), 716 deletions(-) delete mode 100644 Engine/NoPrioSemantics2.v diff --git a/Engine/NoPrioSemantics.v b/Engine/NoPrioSemantics.v index b34292d..d19315c 100644 --- a/Engine/NoPrioSemantics.v +++ b/Engine/NoPrioSemantics.v @@ -14,107 +14,68 @@ From Linden Require Import FlatMap Equivalence FunctionalUtils. (* A rephrasing of the semantics, where priority does not matter *) (* It's a relation about leaves, not necessarily the first one *) (* There are no actions, the shape of the regex determines the relation *) +(* For this version, we don't veen consider group_maps (although we could compute them along the way) + Because for the reversal property we don't need them. *) Section NoPrioSemantics. Context {params: LindenParameters}. Context (rer: RegExpRecord). - Inductive noprio: Direction -> input -> group_map -> regex -> input -> group_map -> Prop := + Inductive noprio: Direction -> input -> regex -> input -> Prop := | np_eps: - forall dir inp gm, - noprio dir inp gm Epsilon inp gm + forall dir inp, + noprio dir inp Epsilon inp | np_char: - forall dir inp gm cd c nextinp + forall dir inp cd c nextinp (READ: read_char rer cd inp dir = Some (c, nextinp)), - noprio dir inp gm (Regex.Character cd) nextinp gm + noprio dir inp (Regex.Character cd) nextinp | np_disj_left: - forall dir inp gm r1 r2 nextinp nextgm - (LEFT: noprio dir inp gm r1 nextinp nextgm), - noprio dir inp gm (Disjunction r1 r2) nextinp nextgm + forall dir inp r1 r2 nextinp + (LEFT: noprio dir inp r1 nextinp), + noprio dir inp (Disjunction r1 r2) nextinp | np_disj_right: - forall dir inp gm r1 r2 nextinp nextgm - (RIGHT: noprio dir inp gm r2 nextinp nextgm), - noprio dir inp gm (Disjunction r1 r2) nextinp nextgm + forall dir inp r1 r2 nextinp + (RIGHT: noprio dir inp r2 nextinp), + noprio dir inp (Disjunction r1 r2) nextinp | np_seq_forward: - forall inp0 gm0 r1 r2 inp1 gm1 inp2 gm2 - (SEQ1: noprio forward inp0 gm0 r1 inp1 gm1) - (SEQ2: noprio forward inp1 gm1 r2 inp2 gm2), - noprio forward inp0 gm0 (Sequence r1 r2) inp2 gm2 + forall inp0 r1 r2 inp1 inp2 + (SEQ1: noprio forward inp0 r1 inp1) + (SEQ2: noprio forward inp1 r2 inp2), + noprio forward inp0 (Sequence r1 r2) inp2 | np_seq_backward: - forall inp0 gm0 r1 r2 inp1 gm1 inp2 gm2 - (SEQ1: noprio backward inp0 gm0 r2 inp1 gm1) - (SEQ2: noprio backward inp1 gm1 r1 inp2 gm2), - noprio backward inp0 gm0 (Sequence r1 r2) inp2 gm2 + forall inp0 r1 r2 inp1 inp2 + (SEQ1: noprio backward inp0 r2 inp1) + (SEQ2: noprio backward inp1 r1 inp2), + noprio backward inp0 (Sequence r1 r2) inp2 | np_quant_forced: - forall dir inp0 gm0 r gidl min delta greedy inp1 gm1 inp2 gm2 - (RESET: gidl = def_groups r) - (ITER: noprio dir inp0 (GroupMap.reset gidl gm0) r inp1 gm1) - (LOOP: noprio dir inp1 gm1 (Quantified greedy min delta r) inp2 gm2), - noprio dir inp0 gm0 (Quantified greedy (S min) delta r) inp2 gm2 + forall dir inp0 r min delta greedy inp1 inp2 + (ITER: noprio dir inp0 r inp1) + (LOOP: noprio dir inp1 (Quantified greedy min delta r) inp2), + noprio dir inp0 (Quantified greedy (S min) delta r) inp2 | np_quant_done: - forall dir inp gm r greedy, - noprio dir inp gm (Quantified greedy 0 (NoI.N 0) r) inp gm + forall dir inp r greedy, + noprio dir inp (Quantified greedy 0 (NoI.N 0) r) inp | np_quant_free: - forall dir inp0 gm0 r greedy delta gidl inp1 gm1 inp2 gm2 - (RESET: gidl = def_groups r) - (ITER: noprio dir inp0 (GroupMap.reset gidl gm0) r inp1 gm1) + forall dir inp0 r greedy delta inp1 inp2 + (ITER: noprio dir inp0 r inp1) (PROGRESS: strict_suffix inp1 inp0 dir) - (LOOP: noprio dir inp1 gm1 (Quantified greedy 0 delta r) inp2 gm2), - noprio dir inp0 gm0 (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp2 gm2 + (LOOP: noprio dir inp1 (Quantified greedy 0 delta r) inp2), + noprio dir inp0 (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp2 | np_quant_skip: - forall dir inp gm r greedy delta, - noprio dir inp gm (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp gm + forall dir inp r greedy delta, + noprio dir inp (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp | np_group: - forall dir inp gm r gid nextinp nextgm - (GROUP: noprio dir inp (GroupMap.open (idx inp) gid gm) r nextinp nextgm), - noprio dir inp gm (Group gid r) nextinp (GroupMap.close (idx nextinp) gid nextgm) + forall dir inp r gid nextinp + (GROUP: noprio dir inp r nextinp), + noprio dir inp (Group gid r) nextinp | np_anchor: - forall dir inp gm a + forall dir inp a (ANCHOR: anchor_satisfied rer a inp = true), - noprio dir inp gm (Anchor a) inp gm. - + noprio dir inp (Anchor a) inp. + (* LATER: there will be an issue if we want to add negative lookarounds: strict positivity *) (* We might want to declare an oracle version of this, since this reversal is used in engines when we already know about the values of deeper lookarounds. *) - - (** * Properties *) - - (* group map irrelevance *) - Theorem noprio_gm_irrel: - forall dir inp0 gm0 r inp1 gm1 gm0' - (NP: noprio dir inp0 gm0 r inp1 gm1), - exists gm1', noprio dir inp0 gm0' r inp1 gm1'. - Proof. - intros dir inp0 gm0 r inp1 gm1 gm0' NP. - generalize dependent gm0'. - induction NP; intros. - - repeat (econstructor; eauto). - - repeat (econstructor; eauto). - - destruct (IHNP gm0') as [gm1' IH]. - repeat (econstructor; eauto). - - destruct (IHNP gm0') as [gm1' IH]. - solve[repeat (econstructor; eauto)]. - - destruct (IHNP1 gm0') as [gm1' IH1]. - destruct (IHNP2 gm1') as [gm2' IH2]. - repeat (econstructor; eauto). - - destruct (IHNP1 gm0') as [gm1' IH1]. - destruct (IHNP2 gm1') as [gm2' IH2]. - repeat (econstructor; eauto). - - destruct (IHNP1 (GroupMap.reset gidl gm0')) as [gm1' IH1]. - destruct (IHNP2 gm1') as [gm2' IH2]. - repeat (econstructor; eauto). - - repeat (econstructor; eauto). - - destruct (IHNP1 (GroupMap.reset gidl gm0')) as [gm1' IH1]. - destruct (IHNP2 gm1') as [gm2' IH2]. - repeat (econstructor; eauto). - - eexists. apply np_quant_skip. - - destruct (IHNP (GroupMap.open (idx inp) gid gm0')) as [gm1' IH]. - repeat (econstructor; eauto). - - repeat (econstructor; eauto). - Qed. - - (* TODO: can we consider removing gm entirely? - We don't have backreferences, and we use it for reversal, the resulting group maps make no sense anyway. *) - + (** * NoPrio Tree Equivalence *) Lemma two_app: @@ -166,120 +127,124 @@ Section NoPrioSemantics. (* all leaves obtained from noprio are leaves of the backtracking tree *) Theorem noprio_is_leaf: - forall dir r inp gm t leafinp leafgm + forall dir r inp gm t leafinp (TREE: is_tree rer [Areg r] inp gm dir t), - noprio dir inp gm r leafinp leafgm -> - In (leafinp, leafgm) (tree_leaves t gm inp dir). + noprio dir inp r leafinp -> + exists leafgm, In (leafinp, leafgm) (tree_leaves t gm inp dir). Proof. - intros dir r inp gm t leafinp leafgm TREE NP. - generalize dependent t. + intros dir r inp gm t leafinp TREE NP. + generalize dependent t. generalize dependent gm. induction NP; intros. - inversion TREE; subst. inversion ISTREE; subst. - simpl. auto. + simpl. eauto. - inversion TREE; subst; rewrite READ0 in READ; inversion READ; subst. inversion TREECONT; subst. simpl. apply read_char_success_advance in READ0. - unfold advance_input'. rewrite READ0. auto. - - inversion TREE; subst. apply IHNP in ISTREE1. - simpl. apply in_or_app. auto. - - inversion TREE; subst. apply IHNP in ISTREE2. - simpl. apply in_or_app. auto. + unfold advance_input'. rewrite READ0. eauto. + - inversion TREE; subst. apply IHNP in ISTREE1 as [leafgm IH1]. + simpl. eexists. apply in_or_app. eauto. + - inversion TREE; subst. apply IHNP in ISTREE2 as [leafgm IH2]. + simpl. eexists. apply in_or_app. eauto. - inversion TREE; subst. simpl in CONT. rewrite two_app in CONT. - specialize (is_tree_productivity rer [Areg r1] inp0 gm0 forward) as [t1 HT1]. + specialize (is_tree_productivity rer [Areg r1] inp0 gm forward) as [t1 HT1]. + apply IHNP1 in HT1 as H. destruct H as [gm1 IN1]. specialize (is_tree_productivity rer [Areg r2] inp1 gm1 forward) as [t2 HT2]. - eapply in_leaves_app; eauto. + apply IHNP2 in HT2 as H. destruct H as [gm2 IN2]. + eexists. eapply in_leaves_app; eauto. - inversion TREE; subst. simpl in CONT. rewrite two_app in CONT. - specialize (is_tree_productivity rer [Areg r2] inp0 gm0 backward) as [t1 HT1]. - specialize (is_tree_productivity rer [Areg r1] inp1 gm1 backward) as [t2 HT2]. - eapply in_leaves_app; eauto. + specialize (is_tree_productivity rer [Areg r2] inp0 gm backward) as [t2 HT2]. + apply IHNP1 in HT2 as H. destruct H as [gm2 IN2]. + specialize (is_tree_productivity rer [Areg r1] inp1 gm2 backward) as [t1 HT1]. + apply IHNP2 in HT1 as H. destruct H as [gm1 IN1]. + eexists. eapply in_leaves_app; eauto. - inversion TREE; subst. rewrite two_app in ISTREE1. - specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm0) dir) as [t1 HT1]. + specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm) dir) as [t1 HT1]. + assert (IN1: exists gm1, In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm) inp0 dir)). + { apply IHNP1. auto. } destruct IN1 as [gm1 IN1]. specialize (is_tree_productivity rer [Areg (Quantified greedy min delta r)] inp1 gm1 dir) as [t2 HT2]. - assert (IN1: In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm0) inp0 dir)). - { apply IHNP1. auto. } - assert (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 dir)). - { apply IHNP2. auto. } - eapply (in_leaves_app _ _ _ _ _ inp2 gm2 _ _ _ _ _ ISTREE1 HT1 HT2 IN1 IN2); eauto. + assert (IN2: exists gm2, In (inp2, gm2) (tree_leaves t2 gm1 inp1 dir)). + { apply IHNP2. auto. } destruct IN2 as [gm2 IN2]. + eexists. eapply (in_leaves_app _ _ _ _ _ inp2 gm2 _ _ _ _ _ ISTREE1 HT1 HT2 IN1 IN2); eauto. - inversion TREE; subst. - + inversion SKIP; subst. simpl. auto. + + inversion SKIP; subst. simpl. eauto. + destruct plus; inversion H1. - inversion TREE; subst. { destruct delta; inversion H1. } assert (DP: plus = delta). { destruct plus; destruct delta; auto; inversion H1; auto. } subst. clear H1. clear SKIP. - specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm0) dir) as [t1 HT1]. + specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm) dir) as [t1 HT1]. + assert (IN1: exists gm1, In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm) inp0 dir)). + { apply IHNP1. auto. } destruct IN1 as [gm1 IN1]. specialize (is_tree_productivity rer [Acheck inp0] inp1 gm1 dir) as [t2 HT2]. - specialize (is_tree_productivity rer [Areg (Quantified greedy 0 delta r)] inp1 gm1 dir) as [t3 HT3]. - assert (IN1: In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm0) inp0 dir)). - { apply IHNP1. auto. } assert (IN2: In (inp1, gm1) (tree_leaves t2 gm1 inp1 dir)). { inversion HT2; subst. - inversion TREECONT; subst. simpl. auto. - apply CHECKFAIL in PROGRESS. inversion PROGRESS. (* we know progress happened *) } - assert (IN3: In (inp2, gm2) (tree_leaves t3 gm1 inp1 dir)). - { apply IHNP2. auto. } + specialize (is_tree_productivity rer [Areg (Quantified greedy 0 delta r)] inp1 gm1 dir) as [t3 HT3]. + assert (IN3: exists gm2, In (inp2, gm2) (tree_leaves t3 gm1 inp1 dir)). + { apply IHNP2. auto. } destruct IN3 as [gm2 IN3]. rewrite three_app in ISTREE1. destruct greedy; simpl. - + apply in_or_app. left. + + eexists. apply in_or_app. left. eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). - + apply in_or_app. right. + + eexists. apply in_or_app. right. eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). - inversion TREE; subst. { destruct delta; inversion H1. } inversion SKIP. subst. - destruct greedy; simpl; auto. - apply in_or_app; simpl; auto. + destruct greedy; simpl; eauto. + eexists. apply in_or_app; simpl; eauto. - inversion TREE; subst. rewrite two_app in TREECONT. specialize (is_tree_productivity rer [Areg r] inp (GroupMap.open (idx inp) gid gm) dir) as [t1 HT1]. + assert (IN1: exists nextgm, In (nextinp, nextgm) (tree_leaves t1 (GroupMap.open (idx inp) gid gm) inp dir)). + { apply IHNP. auto. } destruct IN1 as [nextgm IN1]. specialize (is_tree_productivity rer [Aclose gid] nextinp nextgm dir) as [t2 HT2]. - assert (IN1: In (nextinp, nextgm) (tree_leaves t1 (GroupMap.open (idx inp) gid gm) inp dir)). - { apply IHNP. auto. } assert (IN2: In (nextinp, GroupMap.close (idx nextinp) gid nextgm) (tree_leaves t2 nextgm nextinp dir)). { inversion HT2. subst. inversion TREECONT0. subst. simpl. auto. } - eapply (in_leaves_app _ _ _ _ _ nextinp (GroupMap.close (idx nextinp) gid nextgm) _ _ _ _ _ TREECONT HT1 HT2 IN1 IN2); eauto. + eexists. eapply (in_leaves_app _ _ _ _ _ nextinp (GroupMap.close (idx nextinp) gid nextgm) _ _ _ _ _ TREECONT HT1 HT2 IN1 IN2); eauto. - inversion TREE; subst; rewrite ANCHOR0 in ANCHOR; inversion ANCHOR. - inversion TREECONT; subst. simpl. auto. + inversion TREECONT; subst. simpl. eauto. Qed. (* Other direction: generalizing the noprio semantics to actions *) - Inductive noprio_action: Direction -> input -> group_map -> action -> input -> group_map -> Prop := + Inductive noprio_action: Direction -> input -> action -> input -> Prop := | np_regex: - forall dir inp gm r nextinp nextgm - (NP: noprio dir inp gm r nextinp nextgm), - noprio_action dir inp gm (Areg r) nextinp nextgm + forall dir inp r nextinp + (NP: noprio dir inp r nextinp), + noprio_action dir inp (Areg r) nextinp | np_close: - forall dir inp gm gid, - noprio_action dir inp gm (Aclose gid) inp (GroupMap.close (idx inp) gid gm) + forall dir inp gid, + noprio_action dir inp (Aclose gid) inp | np_check: - forall dir inp gm inpcheck + forall dir inp inpcheck (PROGRESS: strict_suffix inp inpcheck dir), - noprio_action dir inp gm (Acheck inpcheck) inp gm. + noprio_action dir inp (Acheck inpcheck) inp. - Inductive noprio_list: Direction -> input -> group_map -> list action -> input -> group_map -> Prop := + Inductive noprio_list: Direction -> input -> list action -> input -> Prop := | np_nil: - forall dir inp gm, - noprio_list dir inp gm [] inp gm + forall dir inp, + noprio_list dir inp [] inp | np_cons: - forall dir inp0 gm0 a inp1 gm1 l inp2 gm2 - (NP_A: noprio_action dir inp0 gm0 a inp1 gm1) - (NP_L: noprio_list dir inp1 gm1 l inp2 gm2), - noprio_list dir inp0 gm0 (a::l) inp2 gm2. + forall dir inp0 a inp1 l inp2 + (NP_A: noprio_action dir inp0 a inp1) + (NP_L: noprio_list dir inp1 l inp2), + noprio_list dir inp0 (a::l) inp2. Lemma is_tree_action_noprio: forall dir inp0 gm0 l t inp1 gm1 (SUBSET: pike_actions l) (TREE: is_tree rer l inp0 gm0 dir t) (LEAF: In (inp1, gm1) (tree_leaves t gm0 inp0 dir)), - noprio_list dir inp0 gm0 l inp1 gm1. + noprio_list dir inp0 l inp1. Proof. intros dir inp0 gm0 l t inp1 gm1 SUBSET TREE LEAF. induction TREE; simpl in LEAF; subst; @@ -293,20 +258,20 @@ Section NoPrioSemantics. unfold advance_input' in LEAF. rewrite ADV in LEAF. eauto. } repeat (econstructor; eauto). - apply in_app_or in LEAF as [LEAF|LEAF]. - + assert (noprio_list dir inp gm (Areg r1::cont) inp1 gm1). + + assert (noprio_list dir inp (Areg r1::cont) inp1). { apply IHTREE1; auto. pike_subset. } inversion H; subst. inversion NP_A. repeat (econstructor; eauto). - + assert (noprio_list dir inp gm (Areg r2::cont) inp1 gm1). + + assert (noprio_list dir inp (Areg r2::cont) inp1). { apply IHTREE2; auto. pike_subset. } inversion H; subst. inversion NP_A. solve[repeat (econstructor; eauto)]. - destruct dir. + simpl in IHTREE. - assert (noprio_list forward inp gm (Areg r1 :: Areg r2 :: cont) inp1 gm1). + assert (noprio_list forward inp (Areg r1 :: Areg r2 :: cont) inp1). { apply IHTREE; auto. pike_subset. } inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; subst. repeat (econstructor; eauto). + simpl in IHTREE. - assert (noprio_list backward inp gm (Areg r2 :: Areg r1 :: cont) inp1 gm1). + assert (noprio_list backward inp (Areg r2 :: Areg r1 :: cont) inp1). { apply IHTREE; auto. pike_subset. } inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; subst. repeat (econstructor; eauto). @@ -321,7 +286,7 @@ Section NoPrioSemantics. (* skip *) 2: { econstructor; eauto. econstructor; eauto. apply np_quant_skip. } (* iter *) - assert (noprio_list dir inp (GroupMap.reset (def_groups r1) gm) (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 +∞ r1) :: cont) inp1 gm1). + assert (noprio_list dir inp (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 +∞ r1) :: cont) inp1). { apply IHTREE1; auto. pike_subset. } inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; inversion NP_L0; inversion NP_A1; subst. repeat (econstructor; eauto). @@ -334,12 +299,12 @@ Section NoPrioSemantics. (* skip *) 2: { econstructor; eauto. econstructor; eauto. apply np_quant_skip. } (* iter *) - assert (noprio_list dir inp (GroupMap.reset (def_groups r1) gm) (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 (NoI.N 0) r1) :: cont) inp1 gm1). + assert (noprio_list dir inp (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 (NoI.N 0) r1) :: cont) inp1). { apply IHTREE1; auto. pike_subset. } inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; inversion NP_L0; inversion NP_A1; subst. repeat (econstructor; eauto). - destruct plus; inversion H3. - - assert (noprio_list dir inp (GroupMap.open (idx inp) gid gm) (Areg r1 :: Aclose gid :: cont) inp1 gm1). + - assert (noprio_list dir inp (Areg r1 :: Aclose gid :: cont) inp1). { apply IHTREE; auto. pike_subset. } inversion H; inversion NP_A; inversion NP_L; inversion NP_A0; subst. repeat (econstructor; eauto). @@ -349,19 +314,126 @@ Section NoPrioSemantics. (* For the Pike Subset, the NoPrio Semantics exactly coincides with leaves of the Tree Semantics *) Theorem noprio_eq_is_leaf: - forall dir r inp gm t leafinp leafgm + forall dir r inp gm t leafinp (SUBSET: pike_regex r) (TREE: is_tree rer [Areg r] inp gm dir t), - noprio dir inp gm r leafinp leafgm <-> - In (leafinp, leafgm) (tree_leaves t gm inp dir). + noprio dir inp r leafinp <-> + exists leafgm, In (leafinp, leafgm) (tree_leaves t gm inp dir). Proof. - intros dir r inp gm t leafinp leafgm SUBSET TREE. split. + intros dir r inp gm t leafinp SUBSET TREE. split. - apply noprio_is_leaf. auto. - - intros. eapply is_tree_action_noprio in TREE; eauto. + - intros [leafgm H]. eapply is_tree_action_noprio in TREE; eauto. 2: pike_subset. inversion TREE; inversion NP_A; inversion NP_L; subst. auto. Qed. + (** * Quantifier Properties *) + + Lemma iteration_suffix: + forall dir r inp0 inp1 + (NP: noprio dir inp0 r inp1), + inp0 = inp1 \/ strict_suffix inp1 inp0 dir. + Proof. + intros dir r inp0 inp1 NP. induction NP; auto. + 1: { apply read_char_suffix in READ. auto. } + all: destruct IHNP1; destruct IHNP2; subst; auto; + right; eapply strict_suffix_trans; eauto. + Qed. + + (* In order to prove the reversal property, we characterize quantifiers in the nopriority semantics *) + + (* n iterations of a regex *) + Inductive iters : nat -> Direction -> input -> regex -> input -> Prop := + | iters_refl: + forall inp r dir, iters 0 dir inp r inp + | iters_next: + forall r n inp0 inp1 inp2 dir + (NEXT: noprio dir inp0 r inp1) + (ITERS: iters n dir inp1 r inp2), + iters (S n) dir inp0 r inp2. + + (* is n <= min + delta ? *) + Inductive smaller: nat -> nat -> non_neg_integer_or_inf -> Prop := + | smaller_nat: forall n min delta, + n <= min + delta -> + smaller n min (NoI.N delta) + | smaller_inf: forall n min, + smaller n min NoI.Inf. + + (* a characterization of quantifiers using numbered iterations *) + Lemma quant_iters: + forall r dir greedy inp0 inp1 min delta + (QUANT: noprio dir inp0 (Quantified greedy min delta r) inp1), + exists n, n >= min /\ smaller n min delta /\ iters n dir inp0 r inp1. + Proof. + intros r dir greedy inp0 inp1 min delta QUANT. + remember (Quantified greedy min delta r) as quant. + generalize dependent min. generalize dependent delta. + induction QUANT; intros; + inversion Heqquant; subst. + - clear IHQUANT1. + specialize (IHQUANT2 delta0 min (eq_refl _)) as [n [GE [LE IT]]]. + exists (S n). split; [lia|]. split. + { inversion LE; subst; constructor. lia. } + econstructor; eauto. + - exists 0. split; [lia|]. split; constructor; auto. + - clear IHQUANT1. specialize (IHQUANT2 delta 0 (eq_refl _)) as [n [GE [LE IT]]]. + exists (S n). split; [lia|]. split. + { inversion LE; subst; constructor. lia. } + econstructor; eauto. + - exists 0. split; [lia|]. split. + { destruct delta; constructor. lia. } + constructor. + Qed. + + Lemma iters_quant: + forall r dir greedy inp0 inp1 min delta n + (GE: n >= min) + (LE: smaller n min delta) + (ITERS: iters n dir inp0 r inp1), + noprio dir inp0 (Quantified greedy min delta r) inp1. + Proof. + intros r dir greedy inp0 inp1 min delta n GE LE ITERS. + generalize dependent min. generalize dependent delta. + induction ITERS; intros. + - destruct min; inversion GE. inversion LE; subst. + + destruct delta0. + * apply np_quant_done. + * replace (NoI.N (S delta0)) with (NoI.N 1 + NoI.N delta0)%NoI by auto. + apply np_quant_skip. + + replace NoI.Inf with (NoI.N 1 + NoI.Inf)%NoI by auto. + apply np_quant_skip. + - destruct min. + (* forced iteration *) + 2:{ eapply np_quant_forced; eauto. apply IHITERS. lia. + inversion LE; subst; constructor. lia. } + (* free iteration: cas analysis on if the first iteration did progress *) + apply iteration_suffix in NEXT as H. destruct H as [EQ|SUF]. + + (* first iteration didn't progress: we skip it in the quantifier *) + subst. apply IHITERS. lia. inversion LE; subst; constructor. lia. + + (* first iteration made progress: we can use it as a quantifier iteration *) + inversion LE; subst. + * destruct delta0; [lia|]. + replace (NoI.N (S delta0)) with (NoI.N 1 + NoI.N delta0)%NoI by auto. + eapply np_quant_free; eauto. apply IHITERS. lia. + constructor. lia. + * replace NoI.Inf with (NoI.N 1 + NoI.Inf)%NoI by auto. + eapply np_quant_free; eauto. apply IHITERS. lia. + constructor. + Qed. + + (* Adding an iteration at the end *) + Lemma add_iter_end: + forall dir r n inp0 inp1 inp2 + (ITERS: iters n dir inp0 r inp1) + (NEXT: noprio dir inp1 r inp2), + iters (S n) dir inp0 r inp2. + Proof. + intros. induction ITERS; repeat (econstructor; eauto). + Qed. + + + (** * Reversal Property *) Definition reverse (d:Direction): Direction := @@ -384,75 +456,54 @@ Section NoPrioSemantics. destruct (char_match) eqn:CM; inversion H. subst. rewrite CM. auto. Qed. - - Theorem noprio_reversal: - forall dir r inp1 inp2 gma gmb - (NP1: noprio dir inp1 gma r inp2 gmb), - forall gmc, exists gmd, noprio (reverse dir) inp2 gmc r inp1 gmd. - Proof. - intros dir r. - induction r; intros. - - inversion NP1. subst. repeat (econstructor; eauto). - - inversion NP1. subst. - apply read_char_reverse in READ as REV. - repeat (econstructor; eauto). - - inversion NP1; subst. - + eapply IHr1 in LEFT as [gmd H]. repeat (econstructor; eauto). - + eapply IHr2 in RIGHT as [gmd H]. solve[repeat (econstructor; eauto)]. - - inversion NP1; subst; simpl in *. - + apply IHr2 with (gmc:=gmc) in SEQ2 as [gmd H2]. - apply IHr1 with (gmc:=gmd) in SEQ1 as H1. destruct H1 as [gme H1]. - (* ah! why doesn't the intro pattern work here? *) - repeat (econstructor; eauto). - + apply IHr1 with (gmc:=gmc) in SEQ2 as [gmd H2]. - apply IHr2 with (gmc:=gmd) in SEQ1 as H1. destruct H1 as [gme H1]. - repeat (econstructor; eauto). - - inversion NP1; subst. - + (* forced *) - (* induction over r fails: r{min} is not a subregex of r{min+1} *) - admit. - + (* done *) - repeat (econstructor; eauto). - + (* free *) - admit. - + (* skip *) - exists gmc. apply np_quant_skip. - - inversion NP1. - - inversion NP1. subst. - eapply IHr in GROUP as [gmd H]. - repeat (econstructor; eauto). - - inversion NP1. subst. - repeat (econstructor; eauto). - - inversion NP1. - Abort. - Theorem noprio_reversal: - forall dir r inp1 inp2 gma gmb - (NP1: noprio dir inp1 gma r inp2 gmb), - forall gmc, exists gmd, noprio (reverse dir) inp2 gmc r inp1 gmd. + forall dir r inp1 inp2 + (NP1: noprio dir inp1 r inp2), + noprio (reverse dir) inp2 r inp1. Proof. - intros dir r inp1 inp2 gma gmb NP1 gmc. - generalize dependent gmc. induction NP1; intros. + intros dir r inp1 inp2 NP1. + induction NP1; intros. - repeat (econstructor; eauto). - apply read_char_reverse in READ as REV. - destruct dir; simpl; exists gmc; econstructor; eauto. - - destruct (IHNP1 gmc) as [gmd H]. eexists. apply np_disj_left. eauto. - - destruct (IHNP1 gmc) as [gmd H]. eexists. apply np_disj_right. eauto. - - destruct (IHNP1_2 gmc) as [gmd H2]. destruct (IHNP1_1 gmd) as [gme H1]. - repeat (econstructor; eauto). - - destruct (IHNP1_2 gmc) as [gmd H1]. destruct (IHNP1_1 gmd) as [gme H2]. - repeat (econstructor; eauto). - - admit. - (* does not work: in one direction we do r and then r{min} - in the other we also do r and then r{min}, but we would like them switched to apply IH. - One solution would be to prove that for noprio, r.r{} is equivalent to r{}.r *) + destruct dir; simpl; econstructor; eauto. + - repeat (econstructor; eauto). + - solve[repeat (econstructor; eauto)]. - repeat (econstructor; eauto). - - admit. - - eexists. eapply np_quant_skip. - - destruct (IHNP1 (GroupMap.open (idx nextinp) gid gmc)) as [gmd H1]. - repeat (econstructor; eauto). - repeat (econstructor; eauto). - Admitted. + - apply quant_iters in IHNP1_2 as [n [GE [LE IT]]]. + apply iters_quant with (n:= S n); auto. lia. + { inversion LE; subst; constructor. lia. } + eapply add_iter_end; eauto. + - repeat (econstructor; eauto). + - apply quant_iters in IHNP1_2 as [n [GE [LE IT]]]. + apply iters_quant with (n:=S n); auto. + { inversion LE; subst; constructor. lia. } + eapply add_iter_end; eauto. + - eapply np_quant_skip. + - repeat (econstructor; eauto). + - repeat (econstructor; eauto). + Qed. + + (** * Leaf Reversal Theorem *) + + (* We come back to is_tree semantics to prove the reversal property *) + Lemma leaf_reversal: + forall r dir inp1 inp2 gm2 t1 t2 + (SUBSET: pike_regex r) + (TREE1: is_tree rer [Areg r] inp1 GroupMap.empty dir t1) + (TREE2: is_tree rer [Areg r] inp2 GroupMap.empty (reverse dir) t2) + (IN: In (inp2, gm2) (tree_leaves t1 GroupMap.empty inp1 dir)), + exists gm1, In (inp1, gm1) (tree_leaves t2 GroupMap.empty inp2 (reverse dir)). + Proof. + intros r dir inp1 inp2 gm2 t1 t2 SUBSET TREE1 TREE2 IN. + assert (NP1: noprio dir inp1 r inp2). + { apply <- noprio_eq_is_leaf; eauto. } + apply noprio_reversal in NP1 as NP2. + assert (IN2: exists leafgm, In (inp1, leafgm) (tree_leaves t2 GroupMap.empty inp2 (reverse dir))). + { eapply noprio_eq_is_leaf; eauto. } + eauto. + Qed. + End NoPrioSemantics. diff --git a/Engine/NoPrioSemantics2.v b/Engine/NoPrioSemantics2.v deleted file mode 100644 index d19315c..0000000 --- a/Engine/NoPrioSemantics2.v +++ /dev/null @@ -1,509 +0,0 @@ -From Stdlib Require Import List Lia. -Import ListNotations. - -From Linden Require Import Regex Chars Groups. -From Linden Require Import Tree Semantics PikeSubset. -From Warblre Require Import Base RegExpRecord. -From Linden Require Import StrictSuffix. -From Linden Require Import FunctionalSemantics. -From Linden Require Import ComputeIsTree. -From Linden Require Import Parameters. -From Linden Require Import FlatMap Equivalence FunctionalUtils. - - -(* A rephrasing of the semantics, where priority does not matter *) -(* It's a relation about leaves, not necessarily the first one *) -(* There are no actions, the shape of the regex determines the relation *) -(* For this version, we don't veen consider group_maps (although we could compute them along the way) - Because for the reversal property we don't need them. *) - -Section NoPrioSemantics. - Context {params: LindenParameters}. - Context (rer: RegExpRecord). - - Inductive noprio: Direction -> input -> regex -> input -> Prop := - | np_eps: - forall dir inp, - noprio dir inp Epsilon inp - | np_char: - forall dir inp cd c nextinp - (READ: read_char rer cd inp dir = Some (c, nextinp)), - noprio dir inp (Regex.Character cd) nextinp - | np_disj_left: - forall dir inp r1 r2 nextinp - (LEFT: noprio dir inp r1 nextinp), - noprio dir inp (Disjunction r1 r2) nextinp - | np_disj_right: - forall dir inp r1 r2 nextinp - (RIGHT: noprio dir inp r2 nextinp), - noprio dir inp (Disjunction r1 r2) nextinp - | np_seq_forward: - forall inp0 r1 r2 inp1 inp2 - (SEQ1: noprio forward inp0 r1 inp1) - (SEQ2: noprio forward inp1 r2 inp2), - noprio forward inp0 (Sequence r1 r2) inp2 - | np_seq_backward: - forall inp0 r1 r2 inp1 inp2 - (SEQ1: noprio backward inp0 r2 inp1) - (SEQ2: noprio backward inp1 r1 inp2), - noprio backward inp0 (Sequence r1 r2) inp2 - | np_quant_forced: - forall dir inp0 r min delta greedy inp1 inp2 - (ITER: noprio dir inp0 r inp1) - (LOOP: noprio dir inp1 (Quantified greedy min delta r) inp2), - noprio dir inp0 (Quantified greedy (S min) delta r) inp2 - | np_quant_done: - forall dir inp r greedy, - noprio dir inp (Quantified greedy 0 (NoI.N 0) r) inp - | np_quant_free: - forall dir inp0 r greedy delta inp1 inp2 - (ITER: noprio dir inp0 r inp1) - (PROGRESS: strict_suffix inp1 inp0 dir) - (LOOP: noprio dir inp1 (Quantified greedy 0 delta r) inp2), - noprio dir inp0 (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp2 - | np_quant_skip: - forall dir inp r greedy delta, - noprio dir inp (Quantified greedy 0 (NoI.N 1 + delta)%NoI r) inp - | np_group: - forall dir inp r gid nextinp - (GROUP: noprio dir inp r nextinp), - noprio dir inp (Group gid r) nextinp - | np_anchor: - forall dir inp a - (ANCHOR: anchor_satisfied rer a inp = true), - noprio dir inp (Anchor a) inp. - - (* LATER: there will be an issue if we want to add negative lookarounds: strict positivity *) - (* We might want to declare an oracle version of this, since this reversal is used in engines when we already know about the values of deeper lookarounds. *) - - (** * NoPrio Tree Equivalence *) - - Lemma two_app: - forall A (a1 a2:A), [a1; a2] = [a1] ++ [a2]. - Proof. auto. Qed. - - Lemma three_app: - forall A (a1 a2 a3:A), [a1; a2; a3] = [a1] ++ [a2] ++ [a3]. - Proof. auto. Qed. - - (* If we can find a leaf in the tree of the first list of actions, - then a leaf in the tree of the second list, - then that final leaf is a leaf of the tree of the concatenation *) - Lemma in_leaves_app: - forall dir inp0 gm0 inp1 gm1 inp2 gm2 a1 a2 t1 t2 t12 - (TREE12: is_tree rer (a1 ++ a2) inp0 gm0 dir t12) - (TREE1: is_tree rer a1 inp0 gm0 dir t1) - (TREE2: is_tree rer a2 inp1 gm1 dir t2) - (IN1: In (inp1,gm1) (tree_leaves t1 gm0 inp0 dir)) - (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 dir)), - In (inp2, gm2) (tree_leaves t12 gm0 inp0 dir). - Proof. - intros dir inp0 gm0 inp1 gm1 inp2 gm2 a1 a2 t1 t2 t12 TREE12 TREE1 TREE2 IN1 IN2. - specialize (leaves_concat _ _ _ _ _ _ _ _ TREE12 TREE1) as FM. - assert (ACT: act_from_leaf rer a2 dir (inp1, gm1) (tree_leaves t2 gm1 inp1 dir)). - { constructor. simpl. auto. } - specialize (FlatMap_in _ _ _ _ _ (act_from_leaf_determ _ _ _) FM IN1 ACT) as FM_IN. - rewrite Forall_forall in FM_IN. - apply FM_IN. auto. - Qed. - - Lemma in_leaves_app3: - forall dir inp0 gm0 inp1 gm1 inp2 gm2 inp3 gm3 a1 a2 a3 t1 t2 t3 t123 - (TREE123: is_tree rer (a1 ++ a2 ++ a3) inp0 gm0 dir t123) - (TREE1: is_tree rer a1 inp0 gm0 dir t1) - (TREE2: is_tree rer a2 inp1 gm1 dir t2) - (TREE3: is_tree rer a3 inp2 gm2 dir t3) - (IN1: In (inp1,gm1) (tree_leaves t1 gm0 inp0 dir)) - (IN2: In (inp2, gm2) (tree_leaves t2 gm1 inp1 dir)) - (IN3: In (inp3, gm3) (tree_leaves t3 gm2 inp2 dir)), - In (inp3, gm3) (tree_leaves t123 gm0 inp0 dir). - Proof. - intros dir inp0 gm0 inp1 gm1 inp2 gm2 inp3 gm3 a1 a2 a3 t1 t2 t3 t123 TREE123 TREE1 TREE2 TREE3 IN1 IN2 IN3. - specialize (is_tree_productivity rer (a2 ++ a3) inp1 gm1 dir) as [t23 TREE23]. - assert (IN23: In (inp3, gm3) (tree_leaves t23 gm1 inp1 dir)). - { apply (in_leaves_app _ _ _ _ _ _ _ _ _ _ _ _ TREE23 TREE2 TREE3 IN2 IN3). } - apply (in_leaves_app _ _ _ _ _ _ _ _ _ _ _ _ TREE123 TREE1 TREE23 IN1 IN23). - Qed. - - (* all leaves obtained from noprio are leaves of the backtracking tree *) - Theorem noprio_is_leaf: - forall dir r inp gm t leafinp - (TREE: is_tree rer [Areg r] inp gm dir t), - noprio dir inp r leafinp -> - exists leafgm, In (leafinp, leafgm) (tree_leaves t gm inp dir). - Proof. - intros dir r inp gm t leafinp TREE NP. - generalize dependent t. generalize dependent gm. - induction NP; intros. - - inversion TREE; subst. inversion ISTREE; subst. - simpl. eauto. - - inversion TREE; subst; - rewrite READ0 in READ; inversion READ; subst. - inversion TREECONT; subst. simpl. - apply read_char_success_advance in READ0. - unfold advance_input'. rewrite READ0. eauto. - - inversion TREE; subst. apply IHNP in ISTREE1 as [leafgm IH1]. - simpl. eexists. apply in_or_app. eauto. - - inversion TREE; subst. apply IHNP in ISTREE2 as [leafgm IH2]. - simpl. eexists. apply in_or_app. eauto. - - inversion TREE; subst. - simpl in CONT. rewrite two_app in CONT. - specialize (is_tree_productivity rer [Areg r1] inp0 gm forward) as [t1 HT1]. - apply IHNP1 in HT1 as H. destruct H as [gm1 IN1]. - specialize (is_tree_productivity rer [Areg r2] inp1 gm1 forward) as [t2 HT2]. - apply IHNP2 in HT2 as H. destruct H as [gm2 IN2]. - eexists. eapply in_leaves_app; eauto. - - inversion TREE; subst. - simpl in CONT. rewrite two_app in CONT. - specialize (is_tree_productivity rer [Areg r2] inp0 gm backward) as [t2 HT2]. - apply IHNP1 in HT2 as H. destruct H as [gm2 IN2]. - specialize (is_tree_productivity rer [Areg r1] inp1 gm2 backward) as [t1 HT1]. - apply IHNP2 in HT1 as H. destruct H as [gm1 IN1]. - eexists. eapply in_leaves_app; eauto. - - inversion TREE; subst. - rewrite two_app in ISTREE1. - specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm) dir) as [t1 HT1]. - assert (IN1: exists gm1, In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm) inp0 dir)). - { apply IHNP1. auto. } destruct IN1 as [gm1 IN1]. - specialize (is_tree_productivity rer [Areg (Quantified greedy min delta r)] inp1 gm1 dir) as [t2 HT2]. - assert (IN2: exists gm2, In (inp2, gm2) (tree_leaves t2 gm1 inp1 dir)). - { apply IHNP2. auto. } destruct IN2 as [gm2 IN2]. - eexists. eapply (in_leaves_app _ _ _ _ _ inp2 gm2 _ _ _ _ _ ISTREE1 HT1 HT2 IN1 IN2); eauto. - - inversion TREE; subst. - + inversion SKIP; subst. simpl. eauto. - + destruct plus; inversion H1. - - inversion TREE; subst. - { destruct delta; inversion H1. } - assert (DP: plus = delta). - { destruct plus; destruct delta; auto; inversion H1; auto. } - subst. clear H1. clear SKIP. - specialize (is_tree_productivity rer [Areg r] inp0 (GroupMap.reset (def_groups r) gm) dir) as [t1 HT1]. - assert (IN1: exists gm1, In (inp1, gm1) (tree_leaves t1 (GroupMap.reset (def_groups r) gm) inp0 dir)). - { apply IHNP1. auto. } destruct IN1 as [gm1 IN1]. - specialize (is_tree_productivity rer [Acheck inp0] inp1 gm1 dir) as [t2 HT2]. - assert (IN2: In (inp1, gm1) (tree_leaves t2 gm1 inp1 dir)). - { inversion HT2; subst. - - inversion TREECONT; subst. simpl. auto. - - apply CHECKFAIL in PROGRESS. inversion PROGRESS. (* we know progress happened *) - } - specialize (is_tree_productivity rer [Areg (Quantified greedy 0 delta r)] inp1 gm1 dir) as [t3 HT3]. - assert (IN3: exists gm2, In (inp2, gm2) (tree_leaves t3 gm1 inp1 dir)). - { apply IHNP2. auto. } destruct IN3 as [gm2 IN3]. - rewrite three_app in ISTREE1. - destruct greedy; simpl. - + eexists. apply in_or_app. left. - eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). - + eexists. apply in_or_app. right. - eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). - - inversion TREE; subst. - { destruct delta; inversion H1. } - inversion SKIP. subst. - destruct greedy; simpl; eauto. - eexists. apply in_or_app; simpl; eauto. - - inversion TREE; subst. - rewrite two_app in TREECONT. - specialize (is_tree_productivity rer [Areg r] inp (GroupMap.open (idx inp) gid gm) dir) as [t1 HT1]. - assert (IN1: exists nextgm, In (nextinp, nextgm) (tree_leaves t1 (GroupMap.open (idx inp) gid gm) inp dir)). - { apply IHNP. auto. } destruct IN1 as [nextgm IN1]. - specialize (is_tree_productivity rer [Aclose gid] nextinp nextgm dir) as [t2 HT2]. - assert (IN2: In (nextinp, GroupMap.close (idx nextinp) gid nextgm) (tree_leaves t2 nextgm nextinp dir)). - { inversion HT2. subst. inversion TREECONT0. subst. simpl. auto. } - eexists. eapply (in_leaves_app _ _ _ _ _ nextinp (GroupMap.close (idx nextinp) gid nextgm) _ _ _ _ _ TREECONT HT1 HT2 IN1 IN2); eauto. - - inversion TREE; subst; - rewrite ANCHOR0 in ANCHOR; inversion ANCHOR. - inversion TREECONT; subst. simpl. eauto. - Qed. - - (* Other direction: generalizing the noprio semantics to actions *) - - Inductive noprio_action: Direction -> input -> action -> input -> Prop := - | np_regex: - forall dir inp r nextinp - (NP: noprio dir inp r nextinp), - noprio_action dir inp (Areg r) nextinp - | np_close: - forall dir inp gid, - noprio_action dir inp (Aclose gid) inp - | np_check: - forall dir inp inpcheck - (PROGRESS: strict_suffix inp inpcheck dir), - noprio_action dir inp (Acheck inpcheck) inp. - - Inductive noprio_list: Direction -> input -> list action -> input -> Prop := - | np_nil: - forall dir inp, - noprio_list dir inp [] inp - | np_cons: - forall dir inp0 a inp1 l inp2 - (NP_A: noprio_action dir inp0 a inp1) - (NP_L: noprio_list dir inp1 l inp2), - noprio_list dir inp0 (a::l) inp2. - - Lemma is_tree_action_noprio: - forall dir inp0 gm0 l t inp1 gm1 - (SUBSET: pike_actions l) - (TREE: is_tree rer l inp0 gm0 dir t) - (LEAF: In (inp1, gm1) (tree_leaves t gm0 inp0 dir)), - noprio_list dir inp0 l inp1. - Proof. - intros dir inp0 gm0 l t inp1 gm1 SUBSET TREE LEAF. - induction TREE; simpl in LEAF; subst; - try solve [inversion LEAF]; pike_subset. - - destruct LEAF as [LEAF|LEAF]; inversion LEAF; subst. constructor. - - repeat (econstructor; eauto). - - repeat (econstructor; eauto). - - repeat (econstructor; eauto). - - econstructor; eauto. - 2: { apply read_char_success_advance in READ as ADV. - unfold advance_input' in LEAF. rewrite ADV in LEAF. eauto. } - repeat (econstructor; eauto). - - apply in_app_or in LEAF as [LEAF|LEAF]. - + assert (noprio_list dir inp (Areg r1::cont) inp1). - { apply IHTREE1; auto. pike_subset. } - inversion H; subst. inversion NP_A. repeat (econstructor; eauto). - + assert (noprio_list dir inp (Areg r2::cont) inp1). - { apply IHTREE2; auto. pike_subset. } - inversion H; subst. inversion NP_A. solve[repeat (econstructor; eauto)]. - - destruct dir. - + simpl in IHTREE. - assert (noprio_list forward inp (Areg r1 :: Areg r2 :: cont) inp1). - { apply IHTREE; auto. pike_subset. } - inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; subst. - repeat (econstructor; eauto). - + simpl in IHTREE. - assert (noprio_list backward inp (Areg r2 :: Areg r1 :: cont) inp1). - { apply IHTREE; auto. pike_subset. } - inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; subst. - repeat (econstructor; eauto). - - specialize (IHTREE H2 LEAF). - repeat econstructor; eauto. - - destruct plus; inversion H3; subst. - specialize (IHTREE2 H2). - assert (In (inp1,gm1) (tree_leaves titer (GroupMap.reset (def_groups r1) gm) inp dir) \/ - In (inp1,gm1) (tree_leaves tskip gm inp dir)) as [LEAFSKIP|LEAFITER]. - { destruct greedy; simpl in LEAF; apply in_app_or in LEAF; auto. - destruct LEAF; auto. } - (* skip *) - 2: { econstructor; eauto. econstructor; eauto. apply np_quant_skip. } - (* iter *) - assert (noprio_list dir inp (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 +∞ r1) :: cont) inp1). - { apply IHTREE1; auto. pike_subset. } - inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; inversion NP_L0; inversion NP_A1; subst. - repeat (econstructor; eauto). - - destruct plus; inversion H3. subst. - specialize (IHTREE2 H2). - assert (In (inp1,gm1) (tree_leaves titer (GroupMap.reset (def_groups r1) gm) inp dir) \/ - In (inp1,gm1) (tree_leaves tskip gm inp dir)) as [LEAFSKIP|LEAFITER]. - { destruct greedy; simpl in LEAF; apply in_app_or in LEAF; auto. - destruct LEAF; auto. } - (* skip *) - 2: { econstructor; eauto. econstructor; eauto. apply np_quant_skip. } - (* iter *) - assert (noprio_list dir inp (Areg r1 :: Acheck inp :: Areg (Quantified greedy 0 (NoI.N 0) r1) :: cont) inp1). - { apply IHTREE1; auto. pike_subset. } - inversion H; inversion NP_L; inversion NP_A; inversion NP_A0; inversion NP_L0; inversion NP_A1; subst. - repeat (econstructor; eauto). - - destruct plus; inversion H3. - - assert (noprio_list dir inp (Areg r1 :: Aclose gid :: cont) inp1). - { apply IHTREE; auto. pike_subset. } - inversion H; inversion NP_A; inversion NP_L; inversion NP_A0; subst. - repeat (econstructor; eauto). - - specialize (IHTREE H2 LEAF). - repeat (econstructor; eauto). - Qed. - - (* For the Pike Subset, the NoPrio Semantics exactly coincides with leaves of the Tree Semantics *) - Theorem noprio_eq_is_leaf: - forall dir r inp gm t leafinp - (SUBSET: pike_regex r) - (TREE: is_tree rer [Areg r] inp gm dir t), - noprio dir inp r leafinp <-> - exists leafgm, In (leafinp, leafgm) (tree_leaves t gm inp dir). - Proof. - intros dir r inp gm t leafinp SUBSET TREE. split. - - apply noprio_is_leaf. auto. - - intros [leafgm H]. eapply is_tree_action_noprio in TREE; eauto. - 2: pike_subset. - inversion TREE; inversion NP_A; inversion NP_L; subst. auto. - Qed. - - (** * Quantifier Properties *) - - Lemma iteration_suffix: - forall dir r inp0 inp1 - (NP: noprio dir inp0 r inp1), - inp0 = inp1 \/ strict_suffix inp1 inp0 dir. - Proof. - intros dir r inp0 inp1 NP. induction NP; auto. - 1: { apply read_char_suffix in READ. auto. } - all: destruct IHNP1; destruct IHNP2; subst; auto; - right; eapply strict_suffix_trans; eauto. - Qed. - - (* In order to prove the reversal property, we characterize quantifiers in the nopriority semantics *) - - (* n iterations of a regex *) - Inductive iters : nat -> Direction -> input -> regex -> input -> Prop := - | iters_refl: - forall inp r dir, iters 0 dir inp r inp - | iters_next: - forall r n inp0 inp1 inp2 dir - (NEXT: noprio dir inp0 r inp1) - (ITERS: iters n dir inp1 r inp2), - iters (S n) dir inp0 r inp2. - - (* is n <= min + delta ? *) - Inductive smaller: nat -> nat -> non_neg_integer_or_inf -> Prop := - | smaller_nat: forall n min delta, - n <= min + delta -> - smaller n min (NoI.N delta) - | smaller_inf: forall n min, - smaller n min NoI.Inf. - - (* a characterization of quantifiers using numbered iterations *) - Lemma quant_iters: - forall r dir greedy inp0 inp1 min delta - (QUANT: noprio dir inp0 (Quantified greedy min delta r) inp1), - exists n, n >= min /\ smaller n min delta /\ iters n dir inp0 r inp1. - Proof. - intros r dir greedy inp0 inp1 min delta QUANT. - remember (Quantified greedy min delta r) as quant. - generalize dependent min. generalize dependent delta. - induction QUANT; intros; - inversion Heqquant; subst. - - clear IHQUANT1. - specialize (IHQUANT2 delta0 min (eq_refl _)) as [n [GE [LE IT]]]. - exists (S n). split; [lia|]. split. - { inversion LE; subst; constructor. lia. } - econstructor; eauto. - - exists 0. split; [lia|]. split; constructor; auto. - - clear IHQUANT1. specialize (IHQUANT2 delta 0 (eq_refl _)) as [n [GE [LE IT]]]. - exists (S n). split; [lia|]. split. - { inversion LE; subst; constructor. lia. } - econstructor; eauto. - - exists 0. split; [lia|]. split. - { destruct delta; constructor. lia. } - constructor. - Qed. - - Lemma iters_quant: - forall r dir greedy inp0 inp1 min delta n - (GE: n >= min) - (LE: smaller n min delta) - (ITERS: iters n dir inp0 r inp1), - noprio dir inp0 (Quantified greedy min delta r) inp1. - Proof. - intros r dir greedy inp0 inp1 min delta n GE LE ITERS. - generalize dependent min. generalize dependent delta. - induction ITERS; intros. - - destruct min; inversion GE. inversion LE; subst. - + destruct delta0. - * apply np_quant_done. - * replace (NoI.N (S delta0)) with (NoI.N 1 + NoI.N delta0)%NoI by auto. - apply np_quant_skip. - + replace NoI.Inf with (NoI.N 1 + NoI.Inf)%NoI by auto. - apply np_quant_skip. - - destruct min. - (* forced iteration *) - 2:{ eapply np_quant_forced; eauto. apply IHITERS. lia. - inversion LE; subst; constructor. lia. } - (* free iteration: cas analysis on if the first iteration did progress *) - apply iteration_suffix in NEXT as H. destruct H as [EQ|SUF]. - + (* first iteration didn't progress: we skip it in the quantifier *) - subst. apply IHITERS. lia. inversion LE; subst; constructor. lia. - + (* first iteration made progress: we can use it as a quantifier iteration *) - inversion LE; subst. - * destruct delta0; [lia|]. - replace (NoI.N (S delta0)) with (NoI.N 1 + NoI.N delta0)%NoI by auto. - eapply np_quant_free; eauto. apply IHITERS. lia. - constructor. lia. - * replace NoI.Inf with (NoI.N 1 + NoI.Inf)%NoI by auto. - eapply np_quant_free; eauto. apply IHITERS. lia. - constructor. - Qed. - - (* Adding an iteration at the end *) - Lemma add_iter_end: - forall dir r n inp0 inp1 inp2 - (ITERS: iters n dir inp0 r inp1) - (NEXT: noprio dir inp1 r inp2), - iters (S n) dir inp0 r inp2. - Proof. - intros. induction ITERS; repeat (econstructor; eauto). - Qed. - - - - (** * Reversal Property *) - - Definition reverse (d:Direction): Direction := - match d with - | forward => backward - | backward => forward - end. - - Lemma read_char_reverse: - forall cd inp dir c nextinp, - read_char rer cd inp dir = Some (c, nextinp) -> - read_char rer cd nextinp (reverse dir) = Some (c, inp). - Proof. - intros cd [next1 pref1] dir c [next2 pref2] H. - destruct dir; simpl; simpl in H. - - destruct next1; inversion H. - destruct (char_match) eqn:CM; inversion H. subst. - rewrite CM. auto. - - destruct pref1; inversion H. - destruct (char_match) eqn:CM; inversion H. subst. - rewrite CM. auto. - Qed. - - Theorem noprio_reversal: - forall dir r inp1 inp2 - (NP1: noprio dir inp1 r inp2), - noprio (reverse dir) inp2 r inp1. - Proof. - intros dir r inp1 inp2 NP1. - induction NP1; intros. - - repeat (econstructor; eauto). - - apply read_char_reverse in READ as REV. - destruct dir; simpl; econstructor; eauto. - - repeat (econstructor; eauto). - - solve[repeat (econstructor; eauto)]. - - repeat (econstructor; eauto). - - repeat (econstructor; eauto). - - apply quant_iters in IHNP1_2 as [n [GE [LE IT]]]. - apply iters_quant with (n:= S n); auto. lia. - { inversion LE; subst; constructor. lia. } - eapply add_iter_end; eauto. - - repeat (econstructor; eauto). - - apply quant_iters in IHNP1_2 as [n [GE [LE IT]]]. - apply iters_quant with (n:=S n); auto. - { inversion LE; subst; constructor. lia. } - eapply add_iter_end; eauto. - - eapply np_quant_skip. - - repeat (econstructor; eauto). - - repeat (econstructor; eauto). - Qed. - - (** * Leaf Reversal Theorem *) - - (* We come back to is_tree semantics to prove the reversal property *) - - Lemma leaf_reversal: - forall r dir inp1 inp2 gm2 t1 t2 - (SUBSET: pike_regex r) - (TREE1: is_tree rer [Areg r] inp1 GroupMap.empty dir t1) - (TREE2: is_tree rer [Areg r] inp2 GroupMap.empty (reverse dir) t2) - (IN: In (inp2, gm2) (tree_leaves t1 GroupMap.empty inp1 dir)), - exists gm1, In (inp1, gm1) (tree_leaves t2 GroupMap.empty inp2 (reverse dir)). - Proof. - intros r dir inp1 inp2 gm2 t1 t2 SUBSET TREE1 TREE2 IN. - assert (NP1: noprio dir inp1 r inp2). - { apply <- noprio_eq_is_leaf; eauto. } - apply noprio_reversal in NP1 as NP2. - assert (IN2: exists leafgm, In (inp1, leafgm) (tree_leaves t2 GroupMap.empty inp2 (reverse dir))). - { eapply noprio_eq_is_leaf; eauto. } - eauto. - Qed. - -End NoPrioSemantics. From c07eea70d76446c4859c56aa5bce3e93b1b14a26 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Fri, 12 Jun 2026 13:21:10 +0200 Subject: [PATCH 10/11] Engine: document the Reversal proof --- Engine/NoPrioSemantics.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/Engine/NoPrioSemantics.v b/Engine/NoPrioSemantics.v index d19315c..1f3e8c8 100644 --- a/Engine/NoPrioSemantics.v +++ b/Engine/NoPrioSemantics.v @@ -341,7 +341,17 @@ Section NoPrioSemantics. Qed. (* In order to prove the reversal property, we characterize quantifiers in the nopriority semantics *) - + (* While reversing a quantifier, something interesting happens: + - when iterating the quantifier, both directions will first do the iteration, then match the reduced quantifier + - this means that the peeled iteration is used for different parts of the string (contrary to the case of the sequence where each subexpression matches exactly the same part of the string) + - to make things worse, the peeled iteration and the following ones might have different constraints: some might check for progress, and some might not. + - yet, the reversal theorem still holds. But, reversing a quantifier might result in a different number of iterations of that quantifier. + - the theorem still holds because all of the checked-for-progress iterations are optional. So if doing iterations in an order results in a position where an iteration cannot be made (but it could be made in the reverse direction), then it was an optional empty iteration that can be skipped entirely. + - to deal with this mix of out-of-orders and checked-for-progress-or-not iterations, we present an alternative characterization of quantifiers: being able to match r{min,delta} is equivalent to saying that there is a chain of n iterations where n in [min,min+delta]. + - all of these iterations are allowed to be empty: even if that could be illegal, it can then be skipped when reconstructing the quantifier semantics + - this characterization makes it easier to prove reversal: we go from quantifier semantics to a numbered sequence, we add an extra iteration on either side (giving us a longer numbered sequence), and then we come back to quantifier semantics. *) + + (* Numbered sequence characterization *) (* n iterations of a regex *) Inductive iters : nat -> Direction -> input -> regex -> input -> Prop := | iters_refl: From 617fe1c268b736bf3943701832f29a543769591c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Tue, 23 Jun 2026 16:44:48 +0200 Subject: [PATCH 11/11] Engine: fix trailing whitespace --- Engine/NoPrioSemantics.v | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/Engine/NoPrioSemantics.v b/Engine/NoPrioSemantics.v index 1f3e8c8..139ebd8 100644 --- a/Engine/NoPrioSemantics.v +++ b/Engine/NoPrioSemantics.v @@ -72,10 +72,10 @@ Section NoPrioSemantics. forall dir inp a (ANCHOR: anchor_satisfied rer a inp = true), noprio dir inp (Anchor a) inp. - + (* LATER: there will be an issue if we want to add negative lookarounds: strict positivity *) (* We might want to declare an oracle version of this, since this reversal is used in engines when we already know about the values of deeper lookarounds. *) - + (** * NoPrio Tree Equivalence *) Lemma two_app: @@ -129,10 +129,10 @@ Section NoPrioSemantics. Theorem noprio_is_leaf: forall dir r inp gm t leafinp (TREE: is_tree rer [Areg r] inp gm dir t), - noprio dir inp r leafinp -> + noprio dir inp r leafinp -> exists leafgm, In (leafinp, leafgm) (tree_leaves t gm inp dir). Proof. - intros dir r inp gm t leafinp TREE NP. + intros dir r inp gm t leafinp TREE NP. generalize dependent t. generalize dependent gm. induction NP; intros. - inversion TREE; subst. inversion ISTREE; subst. @@ -186,20 +186,20 @@ Section NoPrioSemantics. - inversion TREECONT; subst. simpl. auto. - apply CHECKFAIL in PROGRESS. inversion PROGRESS. (* we know progress happened *) } - specialize (is_tree_productivity rer [Areg (Quantified greedy 0 delta r)] inp1 gm1 dir) as [t3 HT3]. + specialize (is_tree_productivity rer [Areg (Quantified greedy 0 delta r)] inp1 gm1 dir) as [t3 HT3]. assert (IN3: exists gm2, In (inp2, gm2) (tree_leaves t3 gm1 inp1 dir)). { apply IHNP2. auto. } destruct IN3 as [gm2 IN3]. rewrite three_app in ISTREE1. destruct greedy; simpl. + eexists. apply in_or_app. left. - eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). + eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). + eexists. apply in_or_app. right. - eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). + eapply (in_leaves_app3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ISTREE1 HT1 HT2 HT3 IN1 IN2 IN3). - inversion TREE; subst. { destruct delta; inversion H1. } inversion SKIP. subst. destruct greedy; simpl; eauto. - eexists. apply in_or_app; simpl; eauto. + eexists. apply in_or_app; simpl; eauto. - inversion TREE; subst. rewrite two_app in TREECONT. specialize (is_tree_productivity rer [Areg r] inp (GroupMap.open (idx inp) gid gm) dir) as [t1 HT1]. @@ -251,12 +251,12 @@ Section NoPrioSemantics. try solve [inversion LEAF]; pike_subset. - destruct LEAF as [LEAF|LEAF]; inversion LEAF; subst. constructor. - repeat (econstructor; eauto). - - repeat (econstructor; eauto). + - repeat (econstructor; eauto). - repeat (econstructor; eauto). - econstructor; eauto. 2: { apply read_char_success_advance in READ as ADV. unfold advance_input' in LEAF. rewrite ADV in LEAF. eauto. } - repeat (econstructor; eauto). + repeat (econstructor; eauto). - apply in_app_or in LEAF as [LEAF|LEAF]. + assert (noprio_list dir inp (Areg r1::cont) inp1). { apply IHTREE1; auto. pike_subset. } @@ -317,7 +317,7 @@ Section NoPrioSemantics. forall dir r inp gm t leafinp (SUBSET: pike_regex r) (TREE: is_tree rer [Areg r] inp gm dir t), - noprio dir inp r leafinp <-> + noprio dir inp r leafinp <-> exists leafgm, In (leafinp, leafgm) (tree_leaves t gm inp dir). Proof. intros dir r inp gm t leafinp SUBSET TREE. split. @@ -350,7 +350,7 @@ Section NoPrioSemantics. - to deal with this mix of out-of-orders and checked-for-progress-or-not iterations, we present an alternative characterization of quantifiers: being able to match r{min,delta} is equivalent to saying that there is a chain of n iterations where n in [min,min+delta]. - all of these iterations are allowed to be empty: even if that could be illegal, it can then be skipped when reconstructing the quantifier semantics - this characterization makes it easier to prove reversal: we go from quantifier semantics to a numbered sequence, we add an extra iteration on either side (giving us a longer numbered sequence), and then we come back to quantifier semantics. *) - + (* Numbered sequence characterization *) (* n iterations of a regex *) Inductive iters : nat -> Direction -> input -> regex -> input -> Prop := @@ -379,7 +379,7 @@ Section NoPrioSemantics. intros r dir greedy inp0 inp1 min delta QUANT. remember (Quantified greedy min delta r) as quant. generalize dependent min. generalize dependent delta. - induction QUANT; intros; + induction QUANT; intros; inversion Heqquant; subst. - clear IHQUANT1. specialize (IHQUANT2 delta0 min (eq_refl _)) as [n [GE [LE IT]]]. @@ -442,8 +442,8 @@ Section NoPrioSemantics. intros. induction ITERS; repeat (econstructor; eauto). Qed. - - + + (** * Reversal Property *) Definition reverse (d:Direction): Direction := @@ -466,7 +466,7 @@ Section NoPrioSemantics. destruct (char_match) eqn:CM; inversion H. subst. rewrite CM. auto. Qed. - + Theorem noprio_reversal: forall dir r inp1 inp2 (NP1: noprio dir inp1 r inp2), @@ -477,7 +477,7 @@ Section NoPrioSemantics. - repeat (econstructor; eauto). - apply read_char_reverse in READ as REV. destruct dir; simpl; econstructor; eauto. - - repeat (econstructor; eauto). + - repeat (econstructor; eauto). - solve[repeat (econstructor; eauto)]. - repeat (econstructor; eauto). - repeat (econstructor; eauto). @@ -498,7 +498,7 @@ Section NoPrioSemantics. (** * Leaf Reversal Theorem *) (* We come back to is_tree semantics to prove the reversal property *) - + Lemma leaf_reversal: forall r dir inp1 inp2 gm2 t1 t2 (SUBSET: pike_regex r) @@ -515,5 +515,5 @@ Section NoPrioSemantics. { eapply noprio_eq_is_leaf; eauto. } eauto. Qed. - + End NoPrioSemantics.