Reasoning about overlapping inductive definitions in Isabelle
I would like to prove the following lemma in Isabelle:
lemma "T (Open # xs) ⟹ ¬ S (Open # xs) ⟹ count xs Close ≤ count xs Open"
Please find the definitions below:
datatype paren = Open | Close
inductive S where
S_empty: "S " |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T " |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
The lemma states that an unbalanced parentheses structure would result in a possibly unbalanced structure when removing an Open
bracket.
I've been trying the techniques that are described in the book "A proof-assistant for Higher-order logic", but so far none of them work. In particular, I tried to use rule inversion and rule induction, sledgehammer
and other techniques.
One of the problems is that I haven't yet learned about Isar proofs, which thus complicates the proof. I would prefer if you can orient me with plain apply commands.
isabelle proof
add a comment |
I would like to prove the following lemma in Isabelle:
lemma "T (Open # xs) ⟹ ¬ S (Open # xs) ⟹ count xs Close ≤ count xs Open"
Please find the definitions below:
datatype paren = Open | Close
inductive S where
S_empty: "S " |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T " |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
The lemma states that an unbalanced parentheses structure would result in a possibly unbalanced structure when removing an Open
bracket.
I've been trying the techniques that are described in the book "A proof-assistant for Higher-order logic", but so far none of them work. In particular, I tried to use rule inversion and rule induction, sledgehammer
and other techniques.
One of the problems is that I haven't yet learned about Isar proofs, which thus complicates the proof. I would prefer if you can orient me with plain apply commands.
isabelle proof
add a comment |
I would like to prove the following lemma in Isabelle:
lemma "T (Open # xs) ⟹ ¬ S (Open # xs) ⟹ count xs Close ≤ count xs Open"
Please find the definitions below:
datatype paren = Open | Close
inductive S where
S_empty: "S " |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T " |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
The lemma states that an unbalanced parentheses structure would result in a possibly unbalanced structure when removing an Open
bracket.
I've been trying the techniques that are described in the book "A proof-assistant for Higher-order logic", but so far none of them work. In particular, I tried to use rule inversion and rule induction, sledgehammer
and other techniques.
One of the problems is that I haven't yet learned about Isar proofs, which thus complicates the proof. I would prefer if you can orient me with plain apply commands.
isabelle proof
I would like to prove the following lemma in Isabelle:
lemma "T (Open # xs) ⟹ ¬ S (Open # xs) ⟹ count xs Close ≤ count xs Open"
Please find the definitions below:
datatype paren = Open | Close
inductive S where
S_empty: "S " |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T " |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
The lemma states that an unbalanced parentheses structure would result in a possibly unbalanced structure when removing an Open
bracket.
I've been trying the techniques that are described in the book "A proof-assistant for Higher-order logic", but so far none of them work. In particular, I tried to use rule inversion and rule induction, sledgehammer
and other techniques.
One of the problems is that I haven't yet learned about Isar proofs, which thus complicates the proof. I would prefer if you can orient me with plain apply commands.
isabelle proof
isabelle proof
edited Nov 3 '18 at 15:26
xanonec
537113
537113
asked Nov 3 '18 at 1:44
JavierJavier
653723
653723
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
Please find a proof below. It is not unlikely that it can be improved: I tried to follow the simplest route towards the proof and relied on sledgehammer
to fill in the details.
theory so_raoidii
imports Complex_Main
begin
declare [[show_types]]
declare [[show_sorts]]
datatype paren = Open | Close
inductive S where
S_empty: "S " |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T " |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
lemma count_list_lem:
"count_list xsa a = n ⟹
count_list ysa a = m ⟹
count_list (xsa @ ysa) a = n + m"
apply(induction xsa arbitrary: ysa n m)
apply auto
done
lemma T_to_count: "T xs ⟹ count_list xs Close ≤ count_list xs Open"
apply(induction rule: T.induct)
by (simp add: count_list_lem)+
lemma T_to_S_count: "T xs ⟹ count_list xs Close = count_list xs Open ⟹ S xs"
apply(induction rule: T.induct)
apply(auto)
apply(simp add: S_empty)
apply(metis S_append T_to_count add.commute add_le_cancel_right count_list_lem
dual_order.antisym)
apply(simp add: count_list_lem S_paren)
using T_to_count by fastforce
lemma "T (Open # xs) ⟹
¬ S (Open # xs) ⟹
count_list xs Close ≤ count_list xs Open"
apply(cases "T xs")
apply(simp add: T_to_count)
using T_to_S_count T_to_count by fastforce
end
i wonder which provers you have in sledgehammer. i think this is one of my problems that vampire is not working well and only have cvc4
– Javier
Nov 3 '18 at 14:23
@Rodrigo I am not certain what exactly do you mean by the phrase "vampire is not working well". If you suspect that vampire is not working how it should, then it may be best to ask another question about it (however, this is not something I could help you with). To answer your question, I only use cvc4 and vampire. Also, please note that I meant to say that I relied onsledgehammer
to fill in the details in my (virtual) 'pen and paper-based' proof outline. Of course, before typesetting the proof in Isabelle, I did produce a proof outline in my mind.
– xanonec
Nov 3 '18 at 14:33
ok, thanks for the clarification, in particular the step with smt is not found by my sledgehammer, ill have to work on it.
– Javier
Nov 3 '18 at 14:41
@Rodrigo I believe that I created thesmt
step from an explicit Isar lemma that I had in my original answer before editing it. Indeed, I was not able to usesledgehammer
for this step withinT_to_S_count
.
– xanonec
Nov 3 '18 at 14:49
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%2f53127680%2freasoning-about-overlapping-inductive-definitions-in-isabelle%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
Please find a proof below. It is not unlikely that it can be improved: I tried to follow the simplest route towards the proof and relied on sledgehammer
to fill in the details.
theory so_raoidii
imports Complex_Main
begin
declare [[show_types]]
declare [[show_sorts]]
datatype paren = Open | Close
inductive S where
S_empty: "S " |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T " |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
lemma count_list_lem:
"count_list xsa a = n ⟹
count_list ysa a = m ⟹
count_list (xsa @ ysa) a = n + m"
apply(induction xsa arbitrary: ysa n m)
apply auto
done
lemma T_to_count: "T xs ⟹ count_list xs Close ≤ count_list xs Open"
apply(induction rule: T.induct)
by (simp add: count_list_lem)+
lemma T_to_S_count: "T xs ⟹ count_list xs Close = count_list xs Open ⟹ S xs"
apply(induction rule: T.induct)
apply(auto)
apply(simp add: S_empty)
apply(metis S_append T_to_count add.commute add_le_cancel_right count_list_lem
dual_order.antisym)
apply(simp add: count_list_lem S_paren)
using T_to_count by fastforce
lemma "T (Open # xs) ⟹
¬ S (Open # xs) ⟹
count_list xs Close ≤ count_list xs Open"
apply(cases "T xs")
apply(simp add: T_to_count)
using T_to_S_count T_to_count by fastforce
end
i wonder which provers you have in sledgehammer. i think this is one of my problems that vampire is not working well and only have cvc4
– Javier
Nov 3 '18 at 14:23
@Rodrigo I am not certain what exactly do you mean by the phrase "vampire is not working well". If you suspect that vampire is not working how it should, then it may be best to ask another question about it (however, this is not something I could help you with). To answer your question, I only use cvc4 and vampire. Also, please note that I meant to say that I relied onsledgehammer
to fill in the details in my (virtual) 'pen and paper-based' proof outline. Of course, before typesetting the proof in Isabelle, I did produce a proof outline in my mind.
– xanonec
Nov 3 '18 at 14:33
ok, thanks for the clarification, in particular the step with smt is not found by my sledgehammer, ill have to work on it.
– Javier
Nov 3 '18 at 14:41
@Rodrigo I believe that I created thesmt
step from an explicit Isar lemma that I had in my original answer before editing it. Indeed, I was not able to usesledgehammer
for this step withinT_to_S_count
.
– xanonec
Nov 3 '18 at 14:49
add a comment |
Please find a proof below. It is not unlikely that it can be improved: I tried to follow the simplest route towards the proof and relied on sledgehammer
to fill in the details.
theory so_raoidii
imports Complex_Main
begin
declare [[show_types]]
declare [[show_sorts]]
datatype paren = Open | Close
inductive S where
S_empty: "S " |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T " |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
lemma count_list_lem:
"count_list xsa a = n ⟹
count_list ysa a = m ⟹
count_list (xsa @ ysa) a = n + m"
apply(induction xsa arbitrary: ysa n m)
apply auto
done
lemma T_to_count: "T xs ⟹ count_list xs Close ≤ count_list xs Open"
apply(induction rule: T.induct)
by (simp add: count_list_lem)+
lemma T_to_S_count: "T xs ⟹ count_list xs Close = count_list xs Open ⟹ S xs"
apply(induction rule: T.induct)
apply(auto)
apply(simp add: S_empty)
apply(metis S_append T_to_count add.commute add_le_cancel_right count_list_lem
dual_order.antisym)
apply(simp add: count_list_lem S_paren)
using T_to_count by fastforce
lemma "T (Open # xs) ⟹
¬ S (Open # xs) ⟹
count_list xs Close ≤ count_list xs Open"
apply(cases "T xs")
apply(simp add: T_to_count)
using T_to_S_count T_to_count by fastforce
end
i wonder which provers you have in sledgehammer. i think this is one of my problems that vampire is not working well and only have cvc4
– Javier
Nov 3 '18 at 14:23
@Rodrigo I am not certain what exactly do you mean by the phrase "vampire is not working well". If you suspect that vampire is not working how it should, then it may be best to ask another question about it (however, this is not something I could help you with). To answer your question, I only use cvc4 and vampire. Also, please note that I meant to say that I relied onsledgehammer
to fill in the details in my (virtual) 'pen and paper-based' proof outline. Of course, before typesetting the proof in Isabelle, I did produce a proof outline in my mind.
– xanonec
Nov 3 '18 at 14:33
ok, thanks for the clarification, in particular the step with smt is not found by my sledgehammer, ill have to work on it.
– Javier
Nov 3 '18 at 14:41
@Rodrigo I believe that I created thesmt
step from an explicit Isar lemma that I had in my original answer before editing it. Indeed, I was not able to usesledgehammer
for this step withinT_to_S_count
.
– xanonec
Nov 3 '18 at 14:49
add a comment |
Please find a proof below. It is not unlikely that it can be improved: I tried to follow the simplest route towards the proof and relied on sledgehammer
to fill in the details.
theory so_raoidii
imports Complex_Main
begin
declare [[show_types]]
declare [[show_sorts]]
datatype paren = Open | Close
inductive S where
S_empty: "S " |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T " |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
lemma count_list_lem:
"count_list xsa a = n ⟹
count_list ysa a = m ⟹
count_list (xsa @ ysa) a = n + m"
apply(induction xsa arbitrary: ysa n m)
apply auto
done
lemma T_to_count: "T xs ⟹ count_list xs Close ≤ count_list xs Open"
apply(induction rule: T.induct)
by (simp add: count_list_lem)+
lemma T_to_S_count: "T xs ⟹ count_list xs Close = count_list xs Open ⟹ S xs"
apply(induction rule: T.induct)
apply(auto)
apply(simp add: S_empty)
apply(metis S_append T_to_count add.commute add_le_cancel_right count_list_lem
dual_order.antisym)
apply(simp add: count_list_lem S_paren)
using T_to_count by fastforce
lemma "T (Open # xs) ⟹
¬ S (Open # xs) ⟹
count_list xs Close ≤ count_list xs Open"
apply(cases "T xs")
apply(simp add: T_to_count)
using T_to_S_count T_to_count by fastforce
end
Please find a proof below. It is not unlikely that it can be improved: I tried to follow the simplest route towards the proof and relied on sledgehammer
to fill in the details.
theory so_raoidii
imports Complex_Main
begin
declare [[show_types]]
declare [[show_sorts]]
datatype paren = Open | Close
inductive S where
S_empty: "S " |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T " |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
lemma count_list_lem:
"count_list xsa a = n ⟹
count_list ysa a = m ⟹
count_list (xsa @ ysa) a = n + m"
apply(induction xsa arbitrary: ysa n m)
apply auto
done
lemma T_to_count: "T xs ⟹ count_list xs Close ≤ count_list xs Open"
apply(induction rule: T.induct)
by (simp add: count_list_lem)+
lemma T_to_S_count: "T xs ⟹ count_list xs Close = count_list xs Open ⟹ S xs"
apply(induction rule: T.induct)
apply(auto)
apply(simp add: S_empty)
apply(metis S_append T_to_count add.commute add_le_cancel_right count_list_lem
dual_order.antisym)
apply(simp add: count_list_lem S_paren)
using T_to_count by fastforce
lemma "T (Open # xs) ⟹
¬ S (Open # xs) ⟹
count_list xs Close ≤ count_list xs Open"
apply(cases "T xs")
apply(simp add: T_to_count)
using T_to_S_count T_to_count by fastforce
end
edited Nov 24 '18 at 20:34
answered Nov 3 '18 at 13:42
xanonecxanonec
537113
537113
i wonder which provers you have in sledgehammer. i think this is one of my problems that vampire is not working well and only have cvc4
– Javier
Nov 3 '18 at 14:23
@Rodrigo I am not certain what exactly do you mean by the phrase "vampire is not working well". If you suspect that vampire is not working how it should, then it may be best to ask another question about it (however, this is not something I could help you with). To answer your question, I only use cvc4 and vampire. Also, please note that I meant to say that I relied onsledgehammer
to fill in the details in my (virtual) 'pen and paper-based' proof outline. Of course, before typesetting the proof in Isabelle, I did produce a proof outline in my mind.
– xanonec
Nov 3 '18 at 14:33
ok, thanks for the clarification, in particular the step with smt is not found by my sledgehammer, ill have to work on it.
– Javier
Nov 3 '18 at 14:41
@Rodrigo I believe that I created thesmt
step from an explicit Isar lemma that I had in my original answer before editing it. Indeed, I was not able to usesledgehammer
for this step withinT_to_S_count
.
– xanonec
Nov 3 '18 at 14:49
add a comment |
i wonder which provers you have in sledgehammer. i think this is one of my problems that vampire is not working well and only have cvc4
– Javier
Nov 3 '18 at 14:23
@Rodrigo I am not certain what exactly do you mean by the phrase "vampire is not working well". If you suspect that vampire is not working how it should, then it may be best to ask another question about it (however, this is not something I could help you with). To answer your question, I only use cvc4 and vampire. Also, please note that I meant to say that I relied onsledgehammer
to fill in the details in my (virtual) 'pen and paper-based' proof outline. Of course, before typesetting the proof in Isabelle, I did produce a proof outline in my mind.
– xanonec
Nov 3 '18 at 14:33
ok, thanks for the clarification, in particular the step with smt is not found by my sledgehammer, ill have to work on it.
– Javier
Nov 3 '18 at 14:41
@Rodrigo I believe that I created thesmt
step from an explicit Isar lemma that I had in my original answer before editing it. Indeed, I was not able to usesledgehammer
for this step withinT_to_S_count
.
– xanonec
Nov 3 '18 at 14:49
i wonder which provers you have in sledgehammer. i think this is one of my problems that vampire is not working well and only have cvc4
– Javier
Nov 3 '18 at 14:23
i wonder which provers you have in sledgehammer. i think this is one of my problems that vampire is not working well and only have cvc4
– Javier
Nov 3 '18 at 14:23
@Rodrigo I am not certain what exactly do you mean by the phrase "vampire is not working well". If you suspect that vampire is not working how it should, then it may be best to ask another question about it (however, this is not something I could help you with). To answer your question, I only use cvc4 and vampire. Also, please note that I meant to say that I relied on
sledgehammer
to fill in the details in my (virtual) 'pen and paper-based' proof outline. Of course, before typesetting the proof in Isabelle, I did produce a proof outline in my mind.– xanonec
Nov 3 '18 at 14:33
@Rodrigo I am not certain what exactly do you mean by the phrase "vampire is not working well". If you suspect that vampire is not working how it should, then it may be best to ask another question about it (however, this is not something I could help you with). To answer your question, I only use cvc4 and vampire. Also, please note that I meant to say that I relied on
sledgehammer
to fill in the details in my (virtual) 'pen and paper-based' proof outline. Of course, before typesetting the proof in Isabelle, I did produce a proof outline in my mind.– xanonec
Nov 3 '18 at 14:33
ok, thanks for the clarification, in particular the step with smt is not found by my sledgehammer, ill have to work on it.
– Javier
Nov 3 '18 at 14:41
ok, thanks for the clarification, in particular the step with smt is not found by my sledgehammer, ill have to work on it.
– Javier
Nov 3 '18 at 14:41
@Rodrigo I believe that I created the
smt
step from an explicit Isar lemma that I had in my original answer before editing it. Indeed, I was not able to use sledgehammer
for this step within T_to_S_count
.– xanonec
Nov 3 '18 at 14:49
@Rodrigo I believe that I created the
smt
step from an explicit Isar lemma that I had in my original answer before editing it. Indeed, I was not able to use sledgehammer
for this step within T_to_S_count
.– xanonec
Nov 3 '18 at 14:49
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%2f53127680%2freasoning-about-overlapping-inductive-definitions-in-isabelle%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