Recursion on Two Arguments

Recursion.v

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.

Import ListNotations.

Require Import Coq.Init.Nat.

Require Import Recdef.
Require Import FunInd.
Require Import Coq.Program.Wf.

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
.

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.

Fail Fixpoint all_parse_trees (w : list A) (start len : nat) (r : Regex) : list parse_tree :=
  match r with
  | Epsilon => [parse_epsilon]
  | CharClass p => match nth_error w start with
                    | Some a => if p a then [parse_charclass] else []
                    | None => []
                    end
  | Concat r1 r2 => flat_map (fun t1 => map (fun t2 => parse_concat t1 t2) (all_parse_trees w (start + parse_length t1) (len - parse_length t1) r2)) (all_parse_trees w start len r1)
  | Union r1 r2 => map (fun t => parse_union_l t) (all_parse_trees w start len r1) ++ map (fun t => parse_union_r t) (all_parse_trees w start len r2)
  | Star r => 
    parse_epsilon :: 
      (flat_map 
      (fun t1 => map (fun t2 => parse_star_cons t1 t2) (all_parse_trees w (start + parse_length t1) (len - parse_length t1) (Star r) ))
      (filter (fun t => ltb 0 (parse_length t)) (all_parse_trees w start len r)))
      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 *)
.

Definition regex_nat_lex (rn : Regex * nat) (rm : Regex * nat) : Prop :=
  match rn, rm with
  | (r1, n1), (r2, n2) => 
    regex_struct r1 r2 \/ (r1 = r2 /\ n1 < n2)
  end.

Program Fixpoint all_parse_trees (w : list A) (start : nat) (rn : Regex * nat) {wf regex_nat_lex rn} : list parse_tree :=
  match rn with
  | (Epsilon, _) => [parse_epsilon]
  | (CharClass p, _) => match nth_error w start with
                      | Some a => if p a then [parse_charclass] else []
                      | None => []
                      end
  | (r1 · r2, len) => flat_map (fun t1 => map (fun t2 => parse_concat t1 t2) (all_parse_trees w (start + parse_length t1) (r2, (len - parse_length t1)))) (all_parse_trees w start (r1, len))
  | (r1 ∪ r2, len) => map (fun t => parse_union_l t) (all_parse_trees w start (r1, len)) ++ map (fun t => parse_union_r t) (all_parse_trees w start (r2, len))
  | ((r *), len) => 
    parse_epsilon :: 
      (flat_map 
      (fun t1 => map (fun t2 => parse_star_cons t1 t2) (all_parse_trees w (start + parse_length t1) ((r *), (len - parse_length t1))))
      (filter (fun t => ltb 0 (parse_length t)) (all_parse_trees w start (r, len))))
      end.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
Admitted.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
Admitted.

Solution1.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 Recdef.
Require Import FunInd.
Require Import Coq.Program.Wf.

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
.

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.

Fail Fixpoint all_parse_trees (w : list A) (start len : nat) (r : Regex) : list parse_tree :=
  match r with
  | Epsilon => [parse_epsilon]
  | CharClass p => match nth_error w start with
                    | Some a => if p a then [parse_charclass] else []
                    | None => []
                    end
  | Concat r1 r2 => flat_map (fun t1 => map (fun t2 => parse_concat t1 t2) (all_parse_trees w (start + parse_length t1) (len - parse_length t1) r2)) (all_parse_trees w start len r1)
  | Union r1 r2 => map (fun t => parse_union_l t) (all_parse_trees w start len r1) ++ map (fun t => parse_union_r t) (all_parse_trees w start len r2)
  | Star r => 
    parse_epsilon :: 
      (flat_map 
      (fun t1 => map (fun t2 => parse_star_cons t1 t2) (all_parse_trees w (start + parse_length t1) (len - parse_length t1) (Star r) ))
      (filter (fun t => ltb 0 (parse_length t)) (all_parse_trees w start len r)))
      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 *)
.

Definition regex_nat_lex (rn : Regex * nat) (rm : Regex * nat) : Prop :=
  match rn, rm with
  | (r1, n1), (r2, n2) => 
    regex_struct r1 r2 \/ (r1 = r2 /\ n1 < n2)
  end.
  
Notation "x >>= f" := (flat_map f x) (at level 42, left associativity).

Program Fixpoint all_parse_trees (w : list A) (start : nat) (rn : Regex * nat) 
  {wf (slexprod _ _ regex_struct lt) rn} : list parse_tree :=
  match rn with
  | (Epsilon, _) => [parse_epsilon]
  | (CharClass p, _) => match nth_error w start with
                      | Some a => if p a then [parse_charclass] else []
                      | None => []
                      end
  | (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)))
  | (r1 ∪ r2, len) => 
       map (fun t => parse_union_l t) (all_parse_trees w start (r1, len))
    ++ map (fun t => parse_union_r t) (all_parse_trees w start (r2, len))
  | ((r *), len) => match len with
      | 0 => [parse_star_nil]
      | _ =>
      (all_parse_trees w start (r, len) >>= fun t1 => match parse_length t1 with
        | 0 => []
        | l1 => map (fun t2 => parse_star_cons t1 t2) 
            (all_parse_trees w (start + parse_length t1) (r *, (len - l1)))
      ++ [parse_star_nil] end) end
  end.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
 right. 
 assert (0 < parse_length t1) as HH. {
    destruct (parse_length t1). 
    congruence. lia.
 }
 assert (0 < n1) as HH'. {
    destruct n1. congruence. lia.
 }
 lia.
Defined.
Next Obligation.
  left. constructor.
Defined.
Next Obligation.
  apply measure_wf.
  apply wf_slexprod.
  - intros r. induction r; constructor; intros.
    1, 2 : inversion H.
    + inversion H; subst; auto.
    + inversion H; subst; auto.
    + inversion H; subst; auto.
  - apply lt_wf.
Defined.