Agnishom.v

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Import ListNotations.
Require Import Coq.Init.Nat.
Require Import Lia.
Require Import Relation_Definitions.

Declare Scope regex_scope.
Open Scope regex_scope.

Section Simple_Lexicographic_Product.

  Variable A : Type.
  Variable B : Type.
  Variable leA : A -> A -> Prop.
  Variable leB : B -> B -> Prop.

  Inductive slexprod : A * B -> A * B -> Prop :=
    | left_slex :
      forall (x x' : A) (y : B) (y' : B),
        leA x x' -> slexprod (x, y) (x', y')
    | right_slex :
      forall (x : A) (y y' : B),
        leB y y' -> slexprod (x, y) (x, y').

  Lemma slexprod_lexprod p1 p2 :
    slexprod p1 p2 <->
    lexprod _ _ leA (fun _ => leB) (sigT_of_prod p1) (sigT_of_prod p2).
  Proof.
    now split; intros HP; destruct p1, p2; inversion HP; constructor.
  Defined.

End Simple_Lexicographic_Product.

Section WfInclusion.
  Variable A : Type.
  Variables R1 R2 : A -> A -> Prop.

  Lemma Acc_incl : inclusion A R1 R2 -> forall z:A, Acc R2 z -> Acc R1 z.
  Proof.
    induction 2.
    apply Acc_intro; auto with sets.
  Defined.

  #[local]
  Hint Resolve Acc_incl : core.

  Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
  Proof.
    unfold well_founded; auto with sets.
  Defined.

End WfInclusion.

Section Inverse_Image.

  Variables A B : Type.
  Variable R : B -> B -> Prop.
  Variable f : A -> B.

  Let Rof (x y:A) : Prop := R (f x) (f y).

  Remark Acc_lemma : forall y:B, Acc R y -> forall x:A, y = f x -> Acc Rof x.
  Proof.
    induction 1 as [y _ IHAcc]; intros x H.
    apply Acc_intro; intros y0 H1.
    apply (IHAcc (f y0)); try trivial.
    rewrite H; trivial.
  Defined.

  Lemma Acc_inverse_image : forall x:A, Acc R (f x) -> Acc Rof x.
  Proof.
    intros; apply (Acc_lemma (f x)); trivial.
  Defined.

  Theorem wf_inverse_image : well_founded R -> well_founded Rof.
  Proof.
    red; intros; apply Acc_inverse_image; auto.
  Defined.

  Variable F : A -> B -> Prop.
  Let RoF (x y:A) : Prop :=
    exists2 b : B, F x b & (forall c:B, F y c -> R b c).

  Lemma Acc_inverse_rel : forall b:B, Acc R b -> forall x:A, F x b -> Acc RoF x.
  Proof.
    induction 1 as [x _ IHAcc]; intros x0 H2.
    constructor; intros y H3.
    destruct H3.
    apply (IHAcc x1); auto.
  Defined.


  Theorem wf_inverse_rel : well_founded R -> well_founded RoF.
  Proof.
    red; constructor; intros.
    case H0; intros.
    apply (Acc_inverse_rel x); auto.
  Defined.

End Inverse_Image.

Section WfSimple_Lexicographic_Product.

  Variable A : Type.
  Variable B : Type.
  Variable leA : A -> A -> Prop.
  Variable leB : B -> B -> Prop.

  Notation LexProd := (slexprod A B leA leB).

  Theorem wf_slexprod:
    well_founded leA -> well_founded leB -> well_founded LexProd.
  Proof.
    intros; eapply wf_incl.
    - intros x y; apply slexprod_lexprod.
    - now apply wf_inverse_image, wf_lexprod.
  Defined.

End WfSimple_Lexicographic_Product.

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
.

Inductive parse_tree : Type :=
| parse_epsilon : parse_tree
| parse_charclass : parse_tree
| parse_concat : parse_tree -> parse_tree -> parse_tree
| parse_union_l : parse_tree -> parse_tree
| parse_union_r : parse_tree -> parse_tree
| parse_star_nil : parse_tree
| parse_star_cons : parse_tree -> parse_tree -> parse_tree
.

Fixpoint parse_length (t : parse_tree) : nat :=
  match t with
  | parse_epsilon => 0
  | parse_charclass => 1
  | parse_concat t1 t2 => parse_length t1 + parse_length t2
  | parse_union_l t => parse_length t
  | parse_union_r t => parse_length t
  | parse_star_nil => 0
  | parse_star_cons t1 t2 => parse_length t1 + parse_length t2
