Unfolding a definition without reduction

Question

The Coq manual states that the unfold qualid tactic unfolds each occurrence of qualid in the goal and replaces it with its beta-iota-normal form.

Is there a simple way to unfold a definition without triggering beta/iota reduction?

Answer 1

You might want to try e.g. the cbv tactic like so:

Definition foo := (fun (x : nat) => x) 42.
Definition bar := (fun (x : nat) => x) 42.

Goal foo = bar.
  cbv delta [foo].

This results in the following proof state:

(fun x : nat => x) 42 = bar