7

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

Zimm i48
  • 2,901
  • 17
  • 26
Ashley Yakeley
  • 664
  • 4
  • 11
  • @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 Oct 18 '16 at 09:28
  • 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 Oct 18 '16 at 09:31
  • @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 Oct 18 '16 at 09:46
  • I do not think you need to name it `coq-ltac`. `ltac` alone seems perfectly fine. If you [search for ltac on SO](http://stackoverflow.com/search?q=ltac) you only get Coq related questions. – Zimm i48 Oct 18 '16 at 09:52
  • @Zimm i48 All right! – Anton Trunov Oct 18 '16 at 09:57

1 Answers1

4

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.

Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
  • 1
    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. – Suzanne Soy May 02 '19 at 07:49