Defining a function by recursion over an inductive predicate in Coq

Question

I'm trying to re-implement some Agda code of mine in Coq. My problem is that one of my Agda functions is defined by recursion on the structure of an inductive predicate.

In my Coq code, I'm trying to follow the same style but there's a pattern matching restriction that does not allow to analyse the structure of a value with type in Prop to produce a result in Set. My question is: Is there a way to define functions by recursion on proofs while producing results in Set (like sumbool)?

The code that contains all definitions to reproduce the error is at the following gist.

Answer 1

The problem is that you need information wrapped up in the proof to construct your tree. Specifically, you need some split (s1, s2) such that s1 ++ s2 = s /\ s1 <<- e1 /\ s2 <<- e2. That split has to be defined computationally as opposed to extracting the appropriate split from the proof H: s1 <<- e1 @ e2.

The simplest way to fix this is to put in_regex in Type, to match how your Agda development works. This means that in_regex has to be constructed computationally, and as a result you can match on it freely.

Inductive in_regex : string -> regex -> Type

The use of not in empty_in_regex_inv breaks, but you can just write s <<- #0 -> False.

Credit to Ben Sherman for pointing this solution out!

It's also possible to keep in_regex in Prop, but then you need a separate computational way of matching regexes which will compute the split, and then a proof that relates this function to in_regex.