Email Gateway (Aug 18 2022 at 14:34): Email Gateway (Aug 18 2022 at 14:34):From: munddr@googlemail.com
Hi,
I have the following and somehow 'auto' spends a lot of time and not
doesn't terminate:
consts
f :: "real => real"
g :: "real => real"
S :: "real set"
types S = "real set"
axioms
a1: "EX Z < S. ALL x : Z. fx ~= g x"
lemma lem: "EX Z < S. EX x : Z. fx ~= g x"
using a1
apply auto
For some reason, auto doesn't terminate. Shouldn't the lemma be
straightforward to prove given a1?
Thanks
John
Email Gateway (Aug 18 2022 at 14:34):From: Tobias Nipkow <nipkow@in.tum.de>
I'm afraid your formulae are not well-formed. Never mind the "fx", but
"EX Z < S. ALL x : Z" doesnt make sense. Pls send an actual theory that
Isabelle is prepared to accept.
Tobias
munddr@googlemail.com wrote:
Email Gateway (Aug 18 2022 at 14:35):From: Stephan Merz <Stephan.Merz@loria.fr>
For your lemma to be true, ax1 should assert that the set Z is non-empty.
Stephan
Email Gateway (Aug 18 2022 at 14:35):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Possibly because your lemma doesn't follow?
Firstly, don't use axiom unless you really know what you're doing, try
use normal lemmas instead. Also, try simplify them to see where isabelle
gets stuck. If we take this simpler lemma and try to prove it with
simple proof steps:
lemma "∃Z⊂S. ∀x∈Z. P x ⟹ ∃Z⊂S. ∃x∈Z. P x"
apply (erule exE)
apply (rule_tac x=Z in exI)
apply (rule conjI, simp)
apply (elim conjE)
we get to this state: ⋀Z. ⟦Z ⊂ S; ∀x∈Z. P x⟧ ⟹ ∃x∈Z. P x
The only thing we can apply now is ballE or ballI, which asks that we
prove the statement for some x in the set Z. Since we don't know whether
Z is empty or not... well, there might not be any x existing in Z at
all. Using auto can't make it so. Simplify it further and you get:
lemma "∀x∈Z. P x ⟹ ∃x∈Z. P x"
apply (case_tac "Z = {}")
apply simp
which asks you to prove "False".
You might want to investigate the Isabelle tutorial for simpler proof
methods than just blasting things with metis and auto. While powerful,
automation in higher-order logic is hard and will require hand-holding
eventually, like in this case.
Also, I highly recommend switching to unicode tokens / xsymbols, I don't
think anyone uses the ASCII syntax much anymore, doesn't look very pretty.
Sincerely,
Rafal Kolanski.
munddr@googlemail.com wrote:
Last updated: Apr 25 2024 at 20:15 UTC