Определение моего собственного типа OrderedType в Coq
Чтобы попытаться понять, как определить свой собственный OrderedType в Coq я работаю над примерами OrderedTypeдано в стандартной библиотеке в 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., Зачем ему требовать доказательства для определения?