Parse Tree Preference

RegexParseTreesFull.v

Require Import Coq.Lists.List.

Declare Scope regex_scope.
Open Scope regex_scope.

Section Regex.

Variable (A : Type).

Inductive Regex : Type :=
| Epsilon : Regex
| CharClass : (A -> bool) -> Regex
| Concat : Regex -> Regex -> Regex
| Union : Regex -> Regex -> Regex
| Star : Regex -> Regex
.

Definition ε := Epsilon.
Infix "·" := Concat (at level 60, right associativity) : regex_scope.
Infix "∪" := Union (at level 50, left associativity) : regex_scope.
Notation "r *" := (Star r) (at level 40, no associativity) : regex_scope.

Inductive parse_tree : Regex -> list A -> nat -> nat -> Type :=
| parse_epsilon : forall (w : list A) (start : nat),
    parse_tree ε w start 0
| parse_charclass : forall (a : A) (pred : A -> bool) (w : list A) (start : nat),
    (pred a = true) 
    -> (nth_error w start = Some a) 
    -> parse_tree (CharClass pred) w start 1
| parse_concat : forall (r1 r2 : Regex) (w : list A) (start d1 d2 : nat),
    parse_tree r1 w start d1 
    -> parse_tree r2 w (start + d1) d2 
    -> parse_tree (r1 · r2) w start (d1 + d2)
| parse_union_l : forall (r1 r2 : Regex) (w : list A) (start d : nat),
    parse_tree r1 w start d 
    -> parse_tree (r1 ∪ r2) w start d
| parse_union_r : forall (r1 r2 : Regex) (w : list A) (start d : nat),
    parse_tree r2 w start d 
    -> parse_tree (r1 ∪ r2) w start d
| parse_star_nil : forall (r : Regex) (w : list A) (start : nat),
    parse_tree (r *) w start 0
| parse_star_cons : forall (r : Regex) (w : list A) (start d1 d2 : nat),
    d1 > 0 
    -> parse_tree r w start d1 
    -> parse_tree (r *) w (start + d1) d2
    -> parse_tree (r *) w start (d1 + d2)
.


Inductive prefer : forall (r : Regex) (w : list A) (i1 d1 i2 d2: nat),
    parse_tree r w i1 d1 -> parse_tree r w i2 d2 -> Prop := 
| prefer_union_l : 
    forall (r1 r2 : Regex) (w : list A) (i1 d1 i2 d2: nat) 
        (p1 : parse_tree r1 w i1 d1) (p2 : parse_tree r2 w i2 d2),
        prefer (r1 ∪ r2) w i1 d1 i2 d2 
            (parse_union_l r1 r2 w i1 d1 p1) 
            (parse_union_r r1 r2 w i2 d2 p2)
| prefer_concat_lex1 :
    forall (r s : Regex) (w : list A) (ir1 dr1 ir2 dr2 ds1 ds2 : nat)
        (pr1 : parse_tree r w ir1 dr1) (pr2 : parse_tree r w ir2 dr2) 
        (ps1 : parse_tree s w (ir1 + dr1) ds1) (ps2 : parse_tree s w (ir2 + dr2) ds2),
        prefer r w ir1 dr1 ir2 dr2 pr1 pr2
        -> prefer (r · s) w ir1 (dr1 + ds1) ir2 (dr2 + ds2) 
            (parse_concat r s w ir1 dr1 ds1 pr1 ps1)
            (parse_concat r s w ir2 dr2 ds2 pr2 ps2)
| prefer_concat_lex2 : 
    forall (r s : Regex) (w : list A) (i dr ds1 ds2 : nat)
        (pr : parse_tree r w i dr)
        (ps1 : parse_tree s w (i + dr) ds1) (ps2 : parse_tree s w (i + dr) ds2),
        prefer s w (i + dr) ds1 (i + dr)  ds2 ps1 ps2 
        -> prefer (r · s) w i (dr + ds1) i (dr + ds2) 
            (parse_concat r s w i dr ds1 pr ps1) 
            (parse_concat r s w i dr ds2 pr ps2)
