Mistral Contrastin (Apr 12 2021 at 11:33): Mistral Contrastin (Apr 12 2021 at 11:33):I have a function definition that is not recursive, but takes about five minutes to be processed (lose its purple background) on a relatively beefy machine. I already tried factoring it at the Plus Plus case. This is enough for the definition to be processed immediately, but I'd like to understand why Isabelle struggles with it so much and how in general I'd go about seeing where time is being spent. After five minutes, it also reports redundant equations and it is not clear to me why these are redundant.
Definitions:
datatype aexp = N int | V string | Plus aexp aexp
fun plus_full :: "aexp ⇒ aexp ⇒ aexp" where
"plus_full (N a) (N b) = N (a + b)" |
"plus_full (Plus p (N a)) (N b) = Plus p (N (a + b))" |
"plus_full (N b) (Plus p (N a)) = Plus p (N (a + b))" |
"plus_full (Plus p (N a)) (Plus q (N b)) = Plus (Plus p q) (N (a + b))" |
"plus_full (Plus p (N a)) (Plus (N b) q) = Plus (Plus p q) (N (a + b))" |
"plus_full (Plus (N a) p) (Plus (N b) q) = Plus (Plus p q) (N (a + b))" |
"plus_full (Plus (N a) p) (Plus q (N b)) = Plus (Plus p q) (N (a + b))" |
"plus_full (Plus p (N a)) q = Plus (Plus p q) (N a)" |
"plus_full q (Plus p (N a)) = Plus (Plus p q) (N a)" |
"plus_full p (N i) = (if i = 0 then p else Plus p (N i))" |
"plus_full (N i) p = (if i = 0 then p else Plus p (N i))" |
"plus_full p q = (Plus p q)"
Redundant equations after five minutes:
Ignoring duplicate rewrite rule:
plus_full (Plus (V ?vc1) (V ?vd1)) (Plus ?v1 (V ?vb1)) ≡
Plus (Plus (V ?vc1) (V ?vd1)) (Plus ?v1 (V ?vb1))
Ignoring duplicate rewrite rule:
plus_full (Plus (Plus ?vc1 ?ve1) (V ?vd1)) (Plus ?v1 (V ?vb1)) ≡
Plus (Plus (Plus ?vc1 ?ve1) (V ?vd1)) (Plus ?v1 (V ?vb1))
Ignoring duplicate rewrite rule:
plus_full (Plus (V ?vc1) (Plus ?vd1 ?ve1)) (Plus ?v1 (V ?vb1)) ≡
Plus (Plus (V ?vc1) (Plus ?vd1 ?ve1)) (Plus ?v1 (V ?vb1))
Ignoring duplicate rewrite rule:
plus_full (Plus (Plus ?vc1 ?vf1) (Plus ?vd1 ?ve1)) (Plus ?v1 (V ?vb1)) ≡
Plus (Plus (Plus ?vc1 ?vf1) (Plus ?vd1 ?ve1)) (Plus ?v1 (V ?vb1))
Ignoring duplicate rewrite rule:
plus_full (Plus ?v1 (V ?vd1)) (Plus (V ?va1) (V ?vb1)) ≡
Plus (Plus ?v1 (V ?vd1)) (Plus (V ?va1) (V ?vb1))
Ignoring duplicate rewrite rule:
plus_full (Plus ?v1 (Plus ?vd1 ?ve1)) (Plus (V ?va1) (V ?vb1)) ≡
Plus (Plus ?v1 (Plus ?vd1 ?ve1)) (Plus (V ?va1) (V ?vb1))
Thanks in advance for the help!
Mathias Fleury (Apr 12 2021 at 12:35):Internally the function packages deduplicates patterns (like plus_full (N i) p and plus p q are duplicates) to generate the right definitions and simplification rules.
Mathias Fleury (Apr 12 2021 at 12:37):The easiest solution in your case is to do the case distinction using case ... of .. \<Rightarrow> ...
Mistral Contrastin (Apr 12 2021 at 12:41):@Mathias Fleury aha, thanks! That explains the redundant equations and it makes sense. It is unfortunate that the definition of the function package leaks its implementation in that way. I might go as far as to say that it is a bug.
Is that also somehow related to the definition taking a long time to be processed?
Mathias Fleury (Apr 12 2021 at 12:46):You really need to do the disambiguation of the patterns, so not really a bug. Imagine that you would not do that and simply take the rules as simp rules. Then you could define the following:
fun f where
"f 0 = 0"
"f _ = 1"
Without further work on the equations, both can be applied to f n but you get different results depending on which equation you use, which is obviously wrong.
Mathias Fleury (Apr 12 2021 at 12:47):Anyway the disambiguation is the reason why the definitions takes such a long time.
Mistral Contrastin (Apr 12 2021 at 12:59):I guess I have the wrong mindset. I figured the second equation on f would implicitly be on Suc n due to the existence of the first equation. I guess such fall through reasoning is not appropriate in Isabelle? Is that right? If that's the case, I'd have expected your definition of f to be rejected due to patterns not being orthogonal.
Mathias Fleury (Apr 12 2021 at 13:01):Yeah indeed the second pattern becomes Suc:
fun f :: ‹nat ⇒ nat› where
"f 0 = 0" |
"f _ = 1"
thm f.simps
(* f 0 = 0
f (Suc ?v) = 1*)
My point is that this transformation from f _ = 1 to f (Suc _) = 1 becomes slow if you have too many patterns
Mathias Fleury (Apr 12 2021 at 13:03):(but it will eventually succeed as your large example illustrates)
Mistral Contrastin (Apr 12 2021 at 13:05):Perfect, I think I understand now. Thanks a lot for your explanations!
Lukas Stevens (Apr 12 2021 at 17:33):Maybe at some point there will be someone who is motivated enough to investigate whether the disambiguation can be sped up :)
Manuel Eberl (Apr 13 2021 at 10:20):If I recall correctly, if you use function instead of fun, you can have overlapping patterns and will be required to prove that whenever you have an overlap, you have the same result on the right-hand side. Unfortunately, you will be unable to do so when recursion is involved, so it is not too helpful in practice.
Last updated: Apr 18 2024 at 20:16 UTC