Как автоматически ввести симметрии в гипотезу Coq?

Question

У меня есть некоторые равенства (=) и неравенства (<>) в гипотезах, таких как:

e : x2 = x1
n : x3 <> x1

Я хочу использовать такую ​​тактику, как assumption, но иногда ожидаемое (не) равенство в цели происходит в другом направлении, например:

x1 = x2
x1 <> x3

Мой вопрос:

Можно ли автоматически вводить симметричные формы (не) равенства выше в гипотезы?

Если нет, то можно ли использовать нотацию, чтобы написать тактику для этого.

Пока что я могу сделать это вручную следующим образом:

assert (x1 = x2) by (symmetry in e; assumption).

assert (x1 <> x3) by (unfold not; intro Hnot; 
  symmetry in Hnot; unfold not in n; apply n in Hnot; inversion Hnot). 

Но это действительно утомительно и шумно. Я не знаю достаточно о том, как автоматизировать это или есть лучший способ.

Answer 1

Возможно, эта тактика может помочь:

Ltac maybe_intro_sym A B :=
  match goal with
    |[H:B=A|-_] => fail 1
    |[H:A=B|-_] => assert (B=A) by auto
  end.

Ltac maybe_intro_sym_neg A B :=
  match goal with
    |[H:B<>A|-_] => fail 1
    |[H:A<>B|-_] => assert (B<>A) by auto
  end.

Ltac intro_sym :=
  repeat match goal with
    |[H:?A=?B|-_] => maybe_intro_sym A B
    |[H:?A<>?B|-_] => maybe_intro_sym_neg A B
  end.

Вот пример:

Parameters a b c d:nat.
Goal a=b -> c=d -> c<>d -> True.
intros.
intro_sym.

Теперь контекст

  H : a = b
  H0 : c = d
  H1 : c <> d
  H2 : d = c
  H3 : b = a
  H4 : d <> c
  ============================
   True