Почему 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.