The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

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
>