Coq tactic for record equality?

Question

In Coq, when attempting to prove equality of records, is there a tactic that will decompose that into equality of all of its fields? For example,

Record R := {x:nat;y:nat}.

Variables a b c d : nat.

Lemma eqr : {|x:=a;y:=b|} = {|x:=c;y:=d|}.

Is there a tactic that will reduce this to a = c /\ b = d? Note that in general, any of a b c d might be big complicated proof terms (which I can then discharge with a proof irrelevance axiom).

Tenerife

@Zimm i48 The description for coq-tactic says: "Tactics are programs written in Ltac, the untyped language used in the Coq proof assistant to transform goals and terms." In my understanding this means questions about how to write tactics using Ltac, or questions on proof automation in general. But I admit the description is a bit ambiguous. – Ashok

All right, fell free to rollback and let's maybe improve the description? Maybe even change the tag name to ltac? It would be so much clearer! – Newby

@Zimm i48 I've looked at the full description and found out the following: "This tag should be used on questions related to the issues in using coq tactics to derive proofs using the Coq proof assistant." In this case I think your edit fits perfectly. I'm going to (1) edit the tag info to make its usage clearer; (2) create a new tag coq-ltac; (3) add coq-ltac to some posts to show its intended usage; (4) maybe we should go through all coq-tactic questions (there are 56 now) and make sure they are really about tactic-related issues. – Ashok

I do not think you need to name it coq-ltac. ltac alone seems perfectly fine. If you search for ltac on SO you only get Coq related questions. – Newby

@Zimm i48 All right! – Ashok

Answer 1

You can use the f_equal tactic, which will work not only for records, but also for arbitrary goals of the form f x1 .. xn = f y1 .. yn, where f is any function symbol, of which constructors are a particular case.

Shimmer

I mistakenly understood this as a series of tactics defined for every f, e.g. defining foo x y would implicitly define foo_equal, bar x y z would define bar_equal and so on. Note for others who get misled: that's not the case, there is a single f_equal tactic, the f is not metasyntactic in the tactic's name. – Per