Coq tactic for record equality?

7
votes

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

1
coqcoq-tactic
@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. – Anton Trunov
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! – Zimm i48
@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. – Anton Trunov
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. – Zimm i48
@Zimm i48 All right! – Anton Trunov

1 Answers

4
votes

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.