Coq tactic for record equality?
coq, coq-tactic
Solution
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.
Problem
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).