Agda中的参数化利用证明

阅读这个答案促使我尝试构建,然后证明多态容器函数的规范形式.施工很简单,但证据证明了这一点.下面是我尝试编写证明的简化版本.

简化版本证明,由于参数性,足够多态的函数不能仅基于参数的选择来改变它们的行为.假设我们有两个参数的函数,一个是固定类型,另一个是参数:

PolyFun : Set ? Set _
PolyFun A = ? {X : Set} ? A ? X ? A

我要证明的财产:

open import Relation.Binary.PropositionalEquality

parametricity : ? {A X Y} ? (f : PolyFun A) ? ? a x y ? f {X} a x ? f {Y} a y
parametricity f a x y = {!!}

这样的陈述是否可以从Agda内部证明？

1> Saizan..：

---

不,在Agda中没有参数化原则(然而![1]).

但是,您可以使用这些组合器来构建相应的自由定理的类型并假设它:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.LightweightFreeTheorems

[1] http://www.cse.chalmers.se/~mouling/share/PresheafModelParametericTT.pdf

---

哦,你在A上没有多态,这使得它变得更难,否则你可能已经[A]成为平等.LFT缺乏身份扩展引理,因此在摘要中您通常只能表明事物是相关的,而不是相等的.对于像Bool这样的具体类型,你可以看到[Bool]实际上是平等的.对于(A:Set0),应该保持一致,假设[A]是相等的,请参阅http://bentnib.org/dtt-parametricity.html