Coq：“`PartialOrder` ` typeclass”的用法

Question

我试图在偏序集上定义字符串上的字典顺序，但我不完全确定如何使用PartialOrder类型集。

Require Import List RelationClasses.

Fail Inductive lex_leq {A : Type} `{po : PartialOrder A} : list A -> list A -> Prop :=
  | lnil: forall l, lex_leq nil l
  | lcons: 
      forall (hd1 hd2 : A) (tl1 tl2 : list A),
        hd1 <= hd2 -> (* error *)
        (hd1 = hd2 -> lex_leq tl1 tl2) -> 
        lex_leq (hd1 :: tl1) (hd2 :: tl2).

部分产出：

The term "hd1" has type "A" while it is expected to have type "nat".

显然，在这里使用<=是错误的；我想知道如何从我的po实例中获得排序关系。

Answer 1

我们可以显式地绑定名称以使事情变得更加明显。在完成此操作之前，我们需要告诉Coq不要使用Generalizable Variables命令抱怨未绑定的变量：

From Coq Require Import List RelationClasses.

Generalizable Variables A eqA R.

Inductive lex_leq `{PartialOrder A eqA R} : list A -> list A -> Prop :=
  | lnil: forall l, lex_leq nil l
  | lcons: 
      forall (hd1 hd2 : A) (tl1 tl2 : list A),
        R hd1 hd2 ->
        (hd1 = hd2 -> lex_leq tl1 tl2) -> 
        lex_leq (hd1 :: tl1) (hd2 :: tl2).

您可以在手册(这里)中找到更多信息。