Wolfgang Jeltsch (Oct 11 2023 at 23:23): Wolfgang Jeltsch (Oct 11 2023 at 23:23):There is an equation Let_def, but it’s not part of the default simpset. Instead, there is a seemingly complicated simproc let_simp that seems to invoke Let_def in certain situations but not in others. Why is this?
Interestingly, there seem to be situations, partly quite simple ones actually, where the let_simp simproc fails but adding Let_def as a rewrite rule succeeds. @Javier Diaz and I have experienced one such situation in our code, and the AFP seems to contain more (there are multiple instances of simp add: Let_def there). What are the potential problems with adding Let_def as a rewrite rule? When is it safe and when not?
Mathias Fleury (Oct 12 2023 at 05:03):The size of the term can explode
Mathias Fleury (Oct 12 2023 at 05:04):I have rarely seen that as a problem though
Mathias Fleury (Oct 12 2023 at 05:07):Think of
A = (
let x = (if a then f y else g y) in
let y = x * x + x in
2*y * y)
becoming
(a ⟶ A = (2 * (f y * f y) + 2 * f y) * (f y * f y + f y)) ∧
(¬ a ⟶ A = (2 * (g y * g y) + 2 * g y) * (g y * g y + g y))
if x and y are meaningfull names, they are much better
Wolfgang Jeltsch (Oct 12 2023 at 11:46):That makes sense.
I understand that let_simp applies Let_def if the variable bound by the let occurs at most one time, but what does it do when there are multiple occurrences? It apparently does something, but I don’t know what.
Last updated: May 02 2024 at 08:19 UTC