end.


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 regex_struct : Regex -> Regex -> Prop :=
| regex_struct_concat_l : forall (r1 r2 : Regex),
    regex_struct r1 (r1 · r2)
| regex_struct_concat_r : forall (r1 r2 : Regex),
    regex_struct r2 (r1 · r2)
| regex_struct_union_l : forall (r1 r2 : Regex),
    regex_struct r1 (r1 ∪ r2)
| regex_struct_union_r : forall (r1 r2 : Regex),
    regex_struct r2 (r1 ∪ r2)
| regex_struct_star : forall (r : Regex),
    regex_struct r (r *)
.


Notation "x >>= f" := (flat_map f x) (at level 42, left associativity).


Lemma acc_regex : forall (rn : Regex * nat), 
  Acc (slexprod Regex nat regex_struct lt) rn.
Proof.
  intros *.
  eapply wf_slexprod.
  (* Note that wf_slexprod's definition is closed by Qed. 
    https://github.com/coq/coq/blob/master/theories/Wellfounded/Lexicographic_Product.v#L87
    So I have rewritten it.
  *)
  +
    (* Taken from Agnishom *)
    intro rs; induction rs; 
    constructor; intros * Ha.
    all:(inversion Ha; subst; auto).
  +
    eapply lt_wf.
    (* Note that lt_wf is closed by Defined so this one is fine.
    https://github.com/coq/coq/blob/master/theories/Arith/Wf_nat.v#L119 
    *)
Defined.


    

Definition all_parse_trees : 
  list A -> nat ->  Regex * nat -> list parse_tree.
Proof.
  intros w start rn.
  cut (Acc (slexprod _ _ regex_struct lt) rn).
  intros Hacc.
  revert start w. (* arugments are chaned a bit *)
  revert dependent rn.
  refine
    (fix all_parse_trees rn Hacc {struct Hacc} := 
    match Hacc with 
    | Acc_intro _ f => _ 
    end).
  refine 
    (match rn as rn' return rn = rn' -> _ with 
    | (Epsilon, _) => fun _ _ _  => [parse_epsilon]
    | (CharClass p, _) => fun Ha start w => 
      match nth_error w start with
      | Some a => if p a then [parse_charclass] else []
      | None => []
      end
    | (r1 · r2, len) => fun Ha start w => 
      all_parse_trees (r1, len) _ start w >>= fun t1 =>
        map (fun t2 => parse_concat t1 t2) 
        (all_parse_trees (r2, (len - parse_length t1)) _ 
        (start + parse_length t1) w)
    | (r1 ∪ r2, len) => fun Ha start w => 
      map (fun t => parse_union_l t) (all_parse_trees (r1, len) _ start w) ++
      map (fun t => parse_union_r t) (all_parse_trees (r2, len) _ start w)
    | ((r *), len) => fun Ha start w => 
      (match len as len' return len = len' -> _ with
      | 0 => fun _ => [parse_star_nil]
      | _ => fun Hb => 
      (all_parse_trees (r, len) _ start w >>= fun t1 =>
        (match parse_length t1 as t' return parse_length t1 = t' -> _ with 
        | 0 => fun _ => []
        | l1 => fun Hc => map (fun t2 => parse_star_cons t1 t2)  
          (all_parse_trees (r *, (len - l1)) _ (start + parse_length t1) w)
          ++ [parse_star_nil] end eq_refl))
      end eq_refl)
    end eq_refl); subst;
    eapply f; [left; constructor | left; constructor |
    left; constructor | left; constructor |
    right; nia | left; constructor].
    eapply acc_regex.
Defined.

(* 
End Regex.
Require Import Extraction.
Extraction all_parse_trees.
*)

Lemma all_parse_trees_concat : forall (w : list A) (start : nat) (r1 r2 : Regex) (len : nat),
  all_parse_trees w start (r1 · r2, len) =
  all_parse_trees w start (r1, len) >>= fun t1 => 
    map (fun t2 => parse_concat t1 t2) 
     (all_parse_trees w (start + parse_length t1) (r2, (len - parse_length t1))).
Proof.
  intros *;
  reflexivity.
Qed.