Stream: Coq users

Topic: Simplifying or unfolding within a term

Patrick Nicodemus (Jan 16 2022 at 22:50):

Suppose I have a goal with subterm t. I want to simplify or unfold something, say the induction principle for a sum sum_ind only within t without affecting the rest of the goal. How can I do this?
The way I had set up was something like

let X := fresh "var" in
set (X := t) ; unfold sum_ind in X; unfold X

but this doesn't work when there are bound variables in t so that the subterm can't be extracted or generalized.

Karl Palmskog (Jan 16 2022 at 22:54):

if you want to simplify/rewrite in subterms, you may want to try SSReflect (can be used without MathComp). There was a whole paper on subterm selection...

Enrico Tassi (Jan 17 2022 at 08:50):

rewrite [in t]/sum_ind

should do it (once you require ssreflect)

Last updated: Sep 30 2023 at 06:01 UTC