Agdaの等価性 - 無関係な引数

Question

私は、値に加えてそのプロパティに関するいくつかの証明からなる依存型を持っています。当然のことながら、このタイプの平等という概念は、価値構成要素の平等と同等であると考えています。これは、この等価性の概念を浮き彫りにしていることを証明するときに問題にぶつかる以外は問題ありません（たとえば、このタイプのリストに対する等価性）。例えば

：

open import Data.Nat 
open import Data.Product 
open import Relation.Binary 
open import Relation.Binary.PropositionalEquality 
open import Relation.Binary.List.Pointwise renaming (Rel to ListRel) hiding (refl) 

module Test where 

    _≈_ : Rel (ℕ × ℕ) _ 
    (a₁ , _) ≈ (a₂ , _) = a₁ ≡ a₂ 

    ≈-sym : Symmetric _≈_ 
    ≈-sym refl = refl 

    ≋-sym : Symmetric (ListRel _≈_) 
    ≋-sym = symmetric ≈-sym 

は、最後の行でAgdaは、ペアのうち第二の突起を解くことができないことを訴えます。興味深いことに、次のイータ等価な式に最後の行を変更することは、それらを解決することができることを意味します

≋-sym = symmetric (λ {x} {y} → ≈-sym {x} {y}) 

は今、当然私は時々Agdaは、すべての暗黙の引数について解くことができないことを知っていると、余分なヘルプのビットを必要としますが、私はこれを行うことで何を提供しているのか新しい情報を理解していません。

私は平等を取り払っています。私はむしろこれらの醜いエタ拡張を私のコードのどこにも追加しないでください。誰かが元のコードに似た何かを渡すことを許可する提案があるのだろうかと思いましたか？

私はirrelevanceを調べましたが、2番目の投影法は、等価性に関して計算上無関係であっても、他の場所で使用されています。

Answer 1

私は推測していますが、暗黙の議論の順序は統一（の一部）の問題ではないと思います。タイプ{m n : ℕ} -> n ≡ m（mがnの前に来る）である

flipped : (({n m : ℕ} -> n ≡ m) -> ℕ) -> ({m n : ℕ} -> n ≡ m) -> ℕ 
flipped k f = k f 

ここ k

タイプ{n m : ℕ} -> n ≡ mの何かを受け取り、f考えてみますが、それぞれの暗黙の引数は推敲中にメタ変数になり、メタ情報が発注されていないので、Agdaは喜んで、これら2つの式を統一（例えば、αをβ -> βにインスタンス化することができず、βからαというインスタンスが生成され、α ≡ α -> αという結果となり、そのようなループ（equirecursive型と呼ばれる）を処理することは悪夢ではありません。それは

≋-sym = symmetric (λ {x} {y} → ≈-sym {x} {y}) 
≋-sym = symmetric (λ {x} {y} → ≈-sym {y} {x}) 

（第2式が悪い型付けされているためだけでなく、なく、かなり、しかし、Agdaは後戻りしないとのいずれかを意味する可能性があるためですから、書くとき

≋-sym = symmetric ≈-sym 

Agdaは、混乱していますflippedが明示的nとmが使用される方法を指定するので、

0の統一これは、 flipped例と異なっている）、従って

をこのような問題を解決することができません

{n1 m1 : ℕ} -> n1 ≡ m1 
{m2 n2 : ℕ} -> n2 ≡ m2 

の結果はn1 ≡ n2,m1 ≡ m2となり、問題は解決される。この仕様を落とすと

unsolved : (({n m : ℕ} -> ℕ) -> ℕ) -> ({m n : ℕ} -> ℕ) -> ℕ 
unsolved k f = k f 

あなたは未解決のメタが戻ってきます。

あなたの定義の正確な問題は、ペアの最初の投影が_≈_のRHSに記載されているだけなので、Agdaは2番目の投影を統一する方法を知らないということです。

record Sing {α} {A : Set α} (x : A) : Set where 

module Test where 

    _≈_ : Rel (ℕ × ℕ) _ 
    (a₁ , b₁) ≈ (a₂ , b₂) = a₁ ≡ a₂ × Sing (b₁ , b₂) 

    ≈-sym : Symmetric _≈_ 
    ≈-sym (refl , _) = (refl , _) 

    ≋-sym : Symmetric (ListRel _≈_) 
    ≋-sym = symmetric ≈-sym 

Singを自動的に推測することができる唯一の住民を持っているダミーの記録である：ここでは、回避策です。しかし、Singは、b₁とb₂のRHSが_≈_であることを推論に適した方法で言及することができ、それによってこれらのメタデータは解読可能となる。

でも、(a₁ , b₁) ≈ (a₂ , b₂) = a₁ ≡ a₂ × Sing b₁はすでに≋-symでメタを解決する方法について十分なヒントをAgdaに与えているようです。徹底した答えを

pattern refl₁ = (refl , _) 

≈-sym : Symmetric _≈_ 
≈-sym refl₁ = refl₁