Using polymorphic functions in definitions
Following my question here, I have several functions with different types of arguments which I defined the Inductive type formula on them. Is there anyway to use Inductive formula in compute_formula. I am doing this to make proving easier by decreasing the number of constructors that I have to handle in proofs. Thank you.
Fixpoint add (n:type1) (m:type2): type3 :=
match n with
(*body for add*)
end.
Fixpoint mul (n:type1) (m:type4): type5 :=
match n with
(*body for mul*)
end.
Inductive formula : Type :=
| Formula {A B}: type1-> A -> (type1->A->B) -> formula.
(* How should I write this *)
Definition compute_formula {A B} (f: formula) (extraArg:A) : B :=
match f with
|Formula {A B} part1 part2 part3=>
if (A isof type2 && B isof type3) then add part1 part2+extraArg
if (A isof type4 && B isof type5) then mul part1 part2+extraArg
end.
coq
asked Nov 22 '18 at 19:52
Tom And.Tom And.
756
add a comment |
Following my question here, I have several functions with different types of arguments which I defined the Inductive type formula on them. Is there anyway to use Inductive formula in compute_formula. I am doing this to make proving easier by decreasing the number of constructors that I have to handle in proofs. Thank you.
Fixpoint add (n:type1) (m:type2): type3 :=
match n with
(*body for add*)
end.
Fixpoint mul (n:type1) (m:type4): type5 :=
match n with
(*body for mul*)
end.
Inductive formula : Type :=
| Formula {A B}: type1-> A -> (type1->A->B) -> formula.
(* How should I write this *)
Definition compute_formula {A B} (f: formula) (extraArg:A) : B :=
match f with
|Formula {A B} part1 part2 part3=>
if (A isof type2 && B isof type3) then add part1 part2+extraArg
if (A isof type4 && B isof type5) then mul part1 part2+extraArg
end.
coq
asked Nov 22 '18 at 19:52
Tom And.Tom And.
756
add a comment |
Following my question here, I have several functions with different types of arguments which I defined the Inductive type formula on them. Is there anyway to use Inductive formula in compute_formula. I am doing this to make proving easier by decreasing the number of constructors that I have to handle in proofs. Thank you.
Fixpoint add (n:type1) (m:type2): type3 :=
match n with
(*body for add*)
end.
Fixpoint mul (n:type1) (m:type4): type5 :=
match n with
(*body for mul*)
end.
Inductive formula : Type :=
| Formula {A B}: type1-> A -> (type1->A->B) -> formula.
(* How should I write this *)
Definition compute_formula {A B} (f: formula) (extraArg:A) : B :=
match f with
|Formula {A B} part1 part2 part3=>
if (A isof type2 && B isof type3) then add part1 part2+extraArg
if (A isof type4 && B isof type5) then mul part1 part2+extraArg
end.
coq
asked Nov 22 '18 at 19:52
Tom And.Tom And.
756
Following my question here, I have several functions with different types of arguments which I defined the Inductive type formula on them. Is there anyway to use Inductive formula in compute_formula. I am doing this to make proving easier by decreasing the number of constructors that I have to handle in proofs. Thank you.
Fixpoint add (n:type1) (m:type2): type3 :=
match n with
(*body for add*)
end.
Fixpoint mul (n:type1) (m:type4): type5 :=
match n with
(*body for mul*)
end.
Inductive formula : Type :=
| Formula {A B}: type1-> A -> (type1->A->B) -> formula.
(* How should I write this *)
Definition compute_formula {A B} (f: formula) (extraArg:A) : B :=
match f with
|Formula {A B} part1 part2 part3=>
if (A isof type2 && B isof type3) then add part1 part2+extraArg
if (A isof type4 && B isof type5) then mul part1 part2+extraArg
end.
coq
coq
asked Nov 22 '18 at 19:52
Tom And.Tom And.
756
asked Nov 22 '18 at 19:52
Tom And.Tom And.
756
edited Nov 22 '18 at 20:12
Tom And.
asked Nov 22 '18 at 19:52
Tom And.Tom And.
756
asked Nov 22 '18 at 19:52
Tom And.Tom And.
756
asked Nov 22 '18 at 19:52
Tom And.Tom And.
756
756
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
What do you want the output type of compute_formula to be? The way the signature is written, the function would have to be able to compute an element of B no matter what B is. Since this is obviously impossible (what if B is Empty?), I'll show you a different approach.
The idea is to use the formula to get the output type.
Definition output_type (f: formula) :=
match f with
| @Formula _ B _ _ _ => B
end.
Then we can define compute_formula as
Definition compute_formula (f: formula): output_type f :=
match f with
| @Formula _ _ t a func => func t a
end.
A few other things. I'm not sure what you mean with the extraArg part. If you're more specific about what that means I might be able to help you. Also, there isn't (at least outside of tactics) a way to do what you want with A isof type2.
answered Nov 23 '18 at 23:42
UserUser
55048
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%2f53437324%2fusing-polymorphic-functions-in-definitions%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
What do you want the output type of compute_formula to be? The way the signature is written, the function would have to be able to compute an element of B no matter what B is. Since this is obviously impossible (what if B is Empty?), I'll show you a different approach.
The idea is to use the formula to get the output type.
Definition output_type (f: formula) :=
match f with
| @Formula _ B _ _ _ => B
end.
Then we can define compute_formula as
Definition compute_formula (f: formula): output_type f :=
match f with
| @Formula _ _ t a func => func t a
end.
A few other things. I'm not sure what you mean with the extraArg part. If you're more specific about what that means I might be able to help you. Also, there isn't (at least outside of tactics) a way to do what you want with A isof type2.
answered Nov 23 '18 at 23:42
UserUser
55048
add a comment |
What do you want the output type of compute_formula to be? The way the signature is written, the function would have to be able to compute an element of B no matter what B is. Since this is obviously impossible (what if B is Empty?), I'll show you a different approach.
The idea is to use the formula to get the output type.
Definition output_type (f: formula) :=
match f with
| @Formula _ B _ _ _ => B
end.
Then we can define compute_formula as
Definition compute_formula (f: formula): output_type f :=
match f with
| @Formula _ _ t a func => func t a
end.
A few other things. I'm not sure what you mean with the extraArg part. If you're more specific about what that means I might be able to help you. Also, there isn't (at least outside of tactics) a way to do what you want with A isof type2.
answered Nov 23 '18 at 23:42
UserUser
55048
add a comment |
What do you want the output type of compute_formula to be? The way the signature is written, the function would have to be able to compute an element of B no matter what B is. Since this is obviously impossible (what if B is Empty?), I'll show you a different approach.
The idea is to use the formula to get the output type.
Definition output_type (f: formula) :=
match f with
| @Formula _ B _ _ _ => B
end.
Then we can define compute_formula as
Definition compute_formula (f: formula): output_type f :=
match f with
| @Formula _ _ t a func => func t a
end.
A few other things. I'm not sure what you mean with the extraArg part. If you're more specific about what that means I might be able to help you. Also, there isn't (at least outside of tactics) a way to do what you want with A isof type2.
answered Nov 23 '18 at 23:42
UserUser
55048
What do you want the output type of compute_formula to be? The way the signature is written, the function would have to be able to compute an element of B no matter what B is. Since this is obviously impossible (what if B is Empty?), I'll show you a different approach.
The idea is to use the formula to get the output type.
Definition output_type (f: formula) :=
match f with
| @Formula _ B _ _ _ => B
end.
Then we can define compute_formula as
Definition compute_formula (f: formula): output_type f :=
match f with
| @Formula _ _ t a func => func t a
end.
A few other things. I'm not sure what you mean with the extraArg part. If you're more specific about what that means I might be able to help you. Also, there isn't (at least outside of tactics) a way to do what you want with A isof type2.
answered Nov 23 '18 at 23:42
UserUser
55048
answered Nov 23 '18 at 23:42
UserUser
55048
answered Nov 23 '18 at 23:42
UserUser
55048
answered Nov 23 '18 at 23:42
UserUser
55048
55048
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%2f53437324%2fusing-polymorphic-functions-in-definitions%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
