spaceloop (May 18 2021 at 14:04): spaceloop (May 18 2021 at 14:04):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?
Emilio Jesús Gallego Arias (May 18 2021 at 14:18):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.
Ana de Almeida Borges (May 18 2021 at 14:20):You can use set x := (x in f x _) and set y := (y in f _ y) to abstract things away
Ana de Almeida Borges (May 18 2021 at 14:23):(this is also an ssr thing, you would need Require Import ssreflect for it to work)
spaceloop (May 19 2021 at 09:22):Thanks :)
Last updated: Oct 13 2024 at 01:02 UTC