\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\lb}{\lambda} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\Nat}{\mathbb{N}} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\Prod}{\textsf{prod}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\cal S} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} \newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

正準構造¶

著者: Assia Mahboubi and Enrico Tassi

この章では正準構造の基本とそれらが記法のオーバーロードや代数構造の階層の構築にどのように使えるかを説明します。例は [MT13] から抜粋しています。簡潔さのためにここでは省略した全ての詳細について興味のある読者にはこの論文を参照することを勧めます。興味のある読者は [GZND11] にも別の、相補的な、正準構造の使用: 高度な証明探索についての詳細な説明を発見するでしょう。後者の論文は正準構造の推論を調整するために用いることが出来るたくさんのテクニックも述べています。

表記法オーバーローディング¶

比較述語のための中置記法 == を構築します。そのような記法はオーバーロードされ、その意味は比較される項の型に依存することになるでしょう。

Module EQ.: Interactive Module EQ started
Record class (T : Type) := Class { cmp : T -> T -> Prop }.: class is defined cmp is defined
Structure type := Pack { obj : Type; class_of : class obj }.: type is defined obj is defined class_of is defined
Definition op (e : type) : obj e -> obj e -> Prop := let 'Pack _ (Class _ the_cmp) := e in the_cmp.: op is defined
Check op.: op : forall e : type, obj e -> obj e -> Prop
Arguments op {e} x y : simpl never.
Arguments Class {T} cmp.
Module theory.: Interactive Module theory started
Notation "x == y" := (op x y) (at level 70).
End theory.: Module theory is defined
End EQ.: Module EQ is defined

Coq のモジュールを名前空間として使います。これによってこの章のこれ以降では同じパターンと命名規則に従うことが出来ます。この基本名前空間は代数構造の定義を含んでいます。例を小さく保つため、我々が定義する代数構造 EQ.type は非常に単純でかつ、ある定義された二項関係上で項を特徴づけ、そのような関係に要求されるどんな性質の正当性の立証もありません。内部のtheoryモジュールはオーバーロードされた記法 == を含み、その代数構造の全てのインスタンスを保持する補題をも含みます (この場合は補題はありません)。

留意すべきは、実際にはユーザは EQ.obj をコアーションとして定義したいかもしれませんが、ここではそれは行いません。

以下の行では EQ クラス内の型 e を仮定したとき、== によってそのオブジェクト二つを関連付けることが出来ることをテストしています。

Import EQ.theory.
Check forall (e : EQ.type) (a b : EQ.obj e), a == b.: forall (e : EQ.type) (a b : EQ.obj e), a == b : Prop

まだ EQ クラスの中には具体的な型はありません。

Fail Check 3 == 3.: The command has indeed failed with message: The term "3" has type "nat" while it is expected to have type "EQ.obj ?e".

これを nat に比較関係を授けることで修正します。

Definition nat_eq (x y : nat) := Nat.compare x y = Eq.: nat_eq is defined
Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq.: nat_EQcl is defined
Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl.: nat_EQty is defined
Check 3 == 3.: 3 == 3 : Prop
Eval compute in 3 == 4.: = Lt = Eq : Prop

この最後のテストは Coq がもはや 3 == 3 の型検査が出来るだけでなく、中置関係が nat_eq 関係に束縛されたことを示しています。この関係は == が nat 型の項の上で使われるときはいつでも選択されます。これは正準構造 nat_EQty を定義した行の中で読み取ることが出来、ここで Pack の最初の引数がキーであり、二番目の引数がそのキーに関連付けられた正準値のグループです。この場合は nat に高々一つの正準値を関連付けました (そのクラスについても、nat_EQcl はただ一つのメンバを持っています)。射影 op の使用はその引数が EQ クラスに属していることを要求し、そのようなメンバ (関数) を実際にその引数を比較するために使います。

同様に、他のどんな型でも比較関係を整えて、そしてこの型の項の上で == 記法を使うことが出来ます。

派生した正準構造¶

私たちは nat、bool、Z のような基本型上で == をどのように使うかを知っています。ここでは型コンストラクタをどのように扱うか、つまり以下の例がどのように動作するかを示します:

Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b).: The command has indeed failed with message: In environment e : EQ.type a : EQ.obj e b : EQ.obj e The term "(a, b)" has type "(EQ.obj e * EQ.obj e)%type" while it is expected to have type "EQ.obj ?e".

