Styjun

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;

0

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

share|improve this question

edited Mar 23 at 20:57

double-beep

3,12151632

asked Mar 23 at 17:36

Borna SirovecBorna Sirovec

41

add a comment | 

0

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

share|improve this question

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

share|improve this question

edited Mar 23 at 20:57

double-beep

3,12151632

asked Mar 23 at 17:36

Borna SirovecBorna Sirovec

41

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).

Lemma neka2 x:
 x * 0 = 0.
Proof.
 induction x.
 -simpl. reflexivity.
 -simpl. (*right here*)
Abort.

1 subgoal
x : nat
IHx : x * 0 = 0
______________________________________(1/1)
match x with
| 0 | _ => 0
end = 0

share|improve this question

edited Mar 23 at 20:57

double-beep

3,12151632

asked Mar 23 at 17:36

Borna SirovecBorna Sirovec

41

share|improve this question

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

asked Mar 23 at 17:36

Borna SirovecBorna Sirovec

41

asked Mar 23 at 17:36

Borna SirovecBorna Sirovec

41

3 Answers
3

active

oldest

votes

2

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.

share|improve this answer

answered Mar 23 at 20:15

user138737user138737

31028

add a comment | 

0

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.

share|improve this answer

answered Mar 23 at 23:14

Borna SirovecBorna Sirovec

41

add a comment | 

0

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.

share|improve this answer

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
);



);

draft saved

draft discarded

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

Name

Email

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

Name

Email

Required, but never shown

2

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.

share|improve this answer

answered Mar 23 at 20:15

user138737user138737

31028

add a comment | 

2

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.

share|improve this answer

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.

share|improve this answer

answered Mar 23 at 20:15

user138737user138737

31028

share|improve this answer

answered Mar 23 at 20:15

user138737user138737

31028

answered Mar 23 at 20:15

user138737user138737

31028

answered Mar 23 at 20:15

user138737user138737

31028

0

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.

share|improve this answer

answered Mar 23 at 23:14

Borna SirovecBorna Sirovec

41

add a comment | 

0

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.

share|improve this answer

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.

share|improve this answer

answered Mar 23 at 23:14

Borna SirovecBorna Sirovec

41

Lemma neka2 x:
 x * 0 = 0.
Proof.
 destruct x.
 -simpl. reflexivity.
 -simpl. (**) 
Abort.

1 subgoal
x : nat
______________________________________(1/1)
x * 0 = 0

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.

share|improve this answer

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

0

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.

share|improve this answer

answered Apr 4 at 10:20

eponiereponier

2,354418

add a comment | 

0

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.

share|improve this answer

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.

share|improve this answer

answered Apr 4 at 10:20

eponiereponier

2,354418

destruct x as [| [|] ]; reflexivity.

share|improve this answer

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