1

为了尝试理解如何OrderedType在 Coq 中定义我自己的，我正在研究（此处）OrderedType中标准库中给出的 s示例。截至目前，我只关心前几个模块：Coq.Structures.OrderedTypeEx

Require Import OrderedType.
Require Import ZArith.
Require Import Omega.
Require Import NArith Ndec.
Require Import Compare_dec.    

Module Type UsualOrderedType.
 Parameter Inline t : Type.
 Definition eq := @eq t.
 Parameter Inline lt : t -> t -> Prop.
 Definition eq_refl := @eq_refl t.
 Definition eq_sym := @eq_sym t.
 Definition eq_trans := @eq_trans t.
 Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
 Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
 Parameter compare : forall x y : t, Compare lt eq x y.
 Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
End UsualOrderedType.

Module UOT_to_OT (U: UsualOrderedType) <: OrderedType := U.

Module Nat_as_OT <: UsualOrderedType.

  Definition t := nat.

  Definition eq := @eq nat.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.

  Definition lt := lt.

  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.        

  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.

  Definition compare x y : Compare lt eq x y.

  Definition eq_dec := eq_nat_dec.

End Nat_as_OT.

当我在 Proof General 中自己逐步完成此操作时，Error: Proof editing in progress.当我到达最后一行时出现错误。看来它希望我lt_trans在它接受模块结束之前证明它。这很公平。但是，如果没有证据，这如何作为标准库的一部分工作呢？它是否以我不理解的方式隐含地引用了一些先前的证据？另外，如果我确实Proof. Admitted.能够跳过引理证明，那么它需要一个Definition compare x y : Compare lt eq x y.. 为什么它会要求一个定义的证明？

4

0 回答 0