相关疑难解决方法(0)

首先是一些无聊的进口:

import Relation.Binary.PropositionalEquality as PE
import Relation.Binary.HeterogeneousEquality as HE
import Algebra
import Data.Nat
import Data.Nat.Properties
open PE
open HE using (_?_)
open CommutativeSemiring commutativeSemiring using (+-commutativeMonoid)
open CommutativeMonoid +-commutativeMonoid using () renaming (comm to +-comm)

现在假设我有一个索引类型,比如自然.

postulate Foo : ? -> Set

而且我想证明在这种类型上运行的函数有一些相同之处Foo.因为agda不是很聪明,所以这些将是异构的平等.一个简单的例子就是

foo : (m n : ?) -> Foo (m + n) -> Foo (n + m)
foo m n x rewrite +-comm n m = x

bar : (m n : ?) (x : Foo …

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

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 =?= …