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

(*****)

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 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_wf.
Defined.

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.

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.

(* 
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 acc_rbc].
    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 _ (Some (parse_star_nil, btc)) _
    | (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 => _
        end eq_refl
    end eq_refl).
    4, 5, 6, 8, 10, 11: exact I.
    all : simpl.
    1, 2 : exact (computational_le _ _ (PeanoNat.Nat.le_refl _)).
    Unshelve.
    { clear y y0. (* clearing these creates extra shelved goals*) 
      (* Also an error is seen here if using Coq 8.18 *)
      rewrite e3 in Pt2. rewrite e2 in Pt1.
      exact (computational_le _ _ (PeanoNat.Nat.le_trans _ _ _ Pt2 Pt1)).
    }
    Unshelve.
    1 : subst t3; exact (computational_le _ _ (PeanoNat.Nat.le_le_succ_r _ _ Pt2)).
    1 : subst t2; exact (computational_le _ _ (PeanoNat.Nat.le_le_succ_r _ _ Pt1)).
    1 : exact (computational_le _ _ (PeanoNat.Nat.le_succ_diag_r _)).
    {
    refine (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 => _
        end eq_refl
    end eq_refl).
    Unshelve.
    2: trivial.
    2 : { rewrite e0. right. simpl. clear y. rewrite e1 in Pt1.
    exact (computational_lt _ _ (Arith_prebase.le_lt_n_Sm _ _ Pt1)).
    }
    refine (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).
    2: trivial.
    { subst t3 t4. simpl in Pt2.
      apply le_S. 
      exact (computational_le _ _ (PeanoNat.Nat.le_trans _ _ _ Pt2 Pt1)).
    } }
    1, 2, 3, 4, 5: subst rbc; left; constructor.
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) | 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; auto.
    +
      repeat constructor.
    +
      repeat constructor.
    +
      exact (computational_le _ _ (PeanoNat.Nat.le_trans _ _ _ Pt2 Pt1)).
    +
      repeat constructor.
    +
      repeat constructor.
    +
      repeat constructor.
    +
      (* Nevermind, it's not working! *)
      eapply right_slex; simpl.
      exact (computational_lt _ _ (Arith_prebase.le_lt_n_Sm _ _ Pt1)).
    +
      apply le_S. 
      exact (computational_le _ _ (PeanoNat.Nat.le_trans _ _ _ 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 _ => 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_length : forall (r : Regex) (bc : list bool) (t : parse_tree) (bc' : list bool),
  decode_aux1 r bc = Some (t, bc') -> length bc' <= length bc.
Proof.
  intros.
  unfold decode_aux1 in H.
  destruct (decode_aux (r, bc)) as [x Px] eqn:Heq.
  destruct x as [[t' bc''] | ]; [ | discriminate].
  inversion H; subst.
  simpl in Px.
  auto.
Qed.

Lemma decode_aux1_eps (bc : list bool) :
    decode_aux1 Epsilon bc = Some (parse_epsilon, bc).
Proof.
    reflexivity.
Qed.

Lemma decode_aux1_charclass (p : A -> bool) (bc : list bool) :
    decode_aux1 (CharClass p) bc = Some (parse_charclass, bc).
Proof.
    reflexivity.
Qed.

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.
    remember (decode_aux (r1 ∪ r2, false :: bc)).
    simpl in Heqs.
    simpl in Heqs. (* nothing happens *)
Abort.

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