如何自动将对称性引入Coq假设？ [英] How to automatically introduce symmetries into Coq hypotheses?

问题描述

在这些假设中，我有一些平等（ = ）和不平等（<> ），例如：

I have some equalities (=) and unequalities (<>) in the hypotheses such as:

e : x2 = x1
n : x3 <> x1

我想使用假设之类的策略，但有时目标的预期（不）平等方向相反：

I want to use tactics like assumption, but sometimes the expected (un)equality in the goal is in the other direction like:

x1 = x2
x1 <> x3

我的问题是：

是

如果没有，是否有可能使用Notation编写战术来做到这一点。

If not, is it possible to use Notation to write a tactical to do this.

到目前为止，我可以手动执行以下操作：

So far, I can do this manually like this:

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). 

但这确实很乏味且嘈杂。我对如何使它自动化或是否有更好的方法还不够了解。

But it is really tedious and noisy. I don't know enough about how to automate this or if there is a better way.

推荐答案

也许这种策略可以帮助您：

Perhaps this tactic can help:

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

这篇关于如何自动将对称性引入Coq假设？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！