Moritz R (Mar 17 2025 at 12:06): Moritz R (Mar 17 2025 at 12:06):I have defined a Relation on symbols for a formalization in Theoretical computer science, but it takes on the order of half a 30 seconds and a 50 seconds on a decently speced macbook for Isabelle to accept the definition (hovering on the fun keyword gives these values, and they are indeed correct).
If i isolate the definitons it is alot faster (10 seconds and 20 seconds) but still not fast. Anything i can do?
Here's the isolated version:
datatype ('n,'t) sym = Nt 'n | Tm 't
type_synonym ('n,'t) syms = "('n,'t) sym list"
type_synonym ('n,'t) prod = "'n × ('n,'t) syms"
type_synonym ('n,'t) prods = "('n,'t) prod list"
type_synonym ('n,'t) Prods = "('n,'t) prod set"
datatype bracket = Op | Cl
datatype version = One | Two
text‹after each (Op,A→a,1) comes a (Cl,A→a,1) and after each (Op,A→a,2) comes a (Cl,A→a,2)›
fun P4 :: ‹(bracket × ('n,'t) prod × version) ⇒ (bracket × ('n,'t) prod × version) ⇒ bool› where
‹P4 (Op, ((A, [Tm a]), One)) (Cl, ((X, [Tm y]), One)) = (X = A ∧ y = a)› |
‹P4 (Op, ((A, [Tm a]), One)) in2 = False› |
‹P4 (Op, ((A, [Tm a]), Two)) (Cl, ((X, [Tm y]), Two)) = (X = A ∧ y = a)› |
‹P4 (Op, ((A, [Tm a]), Two)) in2 = False› |
‹P4 x y = True›
fun P4_sym :: ‹('n, bracket × ('n,'t) prod × version) sym ⇒ ('n, bracket × ('n,'t) prod × version) sym ⇒ bool› where
‹P4_sym (Tm (Op, ((A, [Tm a]), One))) (Tm (Cl, ((X, [Tm y]), One))) = (X = A ∧ y = a)› |
‹P4_sym (Tm (Op, ((A, [Tm a]), One))) in2 = False› |
‹P4_sym (Tm (Op, ((A, [Tm a]), Two))) (Tm (Cl, ((X, [Tm y]), Two))) = (X = A ∧ y = a)› |
‹P4_sym (Tm (Op, ((A, [Tm a]), Two))) in2 = False› |
‹P4_sym x y = True›
P4.simps has length 96 after disambiguation…
Moritz R (Mar 17 2025 at 12:12):yes, and im not sure i can do anything about the complex pattern :(
Mathias Fleury (Mar 17 2025 at 12:12):isn't this the same:
text‹after each (Op,A→a,1) comes a (Cl,A→a,1) and after each (Op,A→a,2) comes a (Cl,A→a,2)›
fun P4 :: ‹(bracket × ('n,'t) prod × version) ⇒ (bracket × ('n,'t) prod × version) ⇒ bool› where
‹P4 (Op, ((A, [Tm a]), s)) (Cl, ((X, [Tm y]), t)) = (s = t ∧ X = A ∧ y = a)› |
‹P4 (Op, ((A, [Tm a]), One)) in2 = False› |
‹P4 (Op, ((A, [Tm a]), Two)) in2 = False› |
‹P4 x y = True›
(that cuts the patterns in half)
Moritz R (Mar 17 2025 at 12:13):ah yes! Good catch!
Mathias Fleury (Mar 17 2025 at 12:14):and then this
text‹after each (Op,A→a,1) comes a (Cl,A→a,1) and after each (Op,A→a,2) comes a (Cl,A→a,2)›
fun P4 :: ‹(bracket × ('n,'t) prod × version) ⇒ (bracket × ('n,'t) prod × version) ⇒ bool› where
‹P4 (Op, ((A, [Tm a]), s)) (Cl, ((X, [Tm y]), t)) = (s = t ∧ X = A ∧ y = a)› |
‹P4 (Op, ((A, [Tm a]), _)) in2 = False› |
‹P4 x y = True›
(I am not touching the list, I assume you really need more then 1 element and not just some/none)
Moritz R (Mar 17 2025 at 12:17):sorry, what list do you mean?
Mathias Fleury (Mar 17 2025 at 12:18):[Tm a]
Moritz R (Mar 17 2025 at 12:19):Ah, yea that is the right side of a production, that needs to stay as a list
Moritz R (Mar 17 2025 at 12:19):Do you see any optimization potential for
text‹After each (Op,A→BC,1), always comes a (Op,(B, _),1), And after each (Op,A→BC,2), always comes a (Op,(C, _),1)›
fun P3 :: ‹(bracket × ('n,'t) prod × version) ⇒ (bracket × ('n,'t) prod × version) ⇒ bool› where
‹P3 (Op, ((A, [Nt B, Nt C]), One)) (Op, ((X,y), One)) = (X = B)› |
‹P3 (Op, ((A, [Nt B, Nt C]), One)) in2 = False› |
‹P3 (Op, ((A, [Nt B, Nt C]), Two)) (Op, ((X,y), One)) = (X = C)› |
‹P3 (Op, ((A, [Nt B, Nt C]), Two)) in2 = False› |
‹P3 x y = True›
aswell?
Mathias Fleury (Mar 17 2025 at 12:25):text‹After each (Op,A→BC,1), always comes a (Op,(B, _),1), And after each (Op,A→BC,2), always comes a (Op,(C, _),1)›
fun P3' :: ‹(bracket × ('n,'t) prod × version) ⇒ (bracket × ('n,'t) prod × version) ⇒ bool› where
‹P3' (Op, ((A, [Nt B, Nt C]), One)) (p, ((X,y), t)) = (p = Op ∧ t = One ∧ X = B)› |
‹P3' (Op, ((A, [Nt B, Nt C]), Two)) (p, ((X,y), t)) = (p = Op ∧ t = One ∧ X = C)› |
‹P3' x y = True›
But you could also go for case:
definition P3'' where
‹P3'' x y = (case (x, y) of
((Op, ((A, [Nt B, Nt C]), One)), (Op, ((X,y), t))) ⇒ (t = One ∧ X = B) |
((Op, ((A, [Nt B, Nt C]), One)), _) ⇒ False |
((Op, ((A, [Nt B, Nt C]), Two)), (Op, ((X,y), t))) ⇒ (t = One ∧X = C) |
((Op, ((A, [Nt B, Nt C]), Two)), in2) ⇒ False |
_ ⇒ True)›
and prove the few simp rules that will be useful for your case
Mathias Fleury (Mar 17 2025 at 12:27):lemma
‹P3'' (Op, ((A, [Nt B, Nt C]), One)) (Op, ((X,y), One)) = (X = B)›
‹P3'' (Op, ((A, [Nt B, Nt C]), Two)) (Op, ((X,y), One)) = (X = C)›
by (auto simp: P3''_def split: bracket.splits list.splits sym.splits)
Usually during proofs, you will only get the matching pattern, not the other weird ones anyway
Moritz R (Mar 17 2025 at 12:33):Considering i will also need to throw this on some concrete strings, the function way would probably be less manual work right?
Moritz R (Mar 17 2025 at 12:39):If i put some constants like you did with Op and turn them to variables that are checked on the right side of the equation, that reduces the pattern match count, but in turn might also make me do more case splitting in induction proofs right?
Mathias Fleury (Mar 17 2025 at 12:41):Yep
Mathias Fleury (Mar 17 2025 at 12:41):but you can also define your own induction principle that does not have duplicates
Mathias Fleury (Mar 17 2025 at 12:41):Although technically, you are only doing a case distinction, it is not really an induction…
Moritz R (Mar 17 2025 at 12:43):Mathias Fleury schrieb:
but you can also define your own induction principle that does not have duplicates
But then i would have to write out all the 100 cases again? I guess there is no free lunch
Mathias Fleury (Mar 17 2025 at 12:51):I am not sure that you need the 100 cases
Mathias Fleury (Mar 17 2025 at 12:52):Usually in proofs you only have the meaningful cases, as the others are deleted by assumptions
Moritz R (Mar 17 2025 at 13:10):Thank you, you have been very helpful!
All the functions are now under 1 second (i have multiple of them) and it has become manageable again.
Last updated: Apr 18 2025 at 20:21 UTC