Coq：PartialOrder類型類的使用

我試圖在字符串上定義字典順序，但我不完全確定如何使用類型類型PartialOrder。Coq：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實例中獲得訂購關係。

來源

2017-06-18 Carl Patenaude Poulin

在這種情況下，關係被命名爲'R'，所以'R hd1 hd2'將起作用;在這種情況下，你當然可以定義你自己的符號。 – ejgallego

可以明確地綁定名稱以使事情更加明顯。我們能做到這一點之前，我們需要告訴勒柯克不要去抱怨使用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).

您可以在手動（here）的更多信息。

來源

2017-06-18 08:32:03

Coq：PartialOrder類型類的使用

回答

相關問題