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?
coq
asked Nov 22 '18 at 11:06
varkorvarkor
1279
|
show 1 more comment
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?
coq
asked Nov 22 '18 at 11:06
varkorvarkor
1279
Your code is very suspicious: The only base case returns 0 and there is no operation on nat. So that if it terminates it only return 0. That's probably not what you want.
– hivert
Nov 22 '18 at 14:34
Yes, I've minimised the definition to make it clearer to read. My actual use-case is less vacuous, but it just adds more noise to the problem. (You could imagine actually incrementing the results of the recursive calls to make a more useful function.)
– varkor
Nov 22 '18 at 14:37
1
As somebody said on IRC, for the current example, "try defining wrapper and unwrapper as mutually inductive", givingInductive Wrapper := Wrap: Unwrapper -> Wrapper with Unwrapper: Coq's concept of "subterm" assumes your recursion follows the structure of your datatypes. I suppose that won't help for the original one, but it'd be good to have an example where this doesn't work. I do have another idea tho...
– Blaisorblade
Nov 22 '18 at 20:28
1
If you also wrap other things, then you need to break the mutual recursion and make functions "parallel" to datatype. So writeWrapper_size: Wrapper T -> (T -> nat) -> nat.Then I'd try usingWrapper_size Unwrapper_sizeinUnwrapper_size: Coq might 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 onUnwrap (wrap t)and recurse ont).
– Blaisorblade
Nov 22 '18 at 20:32
If all else fails there's always well-founded induction, but it's annoying enough that I'd try avoiding it.
– Blaisorblade
Nov 22 '18 at 20:33
|
show 1 more comment
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?
coq
asked Nov 22 '18 at 11:06
varkorvarkor
1279
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?
coq
coq
asked Nov 22 '18 at 11:06
varkorvarkor
1279
asked Nov 22 '18 at 11:06
varkorvarkor
1279
asked Nov 22 '18 at 11:06
varkorvarkor
1279
asked Nov 22 '18 at 11:06
varkorvarkor
1279
asked Nov 22 '18 at 11:06
varkorvarkor
1279
1279
Your code is very suspicious: The only base case returns 0 and there is no operation on nat. So that if it terminates it only return 0. That's probably not what you want.
– hivert
Nov 22 '18 at 14:34
Yes, I've minimised the definition to make it clearer to read. My actual use-case is less vacuous, but it just adds more noise to the problem. (You could imagine actually incrementing the results of the recursive calls to make a more useful function.)
– varkor
Nov 22 '18 at 14:37
1
As somebody said on IRC, for the current example, "try defining wrapper and unwrapper as mutually inductive", givingInductive Wrapper := Wrap: Unwrapper -> Wrapper with Unwrapper: Coq's concept of "subterm" assumes your recursion follows the structure of your datatypes. I suppose that won't help for the original one, but it'd be good to have an example where this doesn't work. I do have another idea tho...
– Blaisorblade
Nov 22 '18 at 20:28
1
If you also wrap other things, then you need to break the mutual recursion and make functions "parallel" to datatype. So writeWrapper_size: Wrapper T -> (T -> nat) -> nat.Then I'd try usingWrapper_size Unwrapper_sizeinUnwrapper_size: Coq might 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 onUnwrap (wrap t)and recurse ont).
– Blaisorblade
Nov 22 '18 at 20:32
If all else fails there's always well-founded induction, but it's annoying enough that I'd try avoiding it.
– Blaisorblade
Nov 22 '18 at 20:33
|
show 1 more comment
Your code is very suspicious: The only base case returns 0 and there is no operation on nat. So that if it terminates it only return 0. That's probably not what you want.
– hivert
Nov 22 '18 at 14:34
Yes, I've minimised the definition to make it clearer to read. My actual use-case is less vacuous, but it just adds more noise to the problem. (You could imagine actually incrementing the results of the recursive calls to make a more useful function.)
– varkor
Nov 22 '18 at 14:37
1
As somebody said on IRC, for the current example, "try defining wrapper and unwrapper as mutually inductive", givingInductive Wrapper := Wrap: Unwrapper -> Wrapper with Unwrapper: Coq's concept of "subterm" assumes your recursion follows the structure of your datatypes. I suppose that won't help for the original one, but it'd be good to have an example where this doesn't work. I do have another idea tho...
– Blaisorblade
Nov 22 '18 at 20:28
1
If you also wrap other things, then you need to break the mutual recursion and make functions "parallel" to datatype. So writeWrapper_size: Wrapper T -> (T -> nat) -> nat.Then I'd try usingWrapper_size Unwrapper_sizeinUnwrapper_size: Coq might 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 onUnwrap (wrap t)and recurse ont).
– Blaisorblade
Nov 22 '18 at 20:32
If all else fails there's always well-founded induction, but it's annoying enough that I'd try avoiding it.
– Blaisorblade
Nov 22 '18 at 20:33
Your code is very suspicious: The only base case returns 0 and there is no operation on nat. So that if it terminates it only return 0. That's probably not what you want.
– hivert
Nov 22 '18 at 14:34
Your code is very suspicious: The only base case returns 0 and there is no operation on nat. So that if it terminates it only return 0. That's probably not what you want.
– hivert
Nov 22 '18 at 14:34
Yes, I've minimised the definition to make it clearer to read. My actual use-case is less vacuous, but it just adds more noise to the problem. (You could imagine actually incrementing the results of the recursive calls to make a more useful function.)
– varkor
Nov 22 '18 at 14:37
Yes, I've minimised the definition to make it clearer to read. My actual use-case is less vacuous, but it just adds more noise to the problem. (You could imagine actually incrementing the results of the recursive calls to make a more useful function.)
– varkor
Nov 22 '18 at 14:37
1
1
As somebody said on IRC, for the current example, "try defining wrapper and unwrapper as mutually inductive", giving
Inductive Wrapper := Wrap: Unwrapper -> Wrapper with Unwrapper: Coq's concept of "subterm" assumes your recursion follows the structure of your datatypes. I suppose that won't help for the original one, but it'd be good to have an example where this doesn't work. I do have another idea tho...– Blaisorblade
Nov 22 '18 at 20:28
As somebody said on IRC, for the current example, "try defining wrapper and unwrapper as mutually inductive", giving
Inductive Wrapper := Wrap: Unwrapper -> Wrapper with Unwrapper: Coq's concept of "subterm" assumes your recursion follows the structure of your datatypes. I suppose that won't help for the original one, but it'd be good to have an example where this doesn't work. I do have another idea tho...– Blaisorblade
Nov 22 '18 at 20:28
1
1
If you also wrap other things, then you need to break the mutual recursion and make functions "parallel" to datatype. So write
Wrapper_size: Wrapper T -> (T -> nat) -> nat. Then I'd try using Wrapper_size Unwrapper_size in Unwrapper_size: Coq might 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).– Blaisorblade
Nov 22 '18 at 20:32
If you also wrap other things, then you need to break the mutual recursion and make functions "parallel" to datatype. So write
Wrapper_size: Wrapper T -> (T -> nat) -> nat. Then I'd try using Wrapper_size Unwrapper_size in Unwrapper_size: Coq might 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).– Blaisorblade
Nov 22 '18 at 20:32
If all else fails there's always well-founded induction, but it's annoying enough that I'd try avoiding it.
– Blaisorblade
Nov 22 '18 at 20:33
If all else fails there's always well-founded induction, but it's annoying enough that I'd try avoiding it.
– Blaisorblade
Nov 22 '18 at 20:33
|
show 1 more comment
1 Answer
1
active
oldest
votes
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.
answered Nov 22 '18 at 21:09
BlaisorbladeBlaisorblade
5,4993457
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
StackExchange.using("externalEditor", function () {
StackExchange.using("snippets", function () {
StackExchange.snippets.init();
});
});
}, "code-snippets");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "1"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53429588%2fdefining-a-parameterised-fixpoint-in-coq%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
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.
answered Nov 22 '18 at 21:09
BlaisorbladeBlaisorblade
5,4993457
add a comment |
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.
answered Nov 22 '18 at 21:09
BlaisorbladeBlaisorblade
5,4993457
add a comment |
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.
answered Nov 22 '18 at 21:09
BlaisorbladeBlaisorblade
5,4993457
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.
answered Nov 22 '18 at 21:09
BlaisorbladeBlaisorblade
5,4993457
answered Nov 22 '18 at 21:09
BlaisorbladeBlaisorblade
5,4993457
answered Nov 22 '18 at 21:09
BlaisorbladeBlaisorblade
5,4993457
answered Nov 22 '18 at 21:09
BlaisorbladeBlaisorblade
5,4993457
5,4993457
add a comment |
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53429588%2fdefining-a-parameterised-fixpoint-in-coq%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Your code is very suspicious: The only base case returns 0 and there is no operation on nat. So that if it terminates it only return 0. That's probably not what you want.
– hivert
Nov 22 '18 at 14:34
Yes, I've minimised the definition to make it clearer to read. My actual use-case is less vacuous, but it just adds more noise to the problem. (You could imagine actually incrementing the results of the recursive calls to make a more useful function.)
– varkor
Nov 22 '18 at 14:37
1
As somebody said on IRC, for the current example, "try defining wrapper and unwrapper as mutually inductive", giving
Inductive Wrapper := Wrap: Unwrapper -> Wrapper with Unwrapper: Coq's concept of "subterm" assumes your recursion follows the structure of your datatypes. I suppose that won't help for the original one, but it'd be good to have an example where this doesn't work. I do have another idea tho...– Blaisorblade
Nov 22 '18 at 20:28
1
If you also wrap other things, then you need to break the mutual recursion and make functions "parallel" to datatype. So write
Wrapper_size: Wrapper T -> (T -> nat) -> nat.Then I'd try usingWrapper_size Unwrapper_sizeinUnwrapper_size: Coq might 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 onUnwrap (wrap t)and recurse ont).– Blaisorblade
Nov 22 '18 at 20:32
If all else fails there's always well-founded induction, but it's annoying enough that I'd try avoiding it.
– Blaisorblade
Nov 22 '18 at 20:33