類型類和自動策略之間的相互作用

Question

考慮這個簡單的發展。我有兩個複雜數據類型：

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. 

兩個證明已完成auto策略，第一個證據至關重要地依靠Hint Constructors和第二個另外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. 

但現在證明自動化休息！例如：

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

給我留下了一個目標：

2 subgoals, subgoal 1 (ID 32) 

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

是auto不再儘管AOrd構造中暗示數據庫中解決。我可以通過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不再解決了這一目標。即使apply AOrd_reflexive不起作用。

我的問題是：是否有可能通過依賴類型類來保持統一的表示法並保持證明自動化的好處？或者有不同的解決方案來爲各種數據類型提供統一的符號。

Answer 1

不涉及類型類的溶液是採取Coq的範圍機制的優勢。

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

問題是您的提示設置爲觸發，例如，@orderR _ AOrd A1 A2，而不是AOrd A1 A2。所以自動化永遠不會看到它正在尋找的模式，也決不會觸發提示。這裏有兩種解決方案：

（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.