coq - 为什么 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 倍)。

• 有没有办法让他们在需要时自动应用对称，而不用每次都打扰我？在手册中找不到关于此问题的任何提及。

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.