coq - Coq 中类型类方法的递归使用

Question

有没有办法对 Coq 的类型类使用递归？例如，在为列表定义显示时，如果您想调用 show递归列表函数，那么你将不得不使用这样的固定点:

Require Import Strings.String.
Require Import Strings.Ascii.

Local Open Scope string_scope.


Class Show (A : Type) : Type :=
  {
    show : A -> string
  }.


Section showNormal.

Instance showList {A : Type} `{Show A} : Show (list A) :=
  {
    show :=
      fix lshow l :=
        match l with
        | nil => "[]"
        | x :: xs => show x ++ " : " ++ lshow xs
        end
  }.

End showNormal.

这一切都很好，但是如果我想定义一些用于定义 Show 的辅助函数怎么办？实例？就像我想创建一个更 DAZZLING 的显示功能，称为 magicShow在某物周围打印星星...

Definition magicShow {A : Type} `{Show A} (a : A) : string :=
  "** " ++ show a ++ " **".


Instance showMagicList {A : Type} `{Show A} : Show (list A) :=
  {
    show :=
      fix lshow l :=
        match l with
        | nil => "[]"
        | x :: xs => show x ++ " : " ++ magicShow xs
        end
  }.

但是，在这种情况下，Coq 找不到列表 xs 的显示实例。转至 magicShow :

Error:
Unable to satisfy the following constraints:
In environment:
A : Type
H : Show A
lshow : list A -> string
l : list A
x : A
xs : list A

?H : "Show (list A)"

一般有没有办法做到这一点？即，您可以使用依赖于您正在定义的类型类实例的函数为类型类定义方法吗？

Answer 1

如果必须这样做，可以通过显式使用底层Record的构造函数来模拟。 (因为“类型类是记录”，引用自软件基础 [ 1 ])，可以使用被定义为固定点的函数来实例化。我将发布三个示例并解释这在哪里有用。

您发布的示例可以这样解决(针对 Coq 8.10.1 测试的所有代码):

Require Import Strings.String.

Local Open Scope list_scope.
Local Open Scope string_scope.

Class Show (A : Type) : Type :=
  {
    show : A -> string
  }.

Definition magicShow {A : Type} `{Show A} (a : A) : string :=
  "** " ++ show a ++ " **".

Print Show.
(* Record Show (A : Type) : Type := Build_Show { show : A -> string }
*)
Check Build_Show.
(* Build_Show : forall A : Type, (A -> string) -> Show A *)
Check @magicShow.
(* @magicShow : forall A : Type, Show A -> A -> string *)

Instance showMagicList {A : Type} `{Show A} : Show (list A) :=
  {
    show :=
      fix lshow l :=
        match l with
        | nil => "[]"
        | x :: xs => show x ++ " : " ++ @magicShow _ (@Build_Show _ lshow) xs
        end
  }.

如果您尝试像这样定义几个类型类方法，则实例化记录构造函数很棘手，但可以通过将函数视为由相互递归定义的函数来完成(尽管不一定必须有任何实际的相互递归)。这是一个人为的示例，其中 Show现在有两种方法。注意 typeclass 实例被添加到带有匿名 let-in 的上下文中。捆绑。显然，这足以满足 Coq 的类型类解析机制。

Require Import Strings.String.

Local Open Scope list_scope.
Local Open Scope string_scope.

Class Show (A : Type) : Type :=
  {
    show1 : A -> string
  ; show2 : A -> string
  }.

Definition magicShow1 {A : Type} `{Show A} (a : A) : string :=
  "** " ++ show1 a ++ " **".

Definition magicShow2 {A : Type} `{Show A} (a : A) : string :=
  "** " ++ show2 a ++ " **".

Fixpoint show1__list {A : Type} `{Show A} (l : list A) : string :=
let _ := (@Build_Show _ show1__list show2__list) in
        match l with
        | nil => "[]"
        | x :: xs => show1 x ++ " : " ++ magicShow1 xs
        end
with show2__list {A : Type} `{Show A} (l : list A) : string :=
let _ := (@Build_Show _ show1__list show2__list) in
        match l with
        | nil => "[]"
        | x :: xs => show1 x ++ " : " ++ magicShow2 xs
        end.

Instance showMagicList {A : Type} `{Show A} : Show (list A) :=
  {
    show1 := show1__list
  ; show2 := show2__list
  }.

那么你为什么要这样做呢？一个很好的例子是当您在(玫瑰)树上定义可判定相等性时。在定义的中间，我们必须递归地诉诸 list (tree A) 的可判定相等性。 .我们想使用标准库辅助函数 Coq.Classes.EquivDec.list_eqdec [ 2 ]，它显示了如何在类型 A 上传递可判定相等性至 list A .由于 list_eqdec需要一个类型类实例(我们正在定义的那个)，我们必须使用上面相同的技巧:

Require Import Coq.Classes.EquivDec.
Require Import Coq.Program.Utils.

Set Implicit Arguments.
Generalizable Variables A.

Inductive tree (A : Type) : Type :=
  | leaf : A -> tree A
  | node : list (tree A) -> tree A.

Program Instance tree_eqdec `(eqa : EqDec A eq) : EqDec (tree A) eq :=
 { equiv_dec := fix tequiv t1 t2 :=
    let _ := list_eqdec tequiv in
    match t1, t2 with
    | leaf a1, leaf a2 =>
        if a1 == a2 then in_left else in_right
    | node ts1, node ts2 =>
        if ts1 == ts2 then in_left else in_right
    | _, _ => in_right
    end
}.

Solve Obligations with unfold not, equiv, complement in * ;
  program_simpl ; intuition (discriminate || eauto).

Next Obligation.
  destruct t1;
  destruct t2; 
  ( program_simpl || unfold complement, not, equiv in *; eauto ).
Qed.

Solve Obligations with split; (intros; try unfold complement, equiv ; program_simpl).
(*
No more obligations remaining
tree_eqdec is defined
*)

注释:没有用于创建 EqDec 类型记录的构造函数(因为它只有一个类方法)，所以要让 Coq 相信 list (tree A)具有可判定的相等性，调用只是 list_eqdec tequiv .对于初学者， Program这里只是允许实例定义中的漏洞稍后填写为 Obligation s，这比内联编写适当的证明更方便。