How to prove something by using a definition?Compute with a recursive function defined by well-defined inductionProving a theorem in Coq using almost only rewrites - no “cleverness”The induction principle generated by Coq does not behave like I want it toProof on permutations with Coq proof assistantHow does the discriminate tactic work?Interaction between type classes and auto tacticUsing 'unfold' of a Fixpoint inside the recursive step of the inductionMinimum in non-empty, finite setHow to prove decidability of a relation swaping its parameters?Prove properties of lists
In Dutch history two people are referred to as "William III"; are there any more cases where this happens?
Can I get the output of a command line program with TeX (using e.g. read18)?
How can sister protect herself from impulse purchases with a credit card?
Can I pay my credit card?
Why we learn compiler?
What color to choose as "danger" if the main color of my app is red
How to laser-level close to a surface
Are there any symmetric cryptosystems based on computational complexity assumptions?
Should all adjustments be random effects in a mixed linear effect?
Good examples of "two is easy, three is hard" in computational sciences
Why is so much ransomware breakable?
Failing students when it might cause them economic ruin
Is there a language that let's you use a try block without a catch block?
How to draw pentagram-like shape in Latex?
How to say "that" as in "the cow that ate" in Japanese?
At what point can a confirmation be established between words of similar meaning in context?
How was the blinking terminal cursor invented?
How do you cope with rejection?
How does this piece of code determine array size without using sizeof( )?
Is it possible to determine from only a photo of a cityscape whether it was taken close with wide angle or from a distance with zoom?
Have the writers and actors of GOT responded to its poor reception?
What were the "pills" that were added to solid waste in Apollo 7?
Why would you put your input amplifier in front of your filtering for an ECG signal?
how to create an executable file for an AppleScript?
How to prove something by using a definition?
Compute with a recursive function defined by well-defined inductionProving a theorem in Coq using almost only rewrites - no “cleverness”The induction principle generated by Coq does not behave like I want it toProof on permutations with Coq proof assistantHow does the discriminate tactic work?Interaction between type classes and auto tacticUsing 'unfold' of a Fixpoint inside the recursive step of the inductionMinimum in non-empty, finite setHow to prove decidability of a relation swaping its parameters?Prove properties of lists
.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty height:90px;width:728px;box-sizing:border-box;
If I define multiplication like this (drugi_c), how do I prove e.g. X*0=0?
(How to prove something by the definition?)
Fixpoint drugi_c(x y: nat): nat:=
match x, y with
| _, O => O
| O, _ => O
| S O, _ => y
| _,S O => x
| S x', S y' => plus y (drugi_c x' y)
end.
Notation "x * y" := (drugi_c x y) (at level 40, left associativity).
Whenever I use "simpl." in proofs instead of 0 = 0, i get the definition in result.
Lemma neka2 x:
x * 0 = 0.
Proof.
induction x.
-simpl. reflexivity.
-simpl. (*right here*)
Abort.
Result after the last simpl.
1 subgoal
x : nat
IHx : x * 0 = 0
______________________________________(1/1)
match x with
| 0 | _ => 0
end = 0
What to write after that last simpl. to finish the proof?
coq coqide
edited Mar 23 at 20:57
double-beep
3,12151632
asked Mar 23 at 17:36
Borna SirovecBorna Sirovec
41
add a comment |
If I define multiplication like this (drugi_c), how do I prove e.g. X*0=0?
(How to prove something by the definition?)
Fixpoint drugi_c(x y: nat): nat:=
match x, y with
| _, O => O
| O, _ => O
| S O, _ => y
| _,S O => x
| S x', S y' => plus y (drugi_c x' y)
end.
Notation "x * y" := (drugi_c x y) (at level 40, left associativity).
Whenever I use "simpl." in proofs instead of 0 = 0, i get the definition in result.
Lemma neka2 x:
x * 0 = 0.
Proof.
induction x.
-simpl. reflexivity.
-simpl. (*right here*)
Abort.
Result after the last simpl.
1 subgoal
x : nat
IHx : x * 0 = 0
______________________________________(1/1)
match x with
| 0 | _ => 0
end = 0
What to write after that last simpl. to finish the proof?
coq coqide
edited Mar 23 at 20:57
double-beep
3,12151632
asked Mar 23 at 17:36
Borna SirovecBorna Sirovec
41
add a comment |
If I define multiplication like this (drugi_c), how do I prove e.g. X*0=0?
(How to prove something by the definition?)
Fixpoint drugi_c(x y: nat): nat:=
match x, y with
| _, O => O
| O, _ => O
| S O, _ => y
| _,S O => x
| S x', S y' => plus y (drugi_c x' y)
end.
Notation "x * y" := (drugi_c x y) (at level 40, left associativity).
Whenever I use "simpl." in proofs instead of 0 = 0, i get the definition in result.
Lemma neka2 x:
x * 0 = 0.
Proof.
induction x.
-simpl. reflexivity.
-simpl. (*right here*)
Abort.
Result after the last simpl.
1 subgoal
x : nat
IHx : x * 0 = 0
______________________________________(1/1)
match x with
| 0 | _ => 0
end = 0
What to write after that last simpl. to finish the proof?
coq coqide
edited Mar 23 at 20:57
double-beep
3,12151632
asked Mar 23 at 17:36
Borna SirovecBorna Sirovec
41
If I define multiplication like this (drugi_c), how do I prove e.g. X*0=0?
(How to prove something by the definition?)
Fixpoint drugi_c(x y: nat): nat:=
match x, y with
| _, O => O
| O, _ => O
| S O, _ => y
| _,S O => x
| S x', S y' => plus y (drugi_c x' y)
end.
Notation "x * y" := (drugi_c x y) (at level 40, left associativity).
Whenever I use "simpl." in proofs instead of 0 = 0, i get the definition in result.
Lemma neka2 x:
x * 0 = 0.
Proof.
induction x.
-simpl. reflexivity.
-simpl. (*right here*)
Abort.
Result after the last simpl.
1 subgoal
x : nat
IHx : x * 0 = 0
______________________________________(1/1)
match x with
| 0 | _ => 0
end = 0
What to write after that last simpl. to finish the proof?
coq coqide
coq coqide
edited Mar 23 at 20:57
double-beep
3,12151632
asked Mar 23 at 17:36
Borna SirovecBorna Sirovec
41
edited Mar 23 at 20:57
double-beep
3,12151632
asked Mar 23 at 17:36
Borna SirovecBorna Sirovec
41
edited Mar 23 at 20:57
double-beep
3,12151632
edited Mar 23 at 20:57
double-beep
3,12151632
edited Mar 23 at 20:57
double-beep
3,12151632
3,12151632
asked Mar 23 at 17:36
Borna SirovecBorna Sirovec
41
asked Mar 23 at 17:36
Borna SirovecBorna Sirovec
41
asked Mar 23 at 17:36
Borna SirovecBorna Sirovec
41
41
add a comment |
add a comment |
3 Answers
3
active
oldest
votes
Your goal has a pattern match on x, but no matter what value x is it will return 0. To force this to simplify, you can destruct x.
Note that you never use the inductive hypothesis here, so you could have done destruct x at the beginning instead of induction x.
answered Mar 23 at 20:15
user138737user138737
31028
add a comment |
Here is what i end up getting:
Lemma neka2 x:
x * 0 = 0.
Proof.
destruct x.
-simpl. reflexivity.
-simpl. (**)
Abort.
Result:
1 subgoal
x : nat
______________________________________(1/1)
x * 0 = 0
I guess you have to prove it with induction because same thing happens when I try to destruct x with predefined mult as well.
Here is x*0=0 proof but with predefined mult:
Theorem mult_0_r : forall n:nat,
n * 0 = 0.
Proof.
intros n.
induction n as [|n'].
Case "n = 0".
simpl.
reflexivity.
Case "n = S n'".
simpl.
rewrite -> IHn'.
reflexivity.
Qed.
answered Mar 23 at 23:14
Borna SirovecBorna Sirovec
41
add a comment |
As @user138737 pointed out, you don't need induction. It is sufficient to explore three cases : x = 0, x = 1 and x = S (S x')). The shortest proof I can come with is thus the following.
destruct x as [| [|] ]; reflexivity.
answered Apr 4 at 10:20
eponiereponier
2,354418
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%2f55316535%2fhow-to-prove-something-by-using-a-definition%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
Your goal has a pattern match on x, but no matter what value x is it will return 0. To force this to simplify, you can destruct x.
Note that you never use the inductive hypothesis here, so you could have done destruct x at the beginning instead of induction x.
answered Mar 23 at 20:15
user138737user138737
31028
add a comment |
Your goal has a pattern match on x, but no matter what value x is it will return 0. To force this to simplify, you can destruct x.
Note that you never use the inductive hypothesis here, so you could have done destruct x at the beginning instead of induction x.
answered Mar 23 at 20:15
user138737user138737
31028
add a comment |
Your goal has a pattern match on x, but no matter what value x is it will return 0. To force this to simplify, you can destruct x.
Note that you never use the inductive hypothesis here, so you could have done destruct x at the beginning instead of induction x.
answered Mar 23 at 20:15
user138737user138737
31028
Your goal has a pattern match on x, but no matter what value x is it will return 0. To force this to simplify, you can destruct x.
Note that you never use the inductive hypothesis here, so you could have done destruct x at the beginning instead of induction x.
answered Mar 23 at 20:15
user138737user138737
31028
answered Mar 23 at 20:15
user138737user138737
31028
answered Mar 23 at 20:15
user138737user138737
31028
answered Mar 23 at 20:15
user138737user138737
31028
31028
add a comment |
add a comment |
Here is what i end up getting:
Lemma neka2 x:
x * 0 = 0.
Proof.
destruct x.
-simpl. reflexivity.
-simpl. (**)
Abort.
Result:
1 subgoal
x : nat
______________________________________(1/1)
x * 0 = 0
I guess you have to prove it with induction because same thing happens when I try to destruct x with predefined mult as well.
Here is x*0=0 proof but with predefined mult:
Theorem mult_0_r : forall n:nat,
n * 0 = 0.
Proof.
intros n.
induction n as [|n'].
Case "n = 0".
simpl.
reflexivity.
Case "n = S n'".
simpl.
rewrite -> IHn'.
reflexivity.
Qed.
answered Mar 23 at 23:14
Borna SirovecBorna Sirovec
41
add a comment |
Here is what i end up getting:
Lemma neka2 x:
x * 0 = 0.
Proof.
destruct x.
-simpl. reflexivity.
-simpl. (**)
Abort.
Result:
1 subgoal
x : nat
______________________________________(1/1)
x * 0 = 0
I guess you have to prove it with induction because same thing happens when I try to destruct x with predefined mult as well.
Here is x*0=0 proof but with predefined mult:
Theorem mult_0_r : forall n:nat,
n * 0 = 0.
Proof.
intros n.
induction n as [|n'].
Case "n = 0".
simpl.
reflexivity.
Case "n = S n'".
simpl.
rewrite -> IHn'.
reflexivity.
Qed.
answered Mar 23 at 23:14
Borna SirovecBorna Sirovec
41
add a comment |
Here is what i end up getting:
Lemma neka2 x:
x * 0 = 0.
Proof.
destruct x.
-simpl. reflexivity.
-simpl. (**)
Abort.
Result:
1 subgoal
x : nat
______________________________________(1/1)
x * 0 = 0
I guess you have to prove it with induction because same thing happens when I try to destruct x with predefined mult as well.
Here is x*0=0 proof but with predefined mult:
Theorem mult_0_r : forall n:nat,
n * 0 = 0.
Proof.
intros n.
induction n as [|n'].
Case "n = 0".
simpl.
reflexivity.
Case "n = S n'".
simpl.
rewrite -> IHn'.
reflexivity.
Qed.
answered Mar 23 at 23:14
Borna SirovecBorna Sirovec
41
Here is what i end up getting:
Lemma neka2 x:
x * 0 = 0.
Proof.
destruct x.
-simpl. reflexivity.
-simpl. (**)
Abort.
Result:
1 subgoal
x : nat
______________________________________(1/1)
x * 0 = 0
I guess you have to prove it with induction because same thing happens when I try to destruct x with predefined mult as well.
Here is x*0=0 proof but with predefined mult:
Theorem mult_0_r : forall n:nat,
n * 0 = 0.
Proof.
intros n.
induction n as [|n'].
Case "n = 0".
simpl.
reflexivity.
Case "n = S n'".
simpl.
rewrite -> IHn'.
reflexivity.
Qed.
answered Mar 23 at 23:14
Borna SirovecBorna Sirovec
41
answered Mar 23 at 23:14
Borna SirovecBorna Sirovec
41
answered Mar 23 at 23:14
Borna SirovecBorna Sirovec
41
answered Mar 23 at 23:14
Borna SirovecBorna Sirovec
41
41
add a comment |
add a comment |
As @user138737 pointed out, you don't need induction. It is sufficient to explore three cases : x = 0, x = 1 and x = S (S x')). The shortest proof I can come with is thus the following.
destruct x as [| [|] ]; reflexivity.
answered Apr 4 at 10:20
eponiereponier
2,354418
add a comment |
As @user138737 pointed out, you don't need induction. It is sufficient to explore three cases : x = 0, x = 1 and x = S (S x')). The shortest proof I can come with is thus the following.
destruct x as [| [|] ]; reflexivity.
answered Apr 4 at 10:20
eponiereponier
2,354418
add a comment |
As @user138737 pointed out, you don't need induction. It is sufficient to explore three cases : x = 0, x = 1 and x = S (S x')). The shortest proof I can come with is thus the following.
destruct x as [| [|] ]; reflexivity.
answered Apr 4 at 10:20
eponiereponier
2,354418
As @user138737 pointed out, you don't need induction. It is sufficient to explore three cases : x = 0, x = 1 and x = S (S x')). The shortest proof I can come with is thus the following.
destruct x as [| [|] ]; reflexivity.
answered Apr 4 at 10:20
eponiereponier
2,354418
answered Apr 4 at 10:20
eponiereponier
2,354418
answered Apr 4 at 10:20
eponiereponier
2,354418
answered Apr 4 at 10:20
eponiereponier
2,354418
2,354418
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%2f55316535%2fhow-to-prove-something-by-using-a-definition%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
