相合的异质平等

我试图用异质平等，以证明涉及此索引的数据类型声明：相合的异质平等

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

我能够使用Relation.Binary.HeterogenousEquality.≅推理给我写的证明，但只通过假定下面的一致性属性：

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′ = {!!}

然而，我不能k≅k′是refl不脱离类型检查得到以下错误消息模式匹配：

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

并且如果我试图对k≅k′进行案例分析。通过使用C-c C-c从Emacs的前端），以确保所有的隐含参数是否正确相对于由refl强加自己的约束相匹配，我得到

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′]

（如果你有兴趣，这里有一些不相关背景：Eliminating subst to prove equality）

来源

2012-02-16 Cactus

作为一种解决方法，我目前使用的是参数化类型而不是索引化类型，并且携带了一个证明： '数据计数器（n：ℕ）：设置其中切割：（ij：ℕ）→（i + j + 1 = n：suc（i + j）≡n）→计数器n' – Cactus 2012-02-17 13:43:06

你可以做的是采取额外的证明，这两个指数都是平等的：

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′是否可以统一时，你会得到这个错误。

由于Counter n正好有ñ元素，它实际上可以证明Counter是射使用像鸽巢原理（和土黄也许可判定的平等），所以你可以不n ≅ n′说法做，尽管这会是乱。

编辑：AFAICT the Het。平等行为依然如此。

来源

2012-02-18 06:33:31 Saizan

相合的异质平等

回答

相关问题