Stream: Coq users

Topic: Unfolding small part of an expression


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip spaceloop (May 19 2021 at 09:22):

Thanks :)


Last updated: Jan 28 2023 at 06:30 UTC