????在 Coq 中，我們通常稱類型為 A -> B 的對(duì)象為“函數(shù)”，但這與數(shù)學(xué)上的“函數(shù)”有一定的區(qū)別。數(shù)學(xué)上的函數(shù)具有“定義域”的屬性，從而有??。為了實(shí)現(xiàn)這種效果，我們可以用類型為?A -> option B 的對(duì)象來(lái)模擬數(shù)學(xué)上的 A -> B 函數(shù)。option 具有類型 Type -> Type，對(duì)于類型 A，具有類型 option A 的對(duì)象或者是 None，或者是 Some a（其中 a : A）。我們首先進(jìn)行以下的準(zhǔn)備工作：（注：下文中，“函數(shù)”可能指的是有定義域的數(shù)學(xué)上的函數(shù)，也可能指的是 A -> B 類型的對(duì)象，需要結(jié)合上下文判斷）

????IsSome 用于判斷一個(gè) option A 類型的對(duì)象是否可寫成 Some a（其中 a : A）。x [∈] S 表示 x 可寫成 Some a 且 a ∈ S。例如，IsSome (@None nat) = False，Some 0 [∈] {0,1,2}。opaque 用于將一個(gè)對(duì)象“不透明化”。例如，opaque 0 : nat，opaque 0 = opaque 1 = opaque 2 = ...，但我們無(wú)法證明?opaque 0 等于某一個(gè)具體的自然數(shù)形式（即 "0",?"1", "2" 這種自然數(shù)的標(biāo)準(zhǔn)形式），也無(wú)法證明 opaque 0 不等于某一個(gè)具體的自然數(shù)形式。

????用 A -> option B 類型的對(duì)象模擬函數(shù)也有其問(wèn)題。例如，設(shè) f : nat -> option nat，則 f 0 < f 1 是不符合語(yǔ)法的，因?yàn)椤?lt;”兩邊的必須都具有類型 nat。為了處理此類問(wèn)題，我們可以定義一些函數(shù)來(lái)實(shí)現(xiàn) A -> B、A -> option B、option A -> option B 類型的轉(zhuǎn)換。

????對(duì)于 f : A -> option B，# f # : option A -> option B，# f # (Some a) = f a，# f # None = None。對(duì)于 f : A -> B，[ f ] : A -> option B，[ f ] a = Some (f a)。對(duì)于 f : A -> option B 和 b : B，f_app f b : A -> B，若 f a = Some x，則 f_app f b a = x，若 f a = None，則 f_app f b a = opaque b。

????現(xiàn)在，我們可以定義函數(shù)的定義域（dom）、值域（ran）、像（f_map）、逆像（f_imap）。

????我們常用“單射”“滿射”“雙射”等詞描述函數(shù)的性質(zhì)，但它們的語(yǔ)法結(jié)構(gòu)不盡相同：“單射”是一元謂詞，是函數(shù)本身的屬性；而“滿射”“雙射”都是三元謂詞，是針對(duì)一個(gè)函數(shù)和兩個(gè)集合而言的（因此“某函數(shù)是滿射的”是不合理的表述，除非上下文已明確針對(duì)的集合）。它們的定義與基本定理如下：

????對(duì)于集合 S 和 T，我們定義“函數(shù)空間 S T”（在數(shù)學(xué)上通常記為??或?）為所有【定義域?yàn)?S，值域是 T 的子集】的函數(shù)組成的集合。對(duì)于函數(shù) f : A -> option B，f 的函數(shù)圖像是所有滿足 f x = Some y 的 (x,y) 組成的集合。