Wf.v

(**
Skip to [Definition decode_aux] to see the main definition.
*)

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 Coq.Arith.Arith_base.

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 Dependent_Equality.

  Theorem eq_sigT_eq_dep : forall (U : Type) (P : U -> Type) (p q : U) 
  (x : P p) (y : P q), existT P p x = existT P q y -> EqdepFacts.eq_dep U P p x q y.
  Proof.
    intros * H.
    dependent rewrite H.
    apply EqdepFacts.eq_dep_intro.
  Defined.

End Dependent_Equality.

Section WfLexicographic_Product.

  Import SigTNotations.

  Variable A : Type.
  Variable B : A -> Type.
  Variable leA : A -> A -> Prop.
  Variable leB : forall x : A, B x -> B x -> Prop.

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

  Lemma acc_A_B_lexprod :
    forall x : A,
      Acc leA x ->
      (forall x0 : A, clos_trans A leA x0 x -> well_founded (leB x0)) ->
      forall y : B x, Acc (leB x) y -> Acc LexProd (x; y).
  Proof.
    induction 1 as [x _ IHAcc]; intros H2 y.
    induction 1 as [x0 H IHAcc0]; intros.
    apply Acc_intro.
    destruct y as [x2 y1]; intro H6.
    simple inversion H6; intro.
    - cut (leA x2 x); intros.
      + apply IHAcc; auto with sets.
        * intros.
          apply H2.
          apply t_trans with x2; auto with sets.

        * red in H2.
          apply H2.
          auto with sets.

      + injection H1 as [= <- _].
        injection H3 as [= <- _]; auto with sets.

    - rewrite <- H1.
      apply eq_sigT_eq_dep in H3.
      destruct H3.
      apply IHAcc0.
      assumption.
  Defined.

  Theorem wf_lexprod :
    well_founded leA ->
    (forall x : A, well_founded (leB x)) -> well_founded LexProd.
  Proof.
    intros wfA wfB; unfold well_founded.
    destruct a.
    apply acc_A_B_lexprod; auto with sets; intros.
    red in wfB.
    auto with sets.
  Defined.


End WfLexicographic_Product.

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.



(*****)

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 (fun (x y : nat) => S x <=? y = true) (rbc_to_rnat rbc1) (rbc_to_rnat rbc2).


Lemma comp_lte : forall a b c : nat, (a <=? b) = true -> (b <=? c) = true -> (a <=? c) = true. 
Proof. 
   induction a as [ | a Iha].
  + 
    intros * Ha Hb.
    reflexivity. 
  +
    intros [| b].
    ++
      intros * Ha Hb. 
      simpl in Ha; congruence. 
    ++
      intros [| c].
      intros Ha Hb. 
      +++
        simpl in Hb; congruence. 
      +++
        intros Ha Hb. 
        simpl in * |- *.
        exact (Iha _ _ Ha Hb).
Defined. 

Theorem acc_ltn : forall (a : nat), Acc (fun x y : nat => (S x <=? y) = true) a. 
Proof. 
 induction a. 
 +
    eapply Acc_intro; 
    intros * Ha. 
    cbn in Ha; 
    try congruence.
  +
    eapply Acc_intro.
    intros x Ha.
    eapply Acc_intro.
    intros y Hb.
    inversion IHa as (Iha).
    eapply Iha.
    simpl in Ha.
    exact (comp_lte _ _ _ Hb Ha).
Defined.

     
Theorem lt_wfc : well_founded (fun x y : nat => (S x <=? y) = true).
Proof. 
  unfold well_founded.
  intros a.
  eapply acc_ltn.
Defined.


Lemma acc_rbc : forall (rbc : Regex * list bool), 
  Acc rbc_lt rbc.
Proof.
  intros *.
  unfold rbc_lt.
  apply Acc_lemma with (y := rbc_to_rnat rbc).
  2: reflexivity.
  apply wf_slexprod.
  - apply regex_struct_wf.
  - apply lt_wfc.
Defined.

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

Definition computational_le (n m: nat) (H: n <= m) : n <= m :=
  match Compare_dec.le_lt_dec n m with
  | left x => x
  | _ => H
  end.

Definition computational_lt (n m: nat) (H: n < m) : n < m :=
  match Compare_dec.le_lt_dec m n with
  | right x => x
  | _ => H
  end.


Theorem le_transs : forall (a b c : nat), a <= b -> b <= c -> a <= c. 
Proof. 
  intros * Ha Hb.
  eapply Compare_dec.leb_correct in Ha, Hb. 
  eapply Compare_dec.leb_complete.
  eapply comp_lte; [exact Ha | exact Hb].
Defined. 


Theorem le_lt_n_Smm : forall (n m : nat), n <= m -> n < S m. 
Proof.
  intros n m Ha. 
  eapply Compare_dec.leb_correct in Ha.
  eapply Nat.ltb_lt. cbn.
  exact Ha.
Defined.     

