Разделите цель соединения на подцели

Рассмотрим следующее игрушечное упражнение:

Theorem swap_id: forall (m n : nat), m = n -> (m, n) = (n, m).
Proof.
  intros m n H.

На данный момент у меня есть следующее:

1 subgoal
m, n : nat
H : m = n
______________________________________(1/1)
(m, n) = (n, m)

Я хотел бы разделить цель на две подцели m = n и n = m. Есть ли такая тактика?


coq coq-tactic
person Carl Patenaude Poulin    schedule 12.05.2017    source источник
comment
Это просто для развлечения или есть какая-то серьезная причина для разделения цели?   -  person Anton Trunov    schedule 12.05.2017
comment
Нет веской причины, я просто пытаюсь выучить базовые идиомы Coq.   -  person Carl Patenaude Poulin    schedule 13.05.2017

Ответы (1)


arrow_upward
4
arrow_downward

Решите проблему с помощью тактики f_equal:

Theorem test: forall (m n : nat), m = n -> (m, n) = (n, m).
Proof.
  intros m n H. f_equal.

С состоянием:

2 subgoals
m, n : nat
H : m = n
______________________________________(1/2)
m = n
______________________________________(2/2)
n = m
person Carl Patenaude Poulin    schedule 12.05.2017
comment
Комментарий о причине работы f_equal: если мы развернем некоторые нотации, мы перейдем от цели (m, n) = (n, m) к pair m n = pair n m, где pair - единственный конструктор типа данных prod. На этом этапе должно быть очевидно, почему f_equal разделяет цель на две подцели. - person Anton Trunov; 12.05.2017