上一篇 LdBeth：NuPRL 中的证明{x:N|2<x<3}–virtual evidence
Constructive proof assistant 有个需求，
千里冰封 你懂吗：dependent type 下的类型推导 (meta variables)
比如 Agda 中
id' : forall (x : Prop) -> x -> x
id' _ x = x
的第一个参数是不参与计算的，就可以写成 implicit argument
id : forall {x : Prop} -> x -> x
id x = x
在用了 implicit argument 以后，id 就是个 polymorphic function。
NuPRL 是如何实现这样的功能的呢。众所周知 universal qualification 是用 dependent function type (Pi type) 实现的。
$\forall x:\mathbb{P}. P(x) == \prod_{x:\mathbb{P}}{P(x)}$
那在不引入 metavariable 的设计下，implicit argument 要如何表示？各位是否还记得 intersection over a family of types? recall 在第一节中出现的
$\forall A : Type, B : A \rightarrow Type, a : A .(\cap x:A.B(x)) \subseteq B(a)$
因而可以有 implicit universal qualification 定义如下
$\forall[x:\mathbb{P}].P(x) == \bigcap_{x:\mathbb{P}}P(x)$
证明 intersection over a family 的要点在于在 [ ] 中的 hidden hypothesis 的 computation content 沒有在 conclusion 中使用到。这样 extract 出来的 program 自然不包含 implicit argument。
这个原则叫做 unhide hypothesis。在上一节中证明 $\{P\} \implies \neg\neg P$ 也是利用这个原则，因为一个返回类型为 Void 的 function 的 computation content 显然是 trivial 的，因此那个证明中 derive 出 $\{P\} \implies P$ 是允许的，因为实际上 P 是个 hidden hypothesis。
这么说有些抽象，用个具体的例子就是 NuPRL 可以证明
$\forall [T:Type]. \forall[P: T \rightarrow \mathbb{P}]. \forall a, b:T. P\; a \lor P\; b\implies \exists x: T.P\; x$
但是不能证明 implicit 版的
$\forall [T:Type]. \forall[P: T \rightarrow \mathbb{P}]. \forall [a, b:T]. P\; a \lor P\; b\implies \exists x: T.P\; x$
原因在哪里呢？非 implicit 版的 witness 是
$\lambda a,b,\%. case\; \%\; of\; inl(\%1) \rightarrow \langle a, \%1 \rangle\; |\; inr(\%2) \rightarrow \langle b, \%2 \rangle$
term a 和 b 出現在了返回的表达式中，也就说明了对应的 hypothesis 的 computation content 使用到了 conclusion 中。而 T 和 P 的 term 并沒有出现在 witness 中，就可以作为实现了 polymorphism 的 implicit argument。 非 implicit 版的 witness 是个合法的接受三个参数的 lambda，而 implicit 版需要的
$\lambda \%. case\; \%\; of\; inl(\%1) \rightarrow \langle a, \%1 \rangle\; |\; inr(\%2) \rightarrow \langle b, \%2 \rangle$
中的 a b 成了 free variable 了。
当然，诚然 Agda 中可以证明使用 implicit argument 的形式，但是使用的时候同样不能 infer 出 implicit 参数。
lemma : ∀{T : Set}{P : T → Set}{a b : T} → P a ⊎ P b → ∃[ x ] P x
lemma {a = a} (inj₁ i) = a , i
lemma {b = b} (inj₂ i) = b , i
neg : Bool → Set
neg true = ⊤
neg false = ⊥
-- 需要提供 metavariable a b 才能 tc
_ : ∃[ x ] neg x
_ = lemma {a = true} {b = false} (inj₁ tt)
当然，在 NuPRL 如果一定要用 implicit universal qualification 证明 $P\; a \lor P\; b\implies \exists x.P\; x$ 还有別的方法，还记得上一篇讲的用于证明 classical proposition 的方法吗？
如果写成
$\forall [T:Type]. \forall[P: T \rightarrow \mathbb{P}]. \forall [a, b:T]. \{P\; a \lor P\; b\implies \exists x: T.P\; x\}$
就可以证啦，具体的证明就给读者作习題了。(bushi