Coq: Verwendung von `PartialOrder` typeclass

Question

Ich versuche lexikographische Anordnung auf Strings über Posets zu definieren, aber ich bin mir nicht ganz sicher, wie man die PartialOrder Typklasse verwendet.

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). 

Teilausgang:

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

Klar <= ist die falsche Schreibweise hier zu verwenden; Ich frage mich, wie ich eine Bestellbeziehung von meiner po Instanz erhalten kann.

Answer 1

Man kann die Namen explizit binden, um die Dinge offensichtlicher zu machen. Bevor wir dies tun können, müssen wir Coq sagen, nicht über ungebundene Variablen zu beklagen den Generalizable Variables Befehl:

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). 

Sie können weitere Informationen im Handbuch (here) finden.