Unfolding identifiers applied to specific values only

Using Coq
1

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

2

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.

3

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.

4

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.

5

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.