Email Gateway (Aug 18 2022 at 13:02): Email Gateway (Aug 18 2022 at 13:02):From: Chris Capel <pdf23ds@gmail.com>
datatype dt = A nat | B dt list;
lemma "EX (x :: dt). P x"
Assuming that producing an existential witness is out of the question
in the actual circumstance, how do I prove this? I.e., how do I apply
cases or induct on it? I'm thinking that the way would be to transform
it into something like
"EX x. (case x of A n => P' n | _ => False) | (case x of B n => P'' n
| _ => False)"
But I don't know how to accomplish this. (BTW, is there a more
succinct way to express that term?)
Upon further thought, it seems that actually the best way is to just
pick some good term to substitute for x, and then simplify. However,
I've encountered a problem with this as well. I have a lemma "!!z. EX
x. P x", and I need my substitution for "x" to depend on "z" to make
sense.
However, applying rule exI[of _ "Q z"] doesn't work--"z" can't be
captured this way; it's renamed to "za". Do I actually need to change
my lemma to read "!!z EX (x z). P (x z)"? That's kind of painful.
Chris Capel
Email Gateway (Aug 18 2022 at 13:03):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting Chris Capel <pdf23ds@gmail.com>:
However, applying rule exI[of _ "Q z"] doesn't work--"z" can't be
captured this way; it's renamed to "za".
Using the "of" attribute only works in this way if "z" is a free
variable. In your case, it appears that "z" is bound by a
meta-universal quantifier within your proof subgoal; there is no way
to refer to such variables using the "of" or "where" attributes.
You have two alternatives:
Use Isar-style declarative proofs. When proving this subgoal, you
can "fix z", after which "z" can be referred to as a free variable.
Stay with apply-style proofs, but use "rule_tac". The "_tac"
variations of tactics can refer to meta-universal-bound variables
within your subgoal. For example, try
apply (rule_tac x="Q z" in exI)
Hope this helps,
Email Gateway (Aug 18 2022 at 13:03):From: Tobias Nipkow <nipkow@in.tum.de>
datatype dt = A nat | B dt list;
lemma "EX (x :: dt). P x"Assuming that producing an existential witness is out of the question
in the actual circumstance, how do I prove this? I.e., how do I apply
cases or induct on it? I'm thinking that the way would be to transform
it into something like"EX x. (case x of A n => P' n | _ => False) | (case x of B n => P'' n
| _ => False)"
Why not just "case x of A n => P' n | B n => P'' n"?
But I don't know how to accomplish this. (BTW, is there a more
succinct way to express that term?)
If you want to rewrite "EX (x :: dt). P x" into some other form, you can
do it explicitly by stating the subgoal "(EX (x :: dt). P x) = ...",
which you prove in the usual way (you may need extensionality here, rule
"ext").
Tobias
Email Gateway (Aug 18 2022 at 13:03):From: Chris Capel <pdf23ds@gmail.com>
On Mon, Feb 23, 2009 at 08:30, Brian Huffman <brianh@cs.pdx.edu> wrote:
You have two alternatives:
- Use Isar-style declarative proofs. When proving this subgoal, you can
"fix z", after which "z" can be referred to as a free variable.
This is helpful. But apply scripts are so much easier to do than Isar
when you don't know either well!
- Stay with apply-style proofs, but use "rule_tac". The "_tac" variations
of tactics can refer to meta-universal-bound variables within your
subgoal. For example, tryapply (rule_tac x="Q z" in exI)
And this is exactly what I was looking for. I'm curious--why the
difference in behavior? The documentation seems cryptic on this point.
I hadn't been aware of the difference between this and (rule_tac
exI[of _ "Q z"]).
On Mon, Feb 23, 2009 at 14:56, Tobias Nipkow <nipkow@in.tum.de> wrote:
If you want to rewrite "EX (x :: dt). P x" into some other form, you can
do it explicitly by stating the subgoal "(EX (x :: dt). P x) = ...",
which you prove in the usual way (you may need extensionality here, rule
"ext").
Ah, yes. I think I accomplished what you speak of here using
subgoal_tac followed by assumption, without needing extensionality.
This disadvantage from rule_tac being that I have to state my entire Q
again, which is quite large. However, with Isar I can use the "is"
keyword and it's not a problem.
Thank you all,
Chris Capel
Last updated: May 03 2024 at 12:27 UTC