type 类 和 auto 战术之间的交互
Interaction between type classes and auto tactic
考虑一下这个简单的开发。我有两种简单的数据类型：
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 数据类型的排序关系有一个单独的符号。我希望能够在任何地方统一使用 <=。 提供了解决问题的方法：使用类型 classes。所以我引入了一个类型 class 用于排序并重新定义我的排序关系以使用这个新符号：
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
尽管 AOrd 构造函数在提示数据库中，但 auto 不再解决。不过我可以用 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 也不起作用。
我的问题是：是否可以通过依赖类型 classes 来获得统一的符号并保持证明自动化的好处？或者是否有不同的解决方案来为各种数据类型使用统一的符号。
问题是您的提示设置为触发 @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) 您可以定义 "folding" 转换类型的引理，并将其添加到数据库中：
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.
不涉及类型类的解决方案是利用 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.
考虑一下这个简单的开发。我有两种简单的数据类型：
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 数据类型的排序关系有一个单独的符号。我希望能够在任何地方统一使用 <=。
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
尽管 AOrd 构造函数在提示数据库中，但 auto 不再解决。不过我可以用 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 也不起作用。
我的问题是：是否可以通过依赖类型 classes 来获得统一的符号并保持证明自动化的好处？或者是否有不同的解决方案来为各种数据类型使用统一的符号。
问题是您的提示设置为触发 @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) 您可以定义 "folding" 转换类型的引理，并将其添加到数据库中：
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.
不涉及类型类的解决方案是利用 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.