Theorem lett_comp : forall (m : nat), m <=? m = true. 
Proof. 
  induction m as [|m Ihm];
  simpl; [exact eq_refl | exact Ihm].
Defined.

Theorem lett: forall (m : nat), m <= m. 
Proof.
  intros *.
  eapply Compare_dec.leb_complete.
  eapply lett_comp.
Defined.
 

Theorem comp_one : forall (a b : nat), a <=? b = true -> a <=? S b = true. 
Proof.
  induction a as [| a Iha].
  +
    cbn; intros; reflexivity.
  +
    intros [|b].
    ++
      simpl; intros; 
      try congruence.
    ++
      simpl; intros.
      eapply Iha.
      exact H.
Defined.

Definition decode_aux 
    (rbc : Regex * list bool) :
    { o : option (parse_tree * list bool) 
        | (match o with | Some (t, btc) => length btc <=? length (snd rbc) = true| 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 _ =>
        match decode_aux (e, btc) (f (e, btc) _) with
        | exist _ t1 Pt1 => match t1 as t1' return t1 = t1' -> _ with
            | None => fun Ha => exist _ None _
            | Some (t1, btc') => fun Ha => exist _ (Some (parse_union_l t1, btc')) _
            end eq_refl
        end 
    | (Union _ e, true :: btc) => fun _ =>
        match decode_aux (e, btc) (f (e, btc) _)  with
        | exist _ t2 Pt2 => match t2 as t2' return t2 = t2' -> _ with
            | None => fun Ha => exist _ None _
            | Some (t2, btc') => fun Ha => exist _ (Some (parse_union_r t2, btc')) _
            end eq_refl
        end 
    | (Concat e e1, btc) => fun _ => 
        match decode_aux (e, btc) (f (e, btc) _)  with
        | exist _ t1 Pt1 => match t1 as t1' return t1 = t1' -> _ with
            | None => fun Ha => exist _ None _
            | Some (t1, btc') => fun Ha =>  
                match decode_aux (e1, btc') (f (e1, btc') _)  with
                | exist _ t2 Pt2 => match t2 as t2' return t2 = t2' -> _ with
                    | None => fun Hb => exist _ None _
                    | Some (t2, btc'') => fun Hb => exist _ (Some (parse_concat t1 t2, btc'')) _
                    end eq_refl
                end
            end eq_refl
        end 
    | (Star _, []) => fun _ => exist _ None _
    | (Star _, true :: btc) => fun _ => exist _ None _
    | (Star e, false :: btc) => fun _ =>
        match decode_aux (e, btc) (f (e, btc) _) with
        | exist _ t1 Pt1 => match t1 as t1' return t1 = t1' -> _ with
            | None => fun Ha => exist _ None _
            | Some (t1, btc') => fun Ha =>  
                match decode_aux (Star e, btc') (f (Star e, btc') _)  with
                | exist _ t2 Pt2 => match t2 as t2' return t2 = t2' -> _ with
                    | None =>  fun Hb => exist _ None _
                    | Some (t2, btc'') => fun Hb => exist _ (Some (parse_star_cons t1 t2, btc'')) _
                    end eq_refl
                end
            end eq_refl
        end 
    end eq_refl);
      simpl in * |- *; subst; try (apply I);
      try (eapply lett_comp).
    +
      repeat constructor.
    +
      repeat constructor.
    +
      exact (comp_lte _ _ _ Pt2 Pt1).
    +
      repeat constructor.
    + 
      eapply comp_one; exact Pt2.
    + repeat constructor.
    + eapply comp_one; exact Pt1.
    + repeat constructor.
    +
      eapply right_slex; simpl.
      exact Pt1.
    +
      eapply comp_one.
      exact (comp_lte _ _ _ Pt2 Pt1).
Defined.


(* Print decode_aux. *)
Eval compute in proj1_sig (decode_aux (Epsilon, [false; true])).
(* Print decode_aux. *)
Eval compute in proj1_sig (decode_aux (CharClass (fun _ => true), [false; true])).
Eval compute in proj1_sig (decode_aux (Union (CharClass (fun _ => true)) _, [false; true])).
Eval compute in proj1_sig (decode_aux (Star (CharClass (fun _ => true)), [false; false; true])).


Print Opaque Dependencies decode_aux.
             
Definition decode_aux1 (r : Regex) (bc : list bool) : option (parse_tree * list bool) :=
  match decode_aux (r, bc) with
  | exist _ (Some (t, bc')) _ => Some (t, bc')
  | _ => None
  end.

Lemma decode_aux1_union_l (r1 r2 : Regex) (bc : list bool) :
    decode_aux1 (r1 ∪ r2) (false :: bc) =
    match decode_aux1 r1 bc with
    | Some (t, bc') => Some (parse_union_l t, bc')
    | None => None
    end.
Proof.
    unfold decode_aux1, decode_aux.
    reflexivity. (* Still not working *)
    
    
Abort.




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