The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

Coq doesn’t create such an equality for you. As Laurent explained, the theorem is just reflexivity and in many situations Coq will do the conversion for you.
There are some situations where such equalities are nonetheless useful, for controlled unfolding in combination with marking things opaque or in rewriting hint databases; here’s a way to produce roughly the statement you want automatically, wrapped up nicely in a tactic-in-term inside a notation (this trick is broadly useful when you want to write “functions” in Ltac):

Local Tactic Notation "unfolded_eq" constr(pf) :=
  let x := (eval red in pf) in
  exact (eq_refl : (pf = x)).

Notation unfolded_eq pf := ltac:(unfolded_eq pf) (only parsing).

Definition foo x y z := x + y + z.
Definition foo_eq := unfolded_eq foo.
Check foo_eq.
(*
foo_eq
     : foo = (fun x y z : nat => x + y + z)
*)

On Tue, Nov 13, 2018 at 2:17 AM Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

Hi coq-club,

Having made a definition f x y z = a b c
how do I get this as an equality theorem that can be used to rewrite
  a b c to f x y z?

(I realise I can set it out as a lemma and prove it using unfold, but
I'm assuming it's already there as a theorem that I just need to find
out how to get hold of it)

thanks

Jeremy