このエラーメッセージは Coq がオブジェクトのペアをどのように比較するかについて知らないと言っています。以下の構成は Coq にまさにそれをどのように行うかを教えています。

Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) := fst x == fst y /\ snd x == snd y.: pair_eq is defined
Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2).: pair_EQcl is defined
Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type := EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2).: pair_EQty is defined
Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b).: forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b) : Prop
Check forall n m : nat, (3, 4) == (n, m).: forall n m : nat, (3, 4) == (n, m) : Prop

pair_EQty 定義のおかげで、Coq はそのペアの各コンポーネントの比較関数を構築することが出来るときは、いつでもペアのための比較関係を構築することが出来ます。その定義は型コンストラクタ * がそれら自身が EQ クラスの中にある二つの型に適用されるときは、キーである * (ペアの型コンストラクタ) に正準比較関係 pair_eq を関連付けます。

構造の階層¶

興味深い例を得るにはもう一つの基本クラスを必要とします。中置 <= 記法を伴った順序関係を装備した型のクラスを選択します。

Module LE.: Interactive Module LE started
Record class T := Class { cmp : T -> T -> Prop }.: class is defined cmp is defined
Structure type := Pack { obj : Type; class_of : class obj }.: type is defined obj is defined class_of is defined
Definition op (e : type) : obj e -> obj e -> Prop := let 'Pack _ (Class _ f) := e in f.: op is defined
Arguments op {_} x y : simpl never.
Arguments Class {T} cmp.
Module theory.: Interactive Module theory started
Notation "x <= y" := (op x y) (at level 70).
End theory.: Module theory is defined
End LE.: Module LE is defined

これまでのように nat のために正準 LE クラスを登録します。

Import LE.theory.
Definition nat_le x y := Nat.compare x y <> Gt.: nat_le is defined
Definition nat_LEcl : LE.class nat := LE.Class nat_le.: nat_LEcl is defined
Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.: nat_LEty is defined

そして Coq に項のペアを <= によって関連付けさせます。

Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) := fst x <= fst y /\ snd x <= snd y.: pair_le is defined
Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2).: pair_LEcl is defined
Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type := LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2).: pair_LEty is defined
Check (3,4,5) <= (3,4,5).: (3, 4, 5) <= (3, 4, 5) : Prop

現段階では我々は自然数の組のような具体型の上で == と <= を使うことができますが、両方の関係を備えた型上の代数的理論を開発することはできません。

Check 2 <= 3 /\ 2 == 2.: 2 <= 3 /\ 2 == 2 : Prop
Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.: The command has indeed failed with message: In environment e : EQ.type x : EQ.obj e y : EQ.obj e The term "x" has type "EQ.obj e" while it is expected to have type "LE.obj ?e".
Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.: The command has indeed failed with message: In environment e : LE.type x : LE.obj e y : LE.obj e The term "x" has type "LE.obj e" while it is expected to have type "EQ.obj ?e".

EQ と LE の両方から派生した新しいクラスを定義する必要があります。

