14

最初のいくつかの退屈なインポート:

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)

ここで、たとえば Naturals によって索引付けされた型があるとします。

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 (m + n)) -> foo m n x ≅ x
bar m n x = {! ?0 !}

バーでの目標は

Goal: (foo m n x | n + m | .Data.Nat.Properties.+-comm n m) ≅ x
————————————————————————————————————————————————————————————
x : Foo (m + n)
n : ℕ
m : ℕ

これら|はゴールで何をしていますか？そして、どうすればこのタイプの用語を構築し始めることができるでしょうか?

この場合、手動で を使用して置換を行うことで問題を回避できますがsubst、大きな型や方程式の場合、これは非常に見苦しく退屈になります。

foo' : (m n : ℕ) -> Foo (m + n) -> Foo (n + m)
foo' m n x = PE.subst Foo (+-comm m n) x

bar' : (m n : ℕ) (x : Foo (m + n)) -> foo' m n x ≅ x
bar' m n x = HE.≡-subst-removable Foo (+-comm m n) x
4

1 に答える 1

13

これらのパイプは、問題の式の結果が出るまでリダクションが中断されていることを示しており、通常は、先withに進むために結果を知る必要があるブロックがあったという事実に要約されます。これは、rewrite構造with体が問題の式の に展開され、それを機能させるために必要な補助値があれば、その後に が一致するためreflです。

+-comm n mこの場合、withブロック内にパターン マッチを導入する必要があることを意味するだけですrefl(そして、それが示唆するように、おそらくスコープにも持ち込む必要がn + mあるため、等式には何か話があります)。Agda の評価モデルは非常に単純であり、何かをパターン マッチした場合 (レコードの偽のパターン マッチを除く)、同じものをパターン マッチするまで減少しません。私があなたのために概説したことをするだけなので、あなたの証明で同じ式で書き直すことさえできるかもしれません。

より正確には、次のように定義すると:

f : ...
f with a | b | c
...  | someDataConstructor | boundButNonConstructorVariable | someRecordConstructor = ...

を式として参照するfと、式aのみで観察したパイプが得られます。これは on に一致するためですsomeDataConstructor。したがって、少なくとも削減するには、導入してから一致fさせる必要があります。一方、andは同じ with ブロックで導入されましたが、評価を停止しません。これは、パターン マッチが行われないためです。また、 は eta を持つレコード型であるため、静的に唯一可能なコンストラクターであることがわかっています。asomeDataConstructorbcbcsomeRecordConstructor

于 2012-09-19T18:46:23.057 に答える