Email Gateway (Aug 18 2022 at 17:56): Email Gateway (Aug 18 2022 at 17:56):From: Christian Kühnel <christian.kuehnel@gmail.com>
Dear isabelle users,
I'm trying to prove this obvious lemma:
"~ (EX t. [1::nat,1,1] ! t = 0 )"
I've been trying for a while but could not figure it out. Can you please
give me a hint, how I can prove this?
Is there more documatation on prooving terms with existential and universal
quantifiers? The isabelle tutorial did not help me there.
>
Best regards,
Christian Kühnel
Email Gateway (Aug 18 2022 at 17:56):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Christian,
your lemma is not provable, because t is not constrained to the length of the
list. It could be, say, 42, and you can hardly prove anything about what you get
if you take an element beyond the list.
Here's the provable version:
"~ (EX t. t < 3 & [1::nat,1,1] ! t = 0 )"
If you apply the simplifier to this goal, it will pull the negation in, turning
the existential quantifier into a universal one, so this is no longer a problem
of existential quantifiers. You can prove the statement in by trying every
possible value -- which is feasible for such small lists, but impractical for
larger ones. If you want to split the cases for t automatically, feed nth_Cons'
to the simplifier:
by(simp add: nth_Cons')
Hope this helps,
Andreas
Email Gateway (Aug 18 2022 at 17:56):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi,
the nth function on lists (xs ! n) is undefined when n is outside the
bounds of xs. That means that we do not know anything about the result.
Since we do not know anything, we do in particular not know whether the
result is 0 or not. Thus your statement is not provable.
I hope this helps.
cheers
chris
Last updated: Apr 26 2024 at 12:28 UTC