Non-obvious Recursion

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


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.

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. simpl.
  (* no progress *)
Abort.

Fail Function 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.

(**

Error: Abstracting over the term "k" leads to a term
fun k0 : nat =>
S v < k0 ->
forall def : list A -> nat -> Regex * nat -> list parse_tree,
iter (list A -> nat -> Regex * nat -> list parse_tree) k0
  all_parse_trees_F def w start (r1 · r2, len) =
rec_res >>=
(fun t1 : parse_tree =>
 map (fun t2 : parse_tree => parse_concat t1 t2)
   (all_parse_trees0 w (start + parse_length t1)
      (r2, len - parse_length t1)))
which is ill-typed.

*)