Pourquoi Coq ne peut-il pas comprendre la symétrie de l'égalité par lui-même?

Question

Supposons que nous essayons de formaliser certains (semi) propriétés du groupe-théorétique, comme ceci:

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. 

Il fonctionne très bien, mais, si on inverse l'équation dans l'une des définitions ci-dessus, à savoir remplacer les définitions de

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

et

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

respectivement, la preuve ne parvient pas à reflexivity, car une ou les deux applications elim ne font rien. Bien sûr, il existe une solution pour elle, basée sur assert, mais qui est ... trop d'effort et tout simplement ennuyeux ...

• Y at-il une raison pour laquelle la tactique impliqués Coq (elim, case, etc.) sont tellement sensibles à la commande? Je suppose, il ne faut pas ralentir sensiblement la tactique (< < 2 fois).

• Y at-il un moyen de les faire appliquer automatiquement symmetry, le cas échéant, sans me déranger à ce sujet à chaque fois? Impossible de trouver une mention de ce problème dans le manuel.

Answer 1

D'abord, l'utilisation de elim pour manipuler l'égalité est fastidieuse. Voici comment je voudrais écrire votre preuve, en utilisant rewrite, et en changeant la définition de 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. 

Notez que le <- dans la première rewrite: il dit Coq de réécrire de l'INSEAD de droite à gauche de gauche à droite. Lorsque vous utilisez elim, vous pouvez essentiellement réécrire uniquement dans une direction (de droite à gauche), ce qui conduit au comportement que vous avez vu.

Je ne peux pas penser maintenant à une raison pour essayer seulement une direction dans la tactique de réécriture, mais je ne pense pas que ce soit pour des raisons de performance. Dans tous les cas, vous pouvez définir votre propre variante de rewrite, qui tente de réécrire de gauche à droite, puis de droite à gauche, si cela ne fonctionne pas:

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.