Module LEQ.: Interactive Module LEQ started
Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) := Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }.: mixin is defined compat is defined
Record class T := Class { EQ_class : EQ.class T; LE_class : LE.class T; extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.: class is defined EQ_class is defined LE_class is defined extra is defined
Structure type := _Pack { obj : Type; class_of : class obj }.: type is defined obj is defined class_of is defined
Arguments Mixin {e le} _.
Arguments Class {T} _ _ _.

`LEQ` クラスの構成部品 mixin は EQ と LE に追加している特別な内容を全て含んでいます. 特にそれは組み合わせた両立できる二つの要求を含んでいます。

残念ながら未だにこの新しいクラスの代数理論の開発の障害があります。

Module theory.: Interactive Module theory started
Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.: The command has indeed failed with message: In environment le : type n : obj le m : obj le The term "n" has type "obj le" while it is expected to have type "LE.obj ?e".

問題は LE と LEQ という二つのクラスが未だにサブクラス関係によって関連付いてないことです。言い換えれば、Coq は LEQ クラスのオブジェクトが LE クラスのオブジェクトでもあるということが分かりません。

以下の二つの構成は Coq に LE.type と EQ.type 構造を同じ型上で与えられた LEQ.type 構造からどのように標準的に構築するかを伝えます。

Definition to_EQ (e : type) : EQ.type := EQ.Pack (obj e) (EQ_class _ (class_of e)).: to_EQ is defined
Canonical Structure to_EQ.
Definition to_LE (e : type) : LE.type := LE.Pack (obj e) (LE_class _ (class_of e)).: to_LE is defined
Canonical Structure to_LE.

我々は今や LEQ 構造のオブジェクト上で最初の定理を定式化することが出来ます。

Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.: 1 subgoal e : type x, y : obj e ============================ x <= y -> y <= x -> x == y
now intros; apply (compat _ _ (extra _ (class_of e)) x y); split.: No more subgoals.
Qed.: lele_eq is defined
Arguments lele_eq {e} x y _ _.
End theory.: Module theory is defined
End LEQ.: Module LEQ is defined
Import LEQ.theory.
Check lele_eq.: lele_eq : forall x y : LEQ.obj ?e, x <= y -> y <= x -> x == y where ?e : [ |- LEQ.type]

もちろん代数的構造のどんな具体例についても代数的な背景の中で証明された結果を適用したい人もいるでしょう。

Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.: 1 subgoal n, m : nat ============================ n <= m -> m <= n -> n == m
Fail apply (lele_eq n m).: The command has indeed failed with message: In environment n, m : nat The term "n" has type "nat" while it is expected to have type "LEQ.obj ?e".
Abort.
Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : n <= m -> m <= n -> n == m.: 1 subgoal l1, l2 : LEQ.type n, m : LEQ.obj l1 * LEQ.obj l2 ============================ n <= m -> m <= n -> n == m
Fail apply (lele_eq n m).: The command has indeed failed with message: In environment l1, l2 : LEQ.type n, m : LEQ.obj l1 * LEQ.obj l2 The term "n" has type "(LEQ.obj l1 * LEQ.obj l2)%type" while it is expected to have type "LEQ.obj ?e".
Abort.

この場合も Coq に nat 型が LEQ クラスに属していること、そして型コンストラクタ * が LEQ クラスとどのように相互作用するのかを伝える必要があります。以下の証明は簡潔さのため省略されています。

Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m.: 1 subgoal n, m : nat ============================ n <= m /\ m <= n <-> n == m
Admitted.: nat_LEQ_compat is declared
Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat.: nat_LEQmx is defined
Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : n <= m /\ m <= n <-> n == m.: 1 subgoal l1, l2 : LEQ.type n, m : LEQ.obj l1 * LEQ.obj l2 ============================ n <= m /\ m <= n <-> n == m
Admitted.: pair_LEQ_compat is declared
Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).: pair_LEQmx is defined

以下のスクリプトは LEQ クラスに nat と型コンストラクタ * を登録します。それらが期待通りに動作することをテストもします。

残念ながらこれらの定義は非常に冗長です。続く項ではそれらをどのようによりコンパクトにするかを示します。

Module Add_instance_attempt.: Interactive Module Add_instance_attempt started
Canonical Structure nat_LEQty : LEQ.type := LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx).: nat_LEQty is defined
Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type := LEQ._Pack (LEQ.obj l1 * LEQ.obj l2) (LEQ.Class (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2))) (LE.class_of (pair_LEty (to_LE l1) (to_LE l2))) (pair_LEQmx l1 l2)).: pair_LEQty is defined Toplevel input, characters 0-264: > Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type := LEQ._Pack (LEQ.obj l1 * LEQ.obj l2) (LEQ.Class (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2))) (LE.class_of (pair_LEty (to_LE l1) (to_LE l2))) (pair_LEQmx l1 l2)). > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Ignoring canonical projection to LEQ.Class by LEQ.class_of in pair_LEQty: redundant with nat_LEQty
Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.: 1 subgoal n, m : nat ============================ n <= m -> m <= n -> n == m
now apply (lele_eq n m).: No more subgoals.
Qed.: test_algebraic is defined
Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m.: 1 subgoal n, m : nat * nat ============================ n <= m -> m <= n -> n == m
now apply (lele_eq n m).: No more subgoals.
Qed.: test_algebraic2 is defined
End Add_instance_attempt.: Module Add_instance_attempt is defined

