Agnishom_proof.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 *)
.

Lemma regex_struct_wf : well_founded regex_struct.
Proof.
    intro rs; induction rs; 
    constructor; intros * Ha.
    all:(inversion Ha; subst; auto).
Defined.

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 *)
  generalize 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.

(*****)

Fixpoint bitcode (t : parse_tree) : list bool :=
  match t with
  | parse_epsilon => []
  | parse_charclass => []
  | parse_concat t1 t2 => bitcode t1 ++ bitcode t2
  | parse_union_l t => false :: bitcode t
  | parse_union_r t => true :: bitcode t
  | parse_star_nil => [true]
  | parse_star_cons t1 t2 => false :: bitcode t1 ++ bitcode t2
  end.

Definition rbc_to_rnat (rbc : Regex * list bool) : Regex * nat :=
   match rbc with
    | (r, bc) => (r, length bc)
    end.

Definition rbc_lt (rbc1 rbc2 : Regex * list bool) : Prop :=
  slexprod _ _ regex_struct lt (rbc_to_rnat rbc1) (rbc_to_rnat rbc2).

Lemma rbc_lt_wf : well_founded rbc_lt.
Proof.
    unfold rbc_lt.
    unfold well_founded.
    intros rbc.
    apply Acc_lemma with (y := rbc_to_rnat rbc).
    2: reflexivity.
    apply wf_slexprod.
    - apply regex_struct_wf.
    - apply lt_wf.
Defined.

