3

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

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在需要的地方自动应用，而不用每次都打扰我？在手册中找不到任何提及此问题的内容。

4

1 回答 1

5

首先，使用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.
于 2017-09-21T23:25:23.357 回答