Email Gateway (Aug 18 2022 at 11:58): Email Gateway (Aug 18 2022 at 11:58):From: Sven Schneider <svens@cs.tu-berlin.de>
Hi,
is there a simple way to proof the following statement?
I have a proof but it contains a case-disinction over all elements in
the datatype. This is inacceptable for the actual dataype which contains
several thousands of elements; the proof would require to much time.
theory Test imports Main begin
datatype A = A0 | A1
datatype Label = B0 A A
instance Label :: "finite"
oops
end
Regards,
Sven
Email Gateway (Aug 18 2022 at 11:58):From: Tobias Nipkow <nipkow@in.tum.de>
I don't think there is an easy way. If your datatype as more than 100
constructors, you will anyway find that it can take a very long time to
even define such a datatype, never mind any proofs based on it. If the
large number of elements comes from the fact that there is a hierarchy
of datatypes, like above, you should be able to prove finiteness in
layers, and each layer should stay manageable.
Since this is in essence a finite problem, Tjark Weber's SAT-solver link
may be able to prove this automatically. Tjark?
Tobias
Email Gateway (Aug 18 2022 at 12:03):From: Tjark Weber <tjark.weber@gmx.de>
Sven,
I am afraid the SAT solver link currently works for (instances of)
propositional tautologies only. (However, link-ups with other automated
provers for more powerful logics are available as well. See, e.g.,
metis and sledgehammer.) I suspect that in your case the performance
issue shows up before the proof goal is purely propositional.
If you want to send me your proof though, I'll be happy to look at it in
more detail.
Best,
Tjark
Last updated: May 03 2024 at 08:18 UTC