CODEWITHSUNDEEP
coq
varkor
varkor

Reputation: 509

Defining a parameterised Fixpoint in Coq

I'm trying to define a fixpoint in Coq in which one of the function definitions refers to the other through a parameter, but I'm getting some confusing errors.

I've minimised the definition to this:

Require Import Coq.Init.Notations.
Require Import Coq.Init.Datatypes.

Inductive Wrapper (T : Type) :=
  | Wrap : T -> Wrapper T
  .
Inductive Unwrapper :=
  | Empty : Unwrapper
  | Unwrap : Wrapper Unwrapper -> Unwrapper
  .

Fixpoint Unwrapper_size (u : Unwrapper) {struct u} : nat :=
  match u with
  | Empty => O
  | Unwrap w => Wrapper_size w
  end

with Wrapper_size (w : Wrapper Unwrapper) {struct w} : nat :=
  match w with
  | Wrap _ t => Unwrapper_size t
  end.

which results in this error:

Recursive definition of Wrapper_size is ill-formed.
In environment
Unwrapper_size : Unwrapper -> nat
Wrapper_size : Wrapper Unwrapper -> nat
w : Wrapper Unwrapper
t : Unwrapper
Recursive call to Unwrapper_size has principal argument equal to
"t" instead of a subterm of "w".
Recursive definition is:
"fun w : Wrapper Unwrapper =>
match w with
| Wrap _ t => Unwrapper_size t
end".

Here, t is evidently a subterm of w — w was what we're matching on to get t, but Coq doesn't accept it. What's the mistake here, and how can I get around it?

Upvotes: 3

Views: 185

Answers (1)

Blaisorblade
Blaisorblade

Reputation: 6488

Let's assume you use Wrapper also on other arguments. Then you need to break the mutual recursion and make functions "parallel" to datatype. So you want to write Wrapper_size: Wrapper T -> (T -> nat) -> nat.

Then you can use Wrapper_size Unwrapper_size in Unwrapper_size: Coq should do enough inlining in termination checking to recognize this is safe.

In this example it's also easy to do that inlining by hand: Unwrapper_size would match on Unwrap (Wrap _ t) and recurse on t.

Upvotes: 3

Related Questions