Mixing
Non-empty list append theorem in Coq
I am trying to prove the following lemma in Coq:
Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
(a <> / b <> ) -> a ++ b <> .
Right now my current strategy was to destruct on a, and after breaking the disjunction I could ideally just state that if a <> then a ++ b must also be <> ... That was the plan, but I can't seem to get past a subgoal that resembles the first " a ++ b <> ", even when my context clearly states that " b <> ". Any advice?
I've also looked through a lot of the pre-existing list theorems and haven't found anything particularly helpful (minus app_nil_l and app_nil_r, for some subgoals).
ocaml coq theorem-proving coq-tactic formal-verification
edited Nov 22 '18 at 14:06
Julien
3527
asked Nov 20 '18 at 0:48
AkhilAkhil
212
add a comment |
I am trying to prove the following lemma in Coq:
Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
(a <> / b <> ) -> a ++ b <> .
Right now my current strategy was to destruct on a, and after breaking the disjunction I could ideally just state that if a <> then a ++ b must also be <> ... That was the plan, but I can't seem to get past a subgoal that resembles the first " a ++ b <> ", even when my context clearly states that " b <> ". Any advice?
I've also looked through a lot of the pre-existing list theorems and haven't found anything particularly helpful (minus app_nil_l and app_nil_r, for some subgoals).
ocaml coq theorem-proving coq-tactic formal-verification
edited Nov 22 '18 at 14:06
Julien
3527
asked Nov 20 '18 at 0:48
AkhilAkhil
212
"apply app_eq_nil" should be useful. When you have a goal "a <> b" you can use "intro" to show that "a = b" lead to a contradiction.
– Boris E.
Nov 20 '18 at 8:01
Could you please show us the proof script you have so far.
– Julien
Nov 22 '18 at 10:17
add a comment |
I am trying to prove the following lemma in Coq:
Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
(a <> / b <> ) -> a ++ b <> .
Right now my current strategy was to destruct on a, and after breaking the disjunction I could ideally just state that if a <> then a ++ b must also be <> ... That was the plan, but I can't seem to get past a subgoal that resembles the first " a ++ b <> ", even when my context clearly states that " b <> ". Any advice?
I've also looked through a lot of the pre-existing list theorems and haven't found anything particularly helpful (minus app_nil_l and app_nil_r, for some subgoals).
ocaml coq theorem-proving coq-tactic formal-verification
edited Nov 22 '18 at 14:06
Julien
3527
asked Nov 20 '18 at 0:48
AkhilAkhil
212
I am trying to prove the following lemma in Coq:
Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
(a <> / b <> ) -> a ++ b <> .
Right now my current strategy was to destruct on a, and after breaking the disjunction I could ideally just state that if a <> then a ++ b must also be <> ... That was the plan, but I can't seem to get past a subgoal that resembles the first " a ++ b <> ", even when my context clearly states that " b <> ". Any advice?
I've also looked through a lot of the pre-existing list theorems and haven't found anything particularly helpful (minus app_nil_l and app_nil_r, for some subgoals).
ocaml coq theorem-proving coq-tactic formal-verification
ocaml coq theorem-proving coq-tactic formal-verification
edited Nov 22 '18 at 14:06
Julien
3527
asked Nov 20 '18 at 0:48
AkhilAkhil
212
edited Nov 22 '18 at 14:06
Julien
3527
asked Nov 20 '18 at 0:48
AkhilAkhil
212
edited Nov 22 '18 at 14:06
Julien
3527
edited Nov 22 '18 at 14:06
Julien
3527
edited Nov 22 '18 at 14:06
Julien
3527
3527
asked Nov 20 '18 at 0:48
AkhilAkhil
212
asked Nov 20 '18 at 0:48
AkhilAkhil
212
asked Nov 20 '18 at 0:48
AkhilAkhil
212
212
"apply app_eq_nil" should be useful. When you have a goal "a <> b" you can use "intro" to show that "a = b" lead to a contradiction.
– Boris E.
Nov 20 '18 at 8:01
Could you please show us the proof script you have so far.
– Julien
Nov 22 '18 at 10:17
add a comment |
"apply app_eq_nil" should be useful. When you have a goal "a <> b" you can use "intro" to show that "a = b" lead to a contradiction.
– Boris E.
Nov 20 '18 at 8:01
Could you please show us the proof script you have so far.
– Julien
Nov 22 '18 at 10:17
"apply app_eq_nil" should be useful. When you have a goal "a <> b" you can use "intro" to show that "a = b" lead to a contradiction.
– Boris E.
Nov 20 '18 at 8:01
"apply app_eq_nil" should be useful. When you have a goal "a <> b" you can use "intro" to show that "a = b" lead to a contradiction.
– Boris E.
Nov 20 '18 at 8:01
Could you please show us the proof script you have so far.
– Julien
Nov 22 '18 at 10:17
Could you please show us the proof script you have so far.
– Julien
Nov 22 '18 at 10:17
add a comment |
3 Answers
3
active
oldest
votes
first, I am not sure which Coq version you are using, the syntax certainly looks odd. Seconds, it is hard for us to help if you don't show us the proof you have so far. I should say that indeed your strategy seems correct, you should destruct both lists, tho it is better if you first inspect the or to see which list is not empty.
Another option is to use computation to show your lemma, in this case, equality will compute and thus you will get the result of the comparison. It suffices to destroy only one list in this case due the order or arguments:
From mathcomp Require Import all_ssreflect.
Lemma not_empty (A : eqType) (a b : seq A) :
[|| a != [::] | b != [::]] -> a ++ b != [::].
Proof. by case: a. Qed.
answered Nov 21 '18 at 1:54
ejgallegoejgallego
5,3541925
add a comment |
You started the right way with your destruct a.
You should end up at some point with a0::a++b<>0. It ressembles a++b<>0 but it is quite different as you have a cons here, thus discriminate knows that it is different from nil.
answered Nov 22 '18 at 10:18
JulienJulien
3527
add a comment |
Starting with destruct a is a good idea indeed.
For the case where a is Nil, you should destruct the (a <> / b <> ) hypothesis. There will be two cases:
- the right one the hypothesis
<>is acontradiction, - the left one, the hypothesis
b <>is your goal (sincea =)
For the case where a is a :: a0, you should use discriminate as Julien said.
answered Nov 22 '18 at 15:42
BrunoBruno
234
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%2f53384688%2fnon-empty-list-append-theorem-in-coq%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
first, I am not sure which Coq version you are using, the syntax certainly looks odd. Seconds, it is hard for us to help if you don't show us the proof you have so far. I should say that indeed your strategy seems correct, you should destruct both lists, tho it is better if you first inspect the or to see which list is not empty.
Another option is to use computation to show your lemma, in this case, equality will compute and thus you will get the result of the comparison. It suffices to destroy only one list in this case due the order or arguments:
From mathcomp Require Import all_ssreflect.
Lemma not_empty (A : eqType) (a b : seq A) :
[|| a != [::] | b != [::]] -> a ++ b != [::].
Proof. by case: a. Qed.
answered Nov 21 '18 at 1:54
ejgallegoejgallego
5,3541925
add a comment |
first, I am not sure which Coq version you are using, the syntax certainly looks odd. Seconds, it is hard for us to help if you don't show us the proof you have so far. I should say that indeed your strategy seems correct, you should destruct both lists, tho it is better if you first inspect the or to see which list is not empty.
Another option is to use computation to show your lemma, in this case, equality will compute and thus you will get the result of the comparison. It suffices to destroy only one list in this case due the order or arguments:
From mathcomp Require Import all_ssreflect.
Lemma not_empty (A : eqType) (a b : seq A) :
[|| a != [::] | b != [::]] -> a ++ b != [::].
Proof. by case: a. Qed.
answered Nov 21 '18 at 1:54
ejgallegoejgallego
5,3541925
add a comment |
first, I am not sure which Coq version you are using, the syntax certainly looks odd. Seconds, it is hard for us to help if you don't show us the proof you have so far. I should say that indeed your strategy seems correct, you should destruct both lists, tho it is better if you first inspect the or to see which list is not empty.
Another option is to use computation to show your lemma, in this case, equality will compute and thus you will get the result of the comparison. It suffices to destroy only one list in this case due the order or arguments:
From mathcomp Require Import all_ssreflect.
Lemma not_empty (A : eqType) (a b : seq A) :
[|| a != [::] | b != [::]] -> a ++ b != [::].
Proof. by case: a. Qed.
answered Nov 21 '18 at 1:54
ejgallegoejgallego
5,3541925
first, I am not sure which Coq version you are using, the syntax certainly looks odd. Seconds, it is hard for us to help if you don't show us the proof you have so far. I should say that indeed your strategy seems correct, you should destruct both lists, tho it is better if you first inspect the or to see which list is not empty.
Another option is to use computation to show your lemma, in this case, equality will compute and thus you will get the result of the comparison. It suffices to destroy only one list in this case due the order or arguments:
From mathcomp Require Import all_ssreflect.
Lemma not_empty (A : eqType) (a b : seq A) :
[|| a != [::] | b != [::]] -> a ++ b != [::].
Proof. by case: a. Qed.
answered Nov 21 '18 at 1:54
ejgallegoejgallego
5,3541925
answered Nov 21 '18 at 1:54
ejgallegoejgallego
5,3541925
answered Nov 21 '18 at 1:54
ejgallegoejgallego
5,3541925
answered Nov 21 '18 at 1:54
ejgallegoejgallego
5,3541925
5,3541925
add a comment |
add a comment |
You started the right way with your destruct a.
You should end up at some point with a0::a++b<>0. It ressembles a++b<>0 but it is quite different as you have a cons here, thus discriminate knows that it is different from nil.
answered Nov 22 '18 at 10:18
JulienJulien
3527
add a comment |
You started the right way with your destruct a.
You should end up at some point with a0::a++b<>0. It ressembles a++b<>0 but it is quite different as you have a cons here, thus discriminate knows that it is different from nil.
answered Nov 22 '18 at 10:18
JulienJulien
3527
add a comment |
You started the right way with your destruct a.
You should end up at some point with a0::a++b<>0. It ressembles a++b<>0 but it is quite different as you have a cons here, thus discriminate knows that it is different from nil.
answered Nov 22 '18 at 10:18
JulienJulien
3527
You started the right way with your destruct a.
You should end up at some point with a0::a++b<>0. It ressembles a++b<>0 but it is quite different as you have a cons here, thus discriminate knows that it is different from nil.
answered Nov 22 '18 at 10:18
JulienJulien
3527
answered Nov 22 '18 at 10:18
JulienJulien
3527
answered Nov 22 '18 at 10:18
JulienJulien
3527
answered Nov 22 '18 at 10:18
JulienJulien
3527
3527
add a comment |
add a comment |
Starting with destruct a is a good idea indeed.
For the case where a is Nil, you should destruct the (a <> / b <> ) hypothesis. There will be two cases:
- the right one the hypothesis
<>is acontradiction, - the left one, the hypothesis
b <>is your goal (sincea =)
For the case where a is a :: a0, you should use discriminate as Julien said.
answered Nov 22 '18 at 15:42
BrunoBruno
234
add a comment |
Starting with destruct a is a good idea indeed.
For the case where a is Nil, you should destruct the (a <> / b <> ) hypothesis. There will be two cases:
- the right one the hypothesis
<>is acontradiction, - the left one, the hypothesis
b <>is your goal (sincea =)
For the case where a is a :: a0, you should use discriminate as Julien said.
answered Nov 22 '18 at 15:42
BrunoBruno
234
add a comment |
Starting with destruct a is a good idea indeed.
For the case where a is Nil, you should destruct the (a <> / b <> ) hypothesis. There will be two cases:
- the right one the hypothesis
<>is acontradiction, - the left one, the hypothesis
b <>is your goal (sincea =)
For the case where a is a :: a0, you should use discriminate as Julien said.
answered Nov 22 '18 at 15:42
BrunoBruno
234
Starting with destruct a is a good idea indeed.
For the case where a is Nil, you should destruct the (a <> / b <> ) hypothesis. There will be two cases:
- the right one the hypothesis
<>is acontradiction, - the left one, the hypothesis
b <>is your goal (sincea =)
For the case where a is a :: a0, you should use discriminate as Julien said.
answered Nov 22 '18 at 15:42
BrunoBruno
234
answered Nov 22 '18 at 15:42
BrunoBruno
234
answered Nov 22 '18 at 15:42
BrunoBruno
234
answered Nov 22 '18 at 15:42
BrunoBruno
234
234
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%2f53384688%2fnon-empty-list-append-theorem-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
"apply app_eq_nil" should be useful. When you have a goal "a <> b" you can use "intro" to show that "a = b" lead to a contradiction.
– Boris E.
Nov 20 '18 at 8:01
Could you please show us the proof script you have so far.
– Julien
Nov 22 '18 at 10:17