Dear all,

The `unfold`

tactic only accepts an identifier as input, it does not accept a term, in contrast with the `fold`

tactic. Is there nonetheless a way to unfold the instances of an identifier only when it is applied to a specific value?

A way to do it is of course to unfold all instances, and then fold the ones applied to the other values, but this requires to know the set of possible values.

Some sirens whispered in my ear that it’s out of the box in ssreflect, but this is not an option for me at the moment.

So, would there be a way that I’m unaware of, or a dirty ltac trick, by any chance?

Here is a self-contained, simplified example illustrating the problem:

```
Require Import Program.Basics.
Class Op (A: Type): Type := op: A -> A -> A.
Instance Op_nat: Op nat := plus.
Instance Op_fun {A: Type}: Op (A -> A) := compose.
Goal forall n, op (fun (x:nat) => op x x) (fun (x:nat) => x) n = op (fun (x:nat) => x) (fun (x: nat) => op x x) n.
intros n.
(* Here, I'd like to unfold the occurences of op from the Op_nat instance, but not the others *)
(* However, the following is not supported *)
(* unfold (@op _ Op_nat).*)
(* I _can_ do: *)
unfold op; fold (@op (nat -> nat) Op_fun).
(* But it's quite clearly impractical in general since it requires to know all possible values to which op may be applied, as opposed to exactly the one I want to unfold *)
```

Thanks in advance for any suggestion.

Best,

Yannick

Hi Yannick,

If you use the “rewrite” tactic from SSReflect (part of the Coq standard library since Coq version 8.7; see its documentation) you can write:

```
rewrite [@op nat]/op.
```

What is written in square brackets before the rewriting item — here unfold (“/”) the constant “op” — is the pattern that describes the subterm(s) where to perform the rewrite.

If there are strong reasons not to use SSReflect (probably there aren’t and you should use it!), you can write an `unfold_term`

tactic in Ltac. Here’s a basic attempt:

```
Ltac get_head t :=
match constr:(t) with
| ?a ?b => get_head a
| ?a => a
end.
Ltac unfold_term t :=
let o := get_head t in
pattern t;
match goal with [ |- ?a ?b] =>
let b := (eval unfold o in b) in change (a b) end;
hnf.
```

Then `unfold_term (@op nat)`

does what you want in your example.

You can run the tactics one after the other to see their effect.

Hi Vincent, Yannick,

The reason I had dismissed using SSReflect is that I’m working in an already developed library of non-trivial size, and had the naïve understanding that opting for SSReflect’s `rewrite`

was likely to be a pervasive change.

But I might be wrong, and may be able to wrap its use purely locally into an ltac?

In the mean time thanks a lot for the `ltac`

hack. I need to stare into it a little bit to understand how it works, but seems to perfectly do the trick!

Edit: Oh got it, that’s nice.

FWIW, after loading ssreflect, `rewrite -> H`

still invokes the standard rewrite — and that’s the most significant change you might have to do (simplest hack: just search-n-replace `rewrite`

with `rewrite ->`

, and fix any errors due to `rewrite -> <-`

; fancier regexps might do better). Also, many standard uses of `rewrite`

will keep working.