なぜ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. 

で定義を置き換える、証明はで失敗しますのアプリケーションのいずれかまたは両方が何もしないためです。 そこ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. 

お知らせ最初の書き換えで<-：それは左から右の右から左へINSEADから書き換えるようにコックを伝えます。 elimを使用すると、本質的に一方向（右から左）で書き換えることができます。これは、見た動作につながります。

書き直し戦術で片方向しか試していない理由は今考えることができませんが、パフォーマンス上の理由ではないと思います。あなたはELIMを使用することを選んだのはなぜ

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.