Email Gateway (Aug 18 2022 at 09:46): Email Gateway (Aug 18 2022 at 09:46):From: D Mulligan <s0346804@sms.ed.ac.uk>
Hi,
I've been formulating some Prolog relations in Isabelle using
inductively defined sets. I've managed to prove some theorems about
relations that are defined entirely within themselves (i.e. plus), but
when I try to prove theorems about relations defined in terms of other
relations, for example the reverse of a list, defined in terms of
itself and append, I hit a wall. My reverse definition is below:
consts
reverse_inductive :: "('a list * 'a list) set"
syntax
reverse :: "'a list => 'a list => bool"
translations
"reverse l r" == "(l, r) \<in> reverse_inductive"
inductive reverse_inductive
intros
nil [intro!]: "reverse [] []"
notnil [intro!]: "(append r [h] a) /\ (reverse t r) ==> (reverse
(h#t) a)"
I'm attempting to prove that the reverse of a reverse of a list is the
same list. I have a lemma that states that states \<exists>c. append a
b c. It's been suggested to me that I use this lemma with rule exE[OF
..] in the proof, but no matter how I attempt to use it I cannot get
the proof to go through.
An attempt at the proof is included below:
theorem reverse_reverse_l:
"\<exists>l'.(reverse l l') /\ (reverse l' l)"
apply(induct_tac l)
apply(rule exI)
apply(rule conjI)
apply(rule reverse_inductive.nil)+
apply(rule exE[OF ex_append])
apply(rule exI)
apply(erule exE)
apply(erule conjE)
apply(rule conjI)
apply(rule reverse_inductive.notnil)
apply(rule conjI)
apply(assumption)
sorry (* Stuck! *)
The problem (as I see it) is in the step case when I apply
reverse_inductive.notnil. Is anybody able to offer any advice as to
how I would go about proving this theorem?
Please note, I'm not using the Isar proof style for a reason. For your
convenience I've attached a theory file with my relations and proofs in
(scroll to the bottom for the relevant proof attempt).
Many thanks for any help offered,
Dominic Mulligan
PrologInductiveSets.thy
Email Gateway (Aug 18 2022 at 09:46):From: Brian Huffman <brianh@csee.ogi.edu>
Hi Dominic,
Since you do not instantiate variables in your rule applications, your proof
state often contains schematic variables that are instantiated later as
needed. (These are the ones written with a leading question mark.)
You need to pay attention to the parameters that these schematic variables
have. In particular, a schematic variable can not be instantiated to a term
that contains variables that were created after the schematic variable was.
In your proof below, "rule exE[OF ex_append]" introduces two schematic
variables, and afterward "erule exE" obtains a new variable l'. Later, you
would like to instantiate the schematic variable to l' but you can't, because
l' did not exist when the schematic variable was created. You might want to
try putting "erule exE" a few steps earlier.
Having unbound schematic variables in your proof state is often very
confusing. I would recommend instantiating your rules as you apply them
instead, i.e. use something like (rule_tac x="list" in exI) instead of just
(rule exI).
Hope this helps.
On Wednesday 04 October 2006 04:57, D Mulligan wrote:
...
I'm attempting to prove that the reverse of a reverse of a list is the
same list. I have a lemma that states that states \<exists>c. append a
b c. It's been suggested to me that I use this lemma with rule exE[OF
..] in the proof, but no matter how I attempt to use it I cannot get
the proof to go through.An attempt at the proof is included below:
theorem reverse_reverse_l:
"\<exists>l'.(reverse l l') /\ (reverse l' l)"
apply(induct_tac l)
apply(rule exI)
apply(rule conjI)
apply(rule reverse_inductive.nil)+
-- variables from induction rule: a, list
apply(rule exE[OF ex_append])
-- introduces schematic variables parameterized on a, list
-- obtains variable x
apply(rule exI)
-- introduces schematic variable parameterized on a, list, x
apply(erule exE)
-- obtains variable l'
apply(erule conjE)
apply(rule conjI)
apply(rule reverse_inductive.notnil)
apply(rule conjI)
apply(assumption)
-- can't apply assumption again because schematic variable
-- must not depend on l'
sorry (* Stuck! *)
Email Gateway (Aug 18 2022 at 09:46):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
I think you will also need a lemma:
theorem reverse_append2:
"\<lbrakk> append r [h] l; reverse r t \<rbrakk> \<Longrightarrow>
reverse l (h#t)"
sorry
This is the opposite case of your reverse definition. With this you
should be able to prove:
theorem reverse_reverse_l:
"\<exists>l'.(reverse l l') \<and> (reverse l' l)"
apply(induct_tac l)
apply(rule exI)
apply(rule conjI)
apply(rule reverse_inductive.nil)+
apply(erule exE)
apply(erule conjE)
apply(rule exE) (* the exE step you mentioned: for the result of
append in the definition of reverse *)
defer
apply(rule exI)
apply(rule conjI)
apply(rule reverse_inductive.notnil)
apply(rule conjI)
defer
apply assumption
apply(rule reverse_append2)
defer
apply assumption
defer
apply assumption
apply assumption
apply (rule ex_append)
done
I'm not sure if this is the most efficient proof... the structure of the
proof is hard to see in apply style. But with this you can at least see
the incremental instantiation of the introduced meta-variables.
best,
lucas
D Mulligan wrote:
Last updated: May 03 2024 at 08:18 UTC