注目すべきは nat * nat 型の n と m についての n <= m -> m <= n -> n == m の直接の証明はユーザから提供されていないことです。ユーザが提供したものは n と m の型 nat についてのこのステートメントの証明とペアコンストラクタがこの性質を保存するという証明です。これら二つの事実の組み合わせは正準構造を推論している間、Coq が自動的に行う証明探索の単純な形です。

正準構造のコンパクトな定義¶

いくらかの基盤が必要です。

Require Import Strings.String.: [Loading ML file z_syntax_plugin.cmxs ... done] [Loading ML file quote_plugin.cmxs ... done] [Loading ML file newring_plugin.cmxs ... done] [Loading ML file ascii_syntax_plugin.cmxs ... done] [Loading ML file string_syntax_plugin.cmxs ... done]
Module infrastructure.: Interactive Module infrastructure started
Inductive phantom {T : Type} (t : T) : Type := Phantom.: phantom is defined phantom_rect is defined phantom_ind is defined phantom_rec is defined
Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := phantom t1 -> phantom t2.: unify is defined
Definition id {T} {t : T} (x : phantom t) := x.: id is defined
Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) (at level 50, v ident, only parsing).
Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) (at level 50, v ident, only parsing).
Notation "'Error : t : s" := (unify _ t (Some s)) (at level 50, format "''Error' : t : s").
Open Scope string_scope.
End infrastructure.: Module infrastructure is defined

記法 [find v | t1 ~ t2] を説明するため、具体例の一つ [find e | EQ.obj e ~ T | "is not an EQ.type" ] を取り上げます。これは以下のように読めます: “あるクラス e を見つける。そのオブジェクトは型 T を持ち、そうでない場合は "T is not an EQ.type" というメッセージとともに失敗する”。

他のユーティリティは Coq に正準構造の推論を必要とすることになるであろう特定的な単一化問題を解くように要求するのに使われます。それらは [MT13] の中でより詳細に説明されています。

今や我々は LEQ クラスのインスタンスを定義するためのコンパクトな "荷造り業者" を作るために必要なものを全て持っています。

Import infrastructure.
Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) := [find e | EQ.obj e ~ T | "is not an EQ.type" ] [find o | LE.obj o ~ T | "is not an LE.type" ] [find ce | EQ.class_of e ~ ce ] [find co | LE.class_of o ~ co ] [find m | m ~ m0 | "is not the right mixin" ] LEQ._Pack T (LEQ.Class ce co m).: packager is defined
Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).

オブジェクト Pack は型 T (キー) と mixin m を取ります。それは LEQ クラスの他の全ての部分を推論し、キーとなる T に関連付けられた正準値としてそれらを定義します。結局のところ、我々が LEQ クラスに新たに追加した情報の断片は mixin だけであり、残りの全ては既に T について正準であり、従って Coq により推論することが出来ます。

Pack は記法であり、従ってその定義時点では型検査されません。それが使われ、T が具体型になるときに型検査されます。packager に渡した奇妙な引数 _ と id はそれぞれ推論されるべきクラス (e や o その他) とそれらの推論を強制するためのトークン (id) を表します。繰り替えしますが、全ての詳細について [MT13] が読者の参考になります。

正準インスタンスの定義は今やよりコンパクトになりえます。

Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.: nat_LEQty is defined
Canonical Structure pair_LEQty (l1 l2 : LEQ.type) := Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2).: pair_LEQty is defined Toplevel input, characters 0-118: > Canonical Structure pair_LEQty (l1 l2 : LEQ.type) := Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2). > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Ignoring canonical projection to LEQ.Class by LEQ.class_of in pair_LEQty: redundant with nat_LEQty

エラーメッセージも非常に理解しやすいです (メッセージの末尾まで飛ばすなら)。

Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx.: The command has indeed failed with message: The term "id" has type "phantom (EQ.obj ?e) -> phantom (EQ.obj ?e)" while it is expected to have type "'Error:bool:"is not an EQ.type"".