Hanno Becker (Jul 19 2023 at 05:22): Hanno Becker (Jul 19 2023 at 05:22):Hi! I've got a large(ish) datatype Foo = A0 | A1 | ... | A49 and a foo_to_word :: Foo => 64 word defined case-by-case. Now I'd like to note that inj foo_to_word, which should be trivial, but somehow proof by case distinction takes considerably time (>20s). Why is that? Yes, there are 2500 cases, but each of them should -- so I thought -- be discharged instantly.
This fits into the more general note that large datatypes such as the one above seem to be quite slow in Isabelle.
Any hints/tricks how to keep complexity down here?
MWE:
datatype Foo =
A00 | A01 | A02 | A03 | A04 | A05 | A06 | A07 | A08 | A09 |
A10 | A11 | A12 | A13 | A14 | A15 | A16 | A17 | A18 | A19 |
A20 | A21 | A22 | A23 | A24 | A25 | A26 | A27 | A28 | A29 |
A30 | A31 | A32 | A33 | A34 | A35 | A36 | A37 | A38 | A39 |
A40 | A41 | A42 | A43 | A44 | A45 | A46 | A47 | A48 | A49
definition foo_to_nat :: ‹Foo ⇒ nat› where
‹foo_to_nat x ≡ case x of
A00 ⇒ 00 | A01 ⇒ 01 | A02 ⇒ 02 | A03 ⇒ 03 | A04 ⇒ 04 | A05 ⇒ 05 | A06 ⇒ 06 | A07 ⇒ 07 | A08 ⇒ 08 | A09 ⇒ 09 |
A10 ⇒ 10 | A11 ⇒ 11 | A12 ⇒ 12 | A13 ⇒ 13 | A14 ⇒ 14 | A15 ⇒ 15 | A16 ⇒ 16 | A17 ⇒ 17 | A18 ⇒ 18 | A19 ⇒ 19 |
A20 ⇒ 20 | A21 ⇒ 21 | A22 ⇒ 22 | A23 ⇒ 23 | A24 ⇒ 24 | A25 ⇒ 25 | A26 ⇒ 26 | A27 ⇒ 27 | A28 ⇒ 28 | A29 ⇒ 29 |
A30 ⇒ 30 | A31 ⇒ 31 | A32 ⇒ 32 | A33 ⇒ 33 | A34 ⇒ 34 | A35 ⇒ 35 | A36 ⇒ 36 | A37 ⇒ 37 | A38 ⇒ 38 | A39 ⇒ 39 |
A40 ⇒ 40 | A41 ⇒ 41 | A42 ⇒ 42 | A43 ⇒ 43 | A44 ⇒ 44 | A45 ⇒ 45 | A46 ⇒ 46 | A47 ⇒ 47 | A48 ⇒ 48 | A49 ⇒ 49›
lemma foo_to_nat_inj:
shows ‹inj foo_to_nat›
by (auto simp add: inj_def foo_to_nat_def split: Foo.splits) (* SLOW *)
Maybe you can selectively enable only those datatype plugins that you really need to make it faster.
Relevant thread:
https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Datatype.20definition.20can.20be.20slow
Relevant document:
https://isabelle.in.tum.de/dist/doc/datatypes.pdf#section.8
Sorry I misread: I thought it is about the datatype definition, not the following lemma...
Mathias Fleury (Jul 19 2023 at 06:49):It is not too bad with
by (auto simp only: semiring_char_0_class.eq_numeral_simps inj_def simp_thms nat.distinct verit_eq_simplify
old.nat.distinct One_nat_def foo_to_nat_def Suc_eq_numeral pred_numeral_simps split: Foo.splits)
(this is around 10 times faster on my machine than your solution)
Hanno Becker (Jul 19 2023 at 07:15):How did you come up with that, @Mathias Fleury ?
Mathias Fleury (Jul 19 2023 at 10:36):I started with
apply (simp only: inj_def foo_to_nat_def split: Foo.splits)
Then I checked what the simplifier needed to continue the proof. Usually with:
lemma "0 = (35::nat)"
supply [[simp_trace]]
apply simp
sorry
At some point, I got to:
apply (simp only: semiring_char_0_class.eq_numeral_simps inj_def simp_thms nat.distinct verit_eq_simplify
old.nat.distinct One_nat_def foo_to_nat_def Suc_eq_numeral pred_numeral_simps split: Foo.splits)
which was not working (because of some missing simplification under forall), but auto worked…
Hanno Becker (Jul 19 2023 at 10:38):Thanks, very illustrative!
Last updated: Apr 27 2024 at 20:14 UTC