Email Gateway (Aug 19 2022 at 10:23): Email Gateway (Aug 19 2022 at 10:23):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
In trying to understand a bit the theory "Equiv_Relations.thy" I started to
prove
some (apparently) simple lemmas.
So I defined some equivalence relations on natural numbers using the
remainder operator and proved
some lemmas relating equivalence relations with its equivalence classes
(partitions).
An unexpected problem occurs in the (experimental, exploratory) proof of
lemma partition_EqR05 (the
last lemma in the theory file).
The proof goes through in Isabelle 2012, but after "apply (auto)"
Isabelle2013-RC2
enters in a loop after a failure in the linear arithmetic proof procedure
(apparently).
Images showing two (normal) snapshots in Isabelle 2012 and the above
mentioned
crash in Isabelle2013-RC2 are included together with the correspondent
theory file.
Any help on this would be greatly appreciated.
Best!
isa2012-equiv-auto-ok.PNG
isa2012-equiv-auto-finished.PNG
isa2013-RC2--equiv-auto-loop.PNG
equiv_error.thy
Email Gateway (Aug 19 2022 at 10:30):From: Makarius <makarius@sketis.net>
The only difference I can see between Isabelle2012 and Isabelle2013-RC2 is
that in Isabelle2012 you need to tick "Tracing" in the Output panel to see
the very same "linarith_split_limit exceeded (current value is 9)". In
both versions the proofs works, but takes very long.
Someone else who understands the "lin_arith" solver needs to explain how
to switch it off, or how to do these proofs about "mod" in a better way.
Makarius
Email Gateway (Aug 19 2022 at 10:30):From: Tjark Weber <webertj@in.tum.de>
The limit exists because repeated splitting leads to an exponential
blow-up of the goal. It can be set, e.g., via
using [[linarith_split_limit=n]]
For this particular proof, n=12 gets rid of the warnings, and also of a
few more subgoals.
Best regards,
Tjark
Email Gateway (Aug 19 2022 at 10:30):From: Alfio Martini <alfio.martini@acm.org>
Thanks Tjark! With n = 12 there´s no need to use (arith)+ after the
existential proofs.
Best!
Last updated: Apr 24 2024 at 20:16 UTC