| prefer_cons_nil :
    forall (r : Regex) (w : list A) (i1 i2 d1 d1' : nat)
        (d1_gt_0 : d1 > 0) 
        (p1 : parse_tree r w i1 d1) (p1' : parse_tree (r *) w (i1 + d1) d1'),
        prefer (r *) w i1 (d1 + d1') i2 0 
            (parse_star_cons r w i1 d1 d1' d1_gt_0 p1 p1')
            (parse_star_nil r w i2)
| prefer_cons_lex1 : 
    forall (r : Regex) (w : list A) (i1 d1 d1' i2 d2 d2' : nat)
        (d1_gt_0 : d1 > 0) (d2_gt_0 : d2 > 0) 
        (p1 : parse_tree r w i1 d1) (p1' : parse_tree (r *) w (i1 + d1) d1')
        (p2 : parse_tree r w i2 d2) (p2' : parse_tree (r *) w (i2 + d2) d2'),
        prefer r w i1 d1 i2 d2 p1 p2
        -> prefer (r *) w i1 (d1 + d1') i2 (d2 + d2') 
            (parse_star_cons r w i1 d1 d1' d1_gt_0 p1 p1') 
            (parse_star_cons r w i2 d2 d2' d2_gt_0 p2 p2')
| prefer_cons_lex2 :
    forall (r : Regex) (w : list A) (i d d1 d2 : nat)
        (d_gt_0 : d > 0) (p : parse_tree r w i d) 
        (p1 : parse_tree (r *) w (i + d) d1) (p2 : parse_tree (r *) w (i + d) d2),
        prefer (r *) w (i + d) d1 (i + d) d2 p1 p2
        -> prefer (r *) w i (d + d1) i (d + d2) 
            (parse_star_cons r w i d d1 d_gt_0 p p1) 
            (parse_star_cons r w i d d2 d_gt_0 p p2)
.

Lemma prefer_eps_antirefl :
    forall (w : list A) (i d : nat) (p : parse_tree _ _ _ _),
    ~ prefer ε w i d i d p p.
Proof.
    unfold not. intros.
    remember ε as r.
    destruct p; inversion Heqr.
    - inversion H.
Qed.

Lemma prefer_charclass_antirefl :
    forall (c : A -> bool) (w : list A) (i d : nat) (p : parse_tree _ _ _ _),
    ~ prefer (CharClass c) w i d i d p p.
Proof.
    unfold not. intros.
    remember (CharClass c) as r.
    destruct p; inversion Heqr.
    - inversion H.
Qed.

Lemma prefer_union_antirefl :
    forall (r1 r2 : Regex) (w : list A) (i d : nat) (p : parse_tree _ _ _ _),
    ~ prefer (r1 ∪ r2) w i d i d p p.
Proof.
    unfold not. intros.
    remember (r1 ∪ r2) as r.
    destruct p; inversion Heqr; inversion H.
Qed.

Lemma prefer_antirefl : 
    forall (r : Regex) (w : list A) (i d : nat) (p : parse_tree _ _ _ _),
    ~ prefer r w i d i d p p.
Proof.
    unfold not. induction r; intros.
    - apply prefer_eps_antirefl in H. assumption.
    - apply prefer_charclass_antirefl in H. assumption.
    - remember (r1 · r2) as r.
      destruct p; inversion Heqr.
      subst. 
      inversion H.
      + admit.
      + admit.
    - apply prefer_union_antirefl in H. assumption.
    - remember (r *) as s.
      destruct p; inversion Heqs.
      subst.
      + inversion H.
      + admit.
Admitted.
    
Inductive greedy_leq : forall (r : Regex) (w : list A) (i1 d1 i2 d2 : nat),
    parse_tree r w i1 d1 -> parse_tree r w i2 d2 -> Prop :=
| greedy_leq_refl : 
    forall (r : Regex) (w : list A) (i d : nat) 
        (p : parse_tree r w i d),
        greedy_leq r w i d i d p p
| greedy_leq_step :
    forall (r : Regex) (w : list A) (i1 d1 i2 d2 : nat) 
        (p1 : parse_tree r w i1 d1) (p2 : parse_tree r w i2 d2),
        prefer r w i1 d1 i2 d2 p1 p2
        -> greedy_leq r w i1 d1 i2 d2 p1 p2
| greedy_leq_trans :
    forall (r : Regex) (w : list A) (i1 d1 i2 d2 i3 d3 : nat) 
        (p1 : parse_tree r w i1 d1) (p2 : parse_tree r w i2 d2) (p3 : parse_tree r w i3 d3),
        greedy_leq r w i1 d1 i2 d2 p1 p2
        -> greedy_leq r w i2 d2 i3 d3 p2 p3
        -> greedy_leq r w i1 d1 i3 d3 p1 p3
.

RegexParseTreesSimple.v

Require Import Coq.Lists.List.


Import ListNotations.

Section Regex.

Variable (A : Type).

Inductive SimpleRegex : Type :=
| CharClass : (A -> bool) -> SimpleRegex
| Concat : SimpleRegex -> SimpleRegex -> SimpleRegex
.

Inductive parse_tree : SimpleRegex -> list A -> Type :=
| parse_charclass : forall f x,
    f x = true ->
    parse_tree (CharClass f) [x]
| parse_concat : forall r1 r2 s1 s2,
    parse_tree r1 s1 ->
    parse_tree r2 s2 ->
    parse_tree (Concat r1 r2) (s1 ++ s2)
.

Inductive prefer : forall (r : SimpleRegex) (w1 w2 : list A),
    parse_tree r w1 -> parse_tree r w2 -> Prop :=
| prefer_concat_lex1 :
    forall (r s : SimpleRegex) (wr1 wr2 ws1 ws2 : list A)
    (pwr1 : parse_tree r wr1) (pwr2 : parse_tree r wr2)
    (pws1 : parse_tree s ws1) (pws2 : parse_tree s ws2),
    prefer r wr1 wr2 pwr1 pwr2 
    -> prefer (Concat r s) (wr1 ++ ws1) (wr2 ++ ws2) 
        (parse_concat r s wr1 ws1 pwr1 pws1) (parse_concat r s wr2 ws2 pwr2 pws2)
| prefer_concat_lex2 :
    forall (r s : SimpleRegex) (wr ws1 ws2 : list A)
    (pwr : parse_tree r wr)
    (pws1 : parse_tree s ws1) (pws2 : parse_tree s ws2),
    prefer s ws1 ws2 pws1 pws2
    -> prefer (Concat r s) (wr ++ ws1) (wr ++ ws2)
        (parse_concat r s wr ws1 pwr pws1) (parse_concat r s wr ws2 pwr pws2)
.

Lemma prefer_charclass_antirefl :
    forall (c : A -> bool) (w : list A) (p : parse_tree (CharClass c) w),
    ~ prefer (CharClass c) w w p p.
Proof.
    unfold not. intros.
    remember (CharClass c) as r.
    destruct p; inversion Heqr.
    - inversion H.
Qed.

Lemma prefer_antirefl : forall r w (p : parse_tree r w),
    ~ prefer r w w p p.
Proof.
    unfold not. induction r; intros.
    - now apply prefer_charclass_antirefl in H.
    - remember (Concat r1 r2) as r.
      destruct p; inversion Heqr.
      (* This inversion above does away with all the cases 
         where p is not related to Concat
      *)
      inversion H. subst.
      + admit.
      + admit.
Admitted.

I would expect your definition to look like this:

I would expect your definition to look like this (avoid `nth_error`, and parse complete lists):

Inductive parse_tree' : Regex -> list A -> Type :=
| parse_epsilon' : parse_tree' ε nil
| parse_charclass' : forall a pred, pred a = true -> parse_tree' (CharClass pred) (a :: nil)
| parse_concat' : forall r1 r2 l1 l2, parse_tree' r1 l1 -> parse_tree' r2 l2 -> parse_tree' (Concat r1 r2) (l1 ++ l2)
| parse_union_l' : forall r1 r2 l, parse_tree' r1 l -> parse_tree' (Union r1 r2) l
| parse_union_r' : forall r1 r2 l, parse_tree' r2 l -> parse_tree' (Union r1 r2) l
| parse_star_nil' : forall r, parse_tree' (Star r) nil
| parse_star_cons' : forall r l1 l2, parse_tree' r l1 -> parse_tree' r l2 -> parse_tree' (Star r) (l1 ++ l2).

That is, avoid `nth_error` and use the structure of lists. If you would like partial parses, so that not the entire list is parsed, you can create an auxiliary definition for that purpose:

Inductive parse_partial : Regex -> list A -> Type :=
| parse_initial : forall r l1 l2, parse_tree' r l1 -> parse_partial r (l1 ++ l2).