Skip to content

Instantly share code, notes, and snippets.

@Agnishom
Created September 2, 2023 01:23
Show Gist options
  • Save Agnishom/1150d29732a6c727396fb6c118dbf375 to your computer and use it in GitHub Desktop.
Save Agnishom/1150d29732a6c727396fb6c118dbf375 to your computer and use it in GitHub Desktop.
Non-obvious Recursion
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.
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment