Coq tactics to ensure equal equality?

Question

When trying to prove equality of records in Coq, is there a tactic that will decompose this into the equality of all its fields? For instance,

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 the general case, any of these a b c dcan be large, complex trial terms (which I can then perform with the evidence-based axiom of inconsistency).

Answer 1

You can use tactics f_equalthat will work not only for records, but also for arbitrary purposes of the form f x1 .. xn = f y1 .. yn, where fis any symbol of the function, of which constructors are a special case.