Email Gateway (Aug 22 2022 at 09:44): Email Gateway (Aug 22 2022 at 09:44):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I have a lemma that states that
f ∈ Θ(g) ⟹ L(f) = L(g)
I also have the following two rules on Θ:
f ∈ Θ(g)
f1 ∈ Θ(g1) ⟹ f2 ∈ Θ(g2) ⟹ (λx. f1 x * f2 x) ∈ Θ(λx. g1 x * g2 x)
These rules together basically allow me to rewrite expressions of the
form "L(λx. … * f x * …)" to "L(λx. … * g x * …)" if I can show "f ∈
Θ(g)", i.e. I can rewrite factors under a "L" individually and
independently.
I would like to get the simplifier to do this automatically, i.e.
whenever there is an expression of the form "L(λx. f1 x * … * fk x)",
try to rewrite every factor individually by using the simp rules to find
an "fi" distinct from "gi" such that "fi ∈ Θ(gi)" and then rewriting the
factor "fi" to "gi".
For example, if I have a simp rule that states "(λ_. c) ∈ Θ(λx. 1)", and
I have an expression like "L(λx. x * 2 * x)", that should be rewritten
to "L(λx. x * 1 * x)".
I could easily write a simproc that does that, but I wonder if this can
also be done in a more straightforward and scalable way, e.g. with
simp/cong rules.
Cheers,
Manuel
Last updated: Nov 21 2024 at 12:39 UTC