为什么 Coq 不能自己找出等式的对称性？

Question

假设我们正在尝试形式化一些（半）群论性质，如下所示：

Section Group.

Variable A: Type.
Variable op: A -> A -> A.

Definition is_left_neutral  (e: A) := forall x: A, (op e x) = x.
Definition is_right_neutral (e: A) := forall x: A, x = (op x e).

Lemma uniqueness_of_neutral:
  forall a b: A, (is_left_neutral a) -> (is_right_neutral b) -> (a = b).
Proof.
  intro; intro.
  intros lna rnb.
  elim lna with b; elim rnb with a.
  reflexivity.
Qed.

End Group.

它工作得很好，但是，如果我们反转上述任一定义中的等式，即将定义替换为

Definition is_left_neutral  (e: A) := forall x: A, x = (op e x).

和

Definition is_right_neutral (e: A) := forall x: A, (op x e) = x.

证明在 reflexivity 处失败，因为一个或两个 elim 应用程序什么都不做。基于 assert，当然有解决方法，但那是......太费力而且很烦人......

Coq的策略（elim、case等）对顺序如此敏感，这是有原因的吗？我想，它不应该显着减慢策略（<< 2 次）。
有没有办法让它们在需要时自动应用 symmetry，而不用每次都打扰我？在手册中找不到任何关于此问题的提及。

Answer 1

首先，使用elim来操纵平等是很麻烦的。以下是我将如何编写您的证明，使用 rewrite，并更改 is_left_neutral.

的定义

Section Group.

Variable A: Type.
Variable op: A -> A -> A.

Definition is_left_neutral  (e: A) := forall x: A, op e x = x.
Definition is_right_neutral (e: A) := forall x: A, op x e = x.

Lemma uniqueness_of_neutral:
  forall a b: A, is_left_neutral a -> is_right_neutral b -> a = b.
Proof.
  intros a b lna rnb.
  now rewrite <- (lna b), rnb.
Qed.

End Group.

注意第一个重写中的 <-：它告诉 Coq 从右到左而不是从左到右重写。当您使用 elim 时，您基本上只能在一个方向（从右到左）重写，这会导致您看到的行为。

我现在想不出在重写策略中只尝试一个方向的原因，但我不认为这是出于性能原因。在任何情况下，您都可以定义自己的 rewrite 变体，它尝试从左到右重写，然后从右到左重写，如果这不起作用：

Section Group.

Variable A: Type.
Variable op: A -> A -> A.

Definition is_left_neutral  (e: A) := forall x: A, op e x = x.
Definition is_right_neutral (e: A) := forall x: A, op x e = x.

Ltac my_rewrite t :=
  first [ rewrite t | rewrite <- t ].

Lemma uniqueness_of_neutral:
  forall a b: A, is_left_neutral a -> is_right_neutral b -> a = b.
Proof.
  intros a b lna rnb.
  now my_rewrite (lna b); my_rewrite rnb.
Qed.

End Group.

为什么 Coq 不能自己找出等式的对称性？

Why can't Coq figure out symmetry of the equality by itself?

formal-verification

formal-methods

coq

formal-languages

coq-tactic