Stream: Coq users

Topic: Tactic to prove equality of pairs?


view this post on Zulip Jordan Mitchell Barrett (Apr 01 2021 at 10:49):

Suppose my current goal reads

(a,b) = (a0,b0)

Is there a tactic I can apply to discharge this goal, and generate two new goals:

a = a0
b = b0

?

More generally, if I have a type

Inductive foo :=
...
| bar : A0 -> A1 -> ... -> An -> foo
...

and a goal that reads

bar a0 a1 ... an = bar a'0 a'1 ... a'n

can I discharge this to the n+1 goals

a0 = a'0
a1 = a'1
...
an = a'n

?

view this post on Zulip Alix Trieu (Apr 01 2021 at 10:50):

The f_equal tactic ?

view this post on Zulip Jordan Mitchell Barrett (Apr 01 2021 at 10:57):

Works a charm, thanks!


Last updated: Feb 06 2023 at 13:03 UTC