タイプクラスと自動戦術の相互作用

Question

この簡単な開発を考えてみましょう。私は2つの些細なデータ型を持っている：

Inductive A := 
| A1 
| A2. 

Inductive B := 
| B1 : A -> B 
| B2. 

は、今私は関係の概念を導入し、データ型AとBに発注定義誘導データ型として表現：

Definition relation (X : Type) := X -> X -> Prop. 

Reserved Notation "a1 '<=A' a2" (at level 70). 

Inductive AOrd : relation A := 
| A1_Ord : A1 <=A A1 
| A2_Ord : A2 <=A A2 
| A1_A2 : A1 <=A A2 
where "a1 '<=A' a2" := (AOrd a1 a2). 

Reserved Notation "b1 '<=B' b2" (at level 70). 

Inductive BOrd : relation B := 
| B1_Ord : forall a1 a2, 
    a1 <=A a2 -> B1 a1 <=B B1 a2 
| B2_Ord : 
    B2 <=B B2 
| B1_B2 : forall a, 
    B1 a <=B B2 
where "b1 '<=B' b2" := (BOrd b1 b2). 

最後に、私は概念を導入します再帰性のと私の関係の両方が反射的であることを証明：

Definition reflexive {X : Type} (R : relation X) := 
    forall a : X, R a a. 

Hint Constructors AOrd BOrd. 

Theorem AOrd_reflexive : reflexive AOrd. 
Proof. 
    intro a. induction a; auto. 
Qed. 

Hint Resolve AOrd_reflexive. 

Theorem BOrd_reflexive : reflexive BOrd. 
Proof. 
    intro b. induction b; auto. 
Qed. 

どちらの証明はで終了します第1の証拠は決定的にHint Constructorsに依存し、第2の証拠はさらにHint Resolve AOrd_reflexiveにヒントデータベースに追加されている。

上記コードの醜いところは、AとBのデータ型の順序関係のための別個の表記法です。どこでも一様に<=を使用できるようにしたいと考えています。 This answerは問題の解決策を提供します：型クラスを使用します。だから私は、注文するための型クラスを導入し、この新しい表記法を使用するために私の順序関係を再定義：

Class OrderR (T : Type) := orderR : relation T. 
Notation "x '<=' y" := (orderR x y) (at level 70). 

Inductive AOrd : OrderR A := 
| A1_Ord : A1 <= A1 
| A2_Ord : A2 <= A2 
| A1_A2 : A1 <= A2. 

Inductive BOrd `{OrderR A} : OrderR B := 
| B1_Ord : forall a1 a2, 
    a1 <= a2 -> B1 a1 <= B1 a2 
| B2_Ord : 
    B2 <= B2 
| B1_B2 : forall a, 
    B1 a <= B2. 

Hint Constructors AOrd BOrd. 

しかし、今証明オートメーション休憩を！たとえば：

2 subgoals, subgoal 1 (ID 32) 

    ───────────────────────────────────────────────────── 
    AOrd A1 A1 

autoはもはやヒントデータベースにあるAOrdコンストラクタにもかかわらず、解決していること：

Theorem AOrd_reflexive : reflexive AOrd. 
Proof. 
    intro a. induction a. 

は目標を私に残します。でも、私はconstructorでゴールを解決することができます：

Theorem AOrd_reflexive : reflexive AOrd. 
Proof. 
    intro a. induction a; constructor. 
Qed. 

より多くの問題は、第二の証明で発生します。やった後：

Theorem BOrd_reflexive `{OrderR A} : reflexive BOrd. 
Proof. 
    intro b. induction b. constructor. 

を私が目標に残っていないのです：

2 subgoals, subgoal 1 (ID 40) 

    H : OrderR A 
    a : A 
    ───────────────────────────────────────────────────── 
    a <= a 

は再び、autoは、もはやこの目標を解決します。 Even apply AOrd_reflexiveも機能しません。

私の質問は：型クラスに依存して一貫した表記をし、証明自動化の利点を維持することは可能ですか？または、さまざまなデータ型に対して一意の表記法を使用することとは異なる解決策があります。

Answer 1

ソリューションは、コックのスコープメカニズムを利用することです。

Inductive A := 
| A1 
| A2. 

Inductive B := 
| B1 : A -> B 
| B2. 

Definition relation (X : Type) := X -> X -> Prop. 

Reserved Notation "a1 '<=' a2" (at level 70). 

Inductive AOrd : relation A := 
| A1_Ord : A1 <= A1 
| A2_Ord : A2 <= A2 
| A1_A2 : A1 <= A2 
where "a1 '<=' a2" := (AOrd a1 a2) : a_scope. 

Delimit Scope a_scope with a. 

Inductive BOrd : relation B := 
| B1_Ord : forall a1 a2, 
    (a1 <= a2)%a -> B1 a1 <= B1 a2 
| B2_Ord : 
    B2 <= B2 
| B1_B2 : forall a, 
    B1 a <= B2 
where "b1 '<=' b2" := (BOrd b1 b2) : b_scope. 

Delimit Scope b_scope with b. 

Definition reflexive {X : Type} (R : relation X) := 
    forall a : X, R a a. 

Hint Constructors AOrd BOrd. 

Theorem AOrd_reflexive : reflexive AOrd. 
Proof. 
    intro a. induction a; auto. 
Qed. 

Hint Resolve AOrd_reflexive. 

Theorem BOrd_reflexive : reflexive BOrd. 
Proof. 
    intro b. induction b; auto. 
Qed. 

Answer 2

ヒントがトリガーするように設定されています（AOrd A1 A2ではなく@orderR _ AOrd A1 A2など）。したがって、自動化は、それが探しているパターンを決して見ず、ヒントをトリガーしません。ここでは、2つのソリューションです：

ヒントデータベースに追加するときにトリガするようにあなたがそれらをしたいとき（1）あなたは、あなたのコンストラクタの種類を調整することができます。

Hint Resolve (A1_Ord : AOrd _ _) (A2_Ord : AOrd _ _) (A1_A2 : AOrd _ _). 
Hint Resolve (@B1_Ord : forall H a1 a2, _ -> BOrd _ _) 
    (@B2_Ord : forall H, BOrd _ _) 
    (@B1_B2 : forall H a, BOrd _ _). 

（2）することができます型を変換する「折りたたみ」補題を定義し、データベースにそれらを追加します。型クラスを必要としない

Definition fold_AOrd a1 a2 (v : a1 <= a2) : AOrd a1 a2 := v. 
Definition fold_BOrd `{OrderR A} (a1 a2 : B) (v : a1 <= a2) : BOrd a1 a2 := v. 
Hint Resolve fold_AOrd fold_BOrd.