0

考虑这个简单的发展。我有两种微不足道的数据类型：

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

尽管构造函数在提示数据库中，但它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不起作用。

我的问题是：是否有可能通过依赖类型类来获得统一的符号并保持证明自动化的好处？或者是否有不同的解决方案来为各种数据类型提供统一的符号。

4

2 回答 2

2

一个不涉及类型类的解决方案是利用 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.
于 2017-09-18T08:04:58.337 回答
0

问题是您的提示设置为触发，例如，@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.
于 2017-09-16T01:32:35.843 回答