Email Gateway (Aug 17 2022 at 14:15): Email Gateway (Aug 17 2022 at 14:15):From: Tom Ridge <Thomas.Ridge@cl.cam.ac.uk>
Should I expect the following to be solved by arith? Or presburger? Or
some other procedure? Or does the presence of the "f" go beyond what
these procedures can handle? Is there an extension to presburger that
can handle problems of this form?
lemma "
! (x::num) y z (f::num=>num).
(x < y) & (f x < f y) & (!x::num. z <= x --> (f x = f z)) --> x < z
"
apply(intro allI impI, elim conjE)
apply(rule ccontr)
apply(frule_tac x=x in spec)
apply(drule_tac x=y in spec)
apply(simp)
done
Thanks
Tom
Email Gateway (Aug 17 2022 at 14:15):From: nipkow@in.tum.de
! (x::num) y z (f::num=>num).
(x < y) & (f x < f y) & (!x::num. z <= x --> (f x = f z)) --> x < z
num = nat/int/real? In either case, this is beyond arith (and arith tries
Presburger) and not in any of the standard classes of decidable theories.
The f is indeed the problem. Clearly a more heuristic approach is needed here.
Tobias
Email Gateway (Aug 17 2022 at 14:16):From: Amine Chaieb <chaieb@informatik.tu-muenchen.de>
Tom,
There are several reasons why arith fails to solve your goal.
1) Unfortunately presbugre works only over int (and nat). You use num?.
2) The abstraction over unknown terms works only if those are variables,
and are not applied to bound variables. Both do not apply to your goal.
The f you use in the goal, is not "uninterpreted" since it has to satisfy
the second conjuct. Here even qfree Preburger + uninterpreted functions
would'nt help. I don'nt know of other decidable theories for this kind of
goals.
Do you need arithmetic at all? the proof seems to only rely on ordering
(may be sth is hidden in num).
Regards,
Amine.
Last updated: May 03 2024 at 12:27 UTC