5

[0, ..., n-1]mod-nカウンターを、間隔を2つの部分に分割したものとして表現しようとしています。

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

これを使用すると、2つの重要な操作を定義するのは簡単です（簡潔にするためにいくつかの証明は省略されています）。

_+1 : ∀ {n} → Counter n → Counter n
cut i zero    +1 = subst Counter {!!} (cut zero i)
cut i (suc j) +1 = subst Counter {!!} (cut (suc i) j)

_-1 : ∀ {n} → Counter n → Counter n
cut zero    j -1 = subst Counter {!!} (cut j zero)
cut (suc i) j -1 = subst Counter {!!} (cut i (suc j))

+1問題は、それ-1が逆であることを証明しようとするときに発生します。subst導入されたこれらのエリミネーターが必要な状況に遭遇し続けます。

subst-elim : {A : Set} → {B : A → Set} → {x x′ : A} → {x=x′ : x ≡ x′} → {y : B x} → subst B x=x′ y ≡ y
subst-elim {A} {B} {x} {.x} {refl} = refl

しかし、これは（ある程度）論点先取であることが判明しました：それはタイプチェッカーによって受け入れられません、なぜならsubst B x=x' y : B x'そしてy : B x...

4

1 に答える 1

5

stdlib から Relation.Binary.HeterogeneousEquality を使用する場合、subst-elim のタイプを指定できます。ただし、with または rewrite 節で x ≡ x' の最終的な証明に対してパターン マッチを行うだけなので、明示的なエリミネータを作成する必要がなく、入力の問題もありません。

于 2012-02-13T21:07:27.497 に答える