CODEWITHSUNDEEP
coqcoq-tactic
Ashley Yakeley
Ashley Yakeley

Reputation: 691

Coq tactic for record equality?

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

Upvotes: 7

Views: 1123

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23622

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.

Upvotes: 4

Related Questions