为什么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,但这......太多的努力,只是烦人......

• 是否有一个原因涉及勒柯克战术(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从左到右从右到左的insead重写.使用时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.