I have a term
x := f <t1> <t2> where t1 and t2 are big sub expressions. I'd like to partially unfold x in my goal, e.g. changing it to
f x y and add the equalities
x = <t1> and
y = <t2> to my hypotheses (or some other way to not unfold all sub expressions). What is the appropriate tactic to use here?
I usually use SSreflect's
rewrite [pat]/foo unfold syntax, or directly define unfolding helper lemmas following the locked pattern. This works very well for me [but requires coding discipline], I'm sure there are other options too.
You can use
set x := (x in f x _) and
set y := (y in f _ y) to abstract things away
(this is also an ssr thing, you would need
Require Import ssreflect for it to work)
Last updated: Oct 05 2023 at 02:01 UTC