(* Equations decode_aux (ebtc : Regex * list bool) : 
  decode_aux_type ebtc
  by wf ebtc (slexprod _ _ regex_struct (fun l m => length l < length m)) :=
decode_aux (Epsilon, btc) := exist _ (Some (parse_epsilon, btc)) _;
decode_aux (CharClass p, btc) := exist _ (Some (parse_charclass, btc)) _;
decode_aux (Union _ _, []) := exist _ None _;
decode_aux (Union e _, false :: btc) with decode_aux (e, btc) := {
    | exist _ None _ := exist _ None _;
    | exist _ (Some (t, btc')) _ := exist _ (Some (parse_union_l t, btc')) _
};
decode_aux (Union _ e, true :: btc) with decode_aux (e, btc) := {
    | exist _ None _ := exist _ None _;
    | exist _ (Some (t, btc')) _ := exist _ (Some (parse_union_r t, btc')) _
};
decode_aux (Concat e f, btc) with decode_aux (e, btc) := {
    | exist _ None _ := exist _ None _;
    | exist _ (Some (t1, btc')) _ with decode_aux (f, btc') := {
        | exist _ None _ := exist _ None _;
        | exist _ (Some (t2, btc'')) _ := exist _ (Some (parse_concat t1 t2, btc'')) _
    }
};
decode_aux (Star _, []) := exist _ None _;
decode_aux (Star _, true :: btc) := exist _ None _;
decode_aux (Star e, false :: btc) with decode_aux (e, btc) := {
    | exist _ None _ := exist _ None _;
    | exist _ (Some (t1, btc')) _ with decode_aux (Star e, btc') := {
        | exist _ None _ := exist _ None _;
        | exist _ (Some (t2, btc'')) _ := exist _ (Some (parse_star_cons t1 t2, btc'')) _
    };
}. *)

Definition decode_aux 
    (rbc : Regex * list bool) :
    { o : option (parse_tree * list bool) 
        | (match o with | Some (t, btc) => length btc <= length (snd rbc) | None => True end)
    }.
Proof.
    cut (Acc rbc_lt rbc); [ | apply rbc_lt_wf].
    intros Hacc.
    generalize dependent rbc.
    refine (fix decode_aux rbc Hacc {struct Hacc} :=
    match Hacc with
    | Acc_intro _ f => _
    end).
    refine (match rbc as rbc' return rbc = rbc' -> _ with
    | (Epsilon, btc) => fun _ => exist _ (Some (parse_epsilon, btc)) _
    | (CharClass p, btc) => fun _ => exist _ (Some (parse_charclass, btc)) _
    | (Union _ _, []) => fun _ => exist _ None _
    | (Union e _, false :: btc) => fun _ =>
        let ebtc_smaller : rbc_lt (e, btc) rbc := _ in
        match decode_aux (e, btc) (f (e, btc) ebtc_smaller) as d1 return _ = d1 -> _ with
        | exist _ t1 Pt1 => match t1 as t1' return t1 = t1' -> _ with
            | None => fun _ _ => exist _ None _
            | Some (t1, btc') => fun _ _ => exist _ (Some (parse_union_l t1, btc')) _
            end eq_refl
        end eq_refl
    | (Union _ e, true :: btc) => fun _ =>
        let ebtc_smaller : rbc_lt (e, btc) rbc := _ in
        match decode_aux (e, btc) (f (e, btc) ebtc_smaller) as d2 return _ = d2 -> _ with
        | exist _ t2 Pt2 => match t2 as t2' return t2 = t2' -> _ with
            | None => fun _ _ => exist _ None _
            | Some (t2, btc') => fun _ _ => exist _ (Some (parse_union_r t2, btc')) _
            end eq_refl
        end eq_refl
    | (Concat e e1, btc) => fun _ => 
        let ebtc_smaller : rbc_lt (e, btc) rbc := _ in
        match decode_aux (e, btc) (f (e, btc) ebtc_smaller) as d1 return _ = d1 -> _ with
        | exist _ t1 Pt1 => match t1 as t1' return t1 = t1' -> _ with
            | None => fun _ _ => exist _ None _
            | Some (t1, btc') => fun _ _ =>
                let e1btc_smaller : rbc_lt (e1, btc') rbc := _ in
                match decode_aux (e1, btc') (f (e1, btc') e1btc_smaller) as d2 return _ = d2 -> _ with
                | exist _ t2 Pt2 => match t2 as t2' return t2 = t2' -> _ with
                    | None => fun _ _ => exist _ None _
                    | Some (t2, btc'') => fun _ _ => exist _ (Some (parse_concat t1 t2, btc'')) _
                    end eq_refl
                end eq_refl
            end eq_refl
        end eq_refl
    | (Star _, []) => fun _ => exist _ None _
    | (Star _, true :: btc) => fun _ => exist _ None _
    | (Star e, false :: btc) => fun _ =>
        let ebtc_smaller : rbc_lt (e, btc) rbc := _ in
        match decode_aux (e, btc) (f (e, btc) ebtc_smaller) as d1 return _ = d1 -> _ with
        | exist _ t1 Pt1 => match t1 as t1' return t1 = t1' -> _ with
            | None => fun _ _ => exist _ None _
            | Some (t1, btc') => fun _ _ =>
                let ebtc1_smaller : rbc_lt (Star e, btc') rbc := _ in
                match decode_aux (Star e, btc') (f (Star e, btc') ebtc1_smaller) as d2 return _ = d2 -> _ with
                | exist _ t2 Pt2 => match t2 as t2' return t2 = t2' -> _ with
                    | None => fun _ _ => exist _ None _
                    | Some (t2, btc'') => fun _ _ => exist _ (Some (parse_star_cons t1 t2, btc'')) _
                    end eq_refl
                end eq_refl
            end eq_refl
        end eq_refl
    end eq_refl);
    simpl in * |- *; auto.
    Unshelve.
    +
      destruct t3 as [(xa, ya) | ];
      destruct t4 as [(xb, yb) | ];
      try congruence.
      inversion e2.
      inversion e3. 
      clear y0 y decode_aux ebtc_smaller e1btc_smaller.
      subst. nia.
      
    + 
      destruct t3 as [(xa, ya) | ];
      try congruence.
      inversion e1. 
      clear y decode_aux ebtc_smaller.
      subst. nia.
    +
      clear y decode_aux ebtc_smaller.
      subst. nia. 
    +
      clear y0 y decode_aux ebtc_smaller ebtc1_smaller.
      subst. nia. 
    + 
      clear decode_aux.
      subst; simpl in * |- *.
      unfold rbc_lt; simpl.
      eapply left_slex.
      constructor.
    +
      clear y decode_aux ebtc_smaller.
      subst; simpl in * |- *.
      unfold rbc_lt; simpl.
      eapply left_slex.
      constructor. 
    +
      clear decode_aux.
      subst; simpl. 
      unfold rbc_lt; simpl.
      eapply left_slex. constructor.
    +
      clear decode_aux.
      subst; simpl.
      unfold rbc_lt; simpl.
      eapply left_slex. constructor.
    +
      clear decode_aux.
      subst; simpl.
      unfold rbc_lt; simpl.
      repeat constructor.
    +
      clear y decode_aux ebtc_smaller.
      subst; simpl.
      unfold rbc_lt; simpl.
      eapply right_slex.
      simpl in * |- *.
      nia. 
  Defined.