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

user_5983187 0
Viewed 745

Suppose we're trying to formalize some (semi)group-theoretic properties, like this:

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.

It works just fine, but, if we reverse the equation in either of the above definitions, i.e. replace the definitions with

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

and

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

respectively, the proof fails at reflexivity, since one or both of the elim applications do nothing. Sure there is a workaround for it, based on assert, but that's... too much effort and simply annoying...

  • Is there a reason why the involved Coq tactics (elim, case, etc.) are so much sensitive to the order? I suppose, it shouldn't slow down the tactics any noticeably (<< 2 times).

  • Is there a way to make them apply symmetry automatically, where needed, without bothering me about it every time? Couldn't find any mention of this issue in the manual.

coq-tactic formal-methods coq formal-verification formal-languages
1 Answers

First, using elim to manipulate equality is cumbersome. Here is how I would write your proof, using rewrite, and changing the definition of 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.

Notice the <- in the first rewrite: it tells Coq to rewrite from right-to-left insead of left-to-right. When you use elim, you can essentially only rewrite in one direction (right-to-left), which leads to the behavior that you saw.

I can't think right now of a reason for only trying one direction in the rewrite tactic, but I do not think it is for performance reasons. In any case, you can define your own variant of rewrite, which tries to rewrite left-to-right, and then right-to-left, if that does not work:

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.
user_16337700
Related