异质平等的一致性

Question

我正在尝试使用异构相等来证明涉及此索引数据类型的语句:

data Counter : ? ? Set where
  cut : (i j : ?) ? Counter (suc i + j)

我能够使用Relation.Binary.HeterogenousEquality.≅-Reasoning编写我的证明,但只能假设以下同余属性:

Counter-cong : ? {n n?} {k : Counter n} {k? : Counter n?} ?
               {A : ? ? Set} ? (f : ?{n} ? Counter n ? A n) ?
               k ? k? ? f k ? f k?
Counter-cong f k?k? = {!!}

然而,我不能模式匹配Relation.Binary.HeterogenousEquality.?-Reasoning是k?k?没有得到从类型检查以下错误消息:

Refuse to solve heterogeneous constraint 
    k : Counter n =?= k? : Counter n?

如果我尝试做一个案例分析refl(即通过使用k?k?Emacs前端)来确保所有隐式参数都与它们施加的约束相匹配C-c C-c,我得到

Cannot decide whether there should be a case for the constructor
refl, since the unification gets stuck on unifying the 
inferred indices 
    [{.Level.zero}, {Counter n}, k] 
with the expected indices 
    [{.Level.zero}, {Counter n?}, k?]

(如果你有兴趣,这里有一些不相关的背景:消除subst来证明平等)

Answer 1

您可以做的是获取两个指数相等的额外证据:

Counter-cong : ? {n n?} {k : Counter n} {k? : Counter n?} ?
               {A : ? ? Set} ? (f : ?{n} ? Counter n ? A n) ?
               n ? n? ? k ? k? ? f k ? f k?
Counter-cong f refl refl = refl

最初的问题是知道Counter n ? Counter n?并不意味着n ? n?因为类型构造函数不被认为是单射的(有一个标志--injective-type-constructors,实际上这使得匹配通过,但它已知与被排除的中间不一致),所以虽然它可以结论是两个类型相同就不会重写n到n?,所以你得到这个错误,当它后来检查k和k?是unifiable.

由于Counter n只有n个元素,实际上可以证明Counter是使用类似于鸽子原则(并且可能是自然的可判定的相等)的内射,因此你可以不用n ? n?参数来做,尽管那会很混乱.

编辑:AFAICT Het.平等行为仍然是一样的.