The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 11/13/18 4:22 AM, Jeremy Dawson wrote:
> 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)

Now there is no. You did the right thing proving the lemma by unfolding.
Note that often you do not need such theorem as the Coq engine directly
knows about this unfolding.

If I set this definition

Definition four := 2 + 2.

and the goal

Goal four = 2 + 2.

I can directly prove it by reflexivity.

Check refl_equal.
apply refl_equal.
Qed.

Note that this can get more powerful as even some
computation may be involved.

Goal four = 0 + 4.
Check refl_equal.
apply refl_equal.
Qed.

For more detail you can read:

https://coq.inria.fr/refman/language/cic.html?highlight=convertibility#conversion-rules

--
Laurent