The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

As a slight improvement, making a function opaque is probably too much. You can tell Coq to not handle fact only in certain reduction cases:

Arguments fact n : simpl never.

Thanks,

Jason Hu

-------- Original message --------

From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>

Date: 11/13/18 09:07 (GMT-05:00)

To: coq-club AT inria.fr

Subject: Re: [Coq-Club] getting a definition as an equality theorem

Hi Jeremy,

This is a very common situation where the "simpl" tactic
unfolds to much or is difficult to control. The easy
(but verbose) way is to generate equations and use rewrite.

Fixpoint fact n :=
  match n with
    | 0   => 1
    | S n => (S n) * fact n
  end.

Fact fact_0 : fact 0 = 1.
Proof. reflexivity. Qed.

Fact fact_S n : fact (S n) = (S n) * fact n.
Proof. reflexivity. Qed.

You can even make fact opaque after that

Opaque fact.

if you need to control the unfolding of the
fixpoint very precisely

That way if you want

fact (S (S (S n))))

to rewrite as

(S (S (S n))) * ( (S (S n)) * fact (S n) )

the tactic "do 2 rewrite fact_S" will do it.

Best regards,

Dominique

----------------------

Le 13/11/2018 à 04:22, Jeremy Dawson a écrit :
> 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
>