Splitting disjunctions (/) in Coq hypothesisProving if then else in CoqHow to apply a Coq hypothesis of the form A = B -> C = D to a subgoal of the form A = BCoq - Error when eliminating ORWhat forms of goal in Coq are considered to be “true”?“Rewrite” a typeHow to make Coq evaluate a specific redex (or - why does it refuse in this case?)How to destruct pair equivalence in Coq?Rewrite hypothesis in Coq, keeping implicationCoq: Rewriting with 'forall' in hypothesis or goalNon-empty list append theorem in Coq
Is CD audio quality good enough for the final delivery of music?
What do different value notes on the same line mean?
Four-in-a-line Puzzle
How do you say “buy” in the sense of “believe”?
Does this degree 12 genus 1 curve have only one point over infinitely many finite fields?
Why colon to denote that a value belongs to a type?
Does revoking a certificate result in revocation of its key?
How many chess players are over 2500 Elo?
Why does the 'metric Lagrangian' approach appear to fail in Newtonian mechanics?
Seed ship, unsexed person, cover has golden person attached to ship by umbilical cord
Would jet fuel for an F-16 or F-35 be producible during WW2?
How were these pictures of spacecraft wind tunnel testing taken?
Placing bypass capacitors after VCC reaches the IC
Is the first derivative operation on a signal a causal system?
General purpose replacement for enum with FlagsAttribute
When and what was the first 3D acceleration device ever released?
How can people dance around bonfires on Lag Lo'Omer - it's darchei emori?
What is the object moving across the ceiling in this stock footage?
Logarithm of dependent variable is uniformly distributed. How to calculate a confidence interval for the mean?
Employer demanding to see degree after poor code review
Where is the logic in castrating fighters?
Full horizontal justification in table
How did early x86 BIOS programmers manage to program full blown TUIs given very few bytes of ROM/EPROM?
Rename photos to match video titles
Splitting disjunctions (/) in Coq hypothesis
Proving if then else in CoqHow to apply a Coq hypothesis of the form A = B -> C = D to a subgoal of the form A = BCoq - Error when eliminating ORWhat forms of goal in Coq are considered to be “true”?“Rewrite” a typeHow to make Coq evaluate a specific redex (or - why does it refuse in this case?)How to destruct pair equivalence in Coq?Rewrite hypothesis in Coq, keeping implicationCoq: Rewriting with 'forall' in hypothesis or goalNon-empty list append theorem in Coq
.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty height:90px;width:728px;box-sizing:border-box;
I'm trying to prove a simple lemma in Coq where the hypothesis is a disjunction. I know how to split disjunctions when they occur in the goal,
but can't manage to split them when they appear in the hypothesis. Here is my example:
Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
Proof.
intros n H1.
split H1. (** this doesn't work ... *)
And here is what Coq says:
1 subgoal
n : nat
H1 : n < 5 / n > 8
______________________________________(1/1)
n > 7 / n < 6
With error:
Error: Illegal tactic application.
I'm clearly missing something simple.
Any help is very much appreciated, thanks!
coq
asked Mar 24 at 6:38
OrenIshShalomOrenIshShalom
1,239924
add a comment |
I'm trying to prove a simple lemma in Coq where the hypothesis is a disjunction. I know how to split disjunctions when they occur in the goal,
but can't manage to split them when they appear in the hypothesis. Here is my example:
Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
Proof.
intros n H1.
split H1. (** this doesn't work ... *)
And here is what Coq says:
1 subgoal
n : nat
H1 : n < 5 / n > 8
______________________________________(1/1)
n > 7 / n < 6
With error:
Error: Illegal tactic application.
I'm clearly missing something simple.
Any help is very much appreciated, thanks!
coq
asked Mar 24 at 6:38
OrenIshShalomOrenIshShalom
1,239924
add a comment |
I'm trying to prove a simple lemma in Coq where the hypothesis is a disjunction. I know how to split disjunctions when they occur in the goal,
but can't manage to split them when they appear in the hypothesis. Here is my example:
Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
Proof.
intros n H1.
split H1. (** this doesn't work ... *)
And here is what Coq says:
1 subgoal
n : nat
H1 : n < 5 / n > 8
______________________________________(1/1)
n > 7 / n < 6
With error:
Error: Illegal tactic application.
I'm clearly missing something simple.
Any help is very much appreciated, thanks!
coq
asked Mar 24 at 6:38
OrenIshShalomOrenIshShalom
1,239924
I'm trying to prove a simple lemma in Coq where the hypothesis is a disjunction. I know how to split disjunctions when they occur in the goal,
but can't manage to split them when they appear in the hypothesis. Here is my example:
Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
Proof.
intros n H1.
split H1. (** this doesn't work ... *)
And here is what Coq says:
1 subgoal
n : nat
H1 : n < 5 / n > 8
______________________________________(1/1)
n > 7 / n < 6
With error:
Error: Illegal tactic application.
I'm clearly missing something simple.
Any help is very much appreciated, thanks!
coq
coq
asked Mar 24 at 6:38
OrenIshShalomOrenIshShalom
1,239924
asked Mar 24 at 6:38
OrenIshShalomOrenIshShalom
1,239924
asked Mar 24 at 6:38
OrenIshShalomOrenIshShalom
1,239924
asked Mar 24 at 6:38
OrenIshShalomOrenIshShalom
1,239924
asked Mar 24 at 6:38
OrenIshShalomOrenIshShalom
1,239924
1,239924
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
The tactic you want is destruct.
Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
Proof.
intros n H1.
destruct H1.
If you want to name the resulting hypotheses you can do destruct H1 as [name1 | name2]..
answered Mar 24 at 7:30
UserUser
1,8391710
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%2f55321328%2fsplitting-disjunctions-in-coq-hypothesis%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
The tactic you want is destruct.
Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
Proof.
intros n H1.
destruct H1.
If you want to name the resulting hypotheses you can do destruct H1 as [name1 | name2]..
answered Mar 24 at 7:30
UserUser
1,8391710
add a comment |
The tactic you want is destruct.
Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
Proof.
intros n H1.
destruct H1.
If you want to name the resulting hypotheses you can do destruct H1 as [name1 | name2]..
answered Mar 24 at 7:30
UserUser
1,8391710
add a comment |
The tactic you want is destruct.
Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
Proof.
intros n H1.
destruct H1.
If you want to name the resulting hypotheses you can do destruct H1 as [name1 | name2]..
answered Mar 24 at 7:30
UserUser
1,8391710
The tactic you want is destruct.
Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
((n < 5) / (n > 8)) -> ((n > 7) / (n < 6)).
Proof.
intros n H1.
destruct H1.
If you want to name the resulting hypotheses you can do destruct H1 as [name1 | name2]..
answered Mar 24 at 7:30
UserUser
1,8391710
answered Mar 24 at 7:30
UserUser
1,8391710
answered Mar 24 at 7:30
UserUser
1,8391710
answered Mar 24 at 7:30
UserUser
1,8391710
1,8391710
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%2f55321328%2fsplitting-disjunctions-in-coq-hypothesis%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
