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

[Jeremy Dawson]

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

[Laurent Thery]

Post by Jeremy Dawson
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

[Tej Chajed]

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)
*)

Post by Jeremy Dawson
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

[Dominique Larchey-Wendling]

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

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

Post by Jeremy Dawson
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

[Jason -Zhong Sheng- Hu]

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-***@loria.fr>
Date: 11/13/18 09:07 (GMT-05:00)
To: coq-***@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

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

Post by Jeremy Dawson
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