Gleichheit in Agda - irrelevante Argumente

Question

Ich habe einen abhängigen Typ, der aus einem Wert plus einige Beweise über seine Eigenschaften besteht. Natürlich möchte ich, dass meine Vorstellung von Gleichheit über diesen Typ der Gleichheit über die Wertkomponente entspricht. Das ist alles in Ordnung, außer dass ich auf Probleme stoße, wenn ich Eigenschaften von aufgehobenen Begriffen dieser Gleichheit (zum Beispiel Gleichheit über Listen dieses Typs) beweise.

Zum Beispiel:

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 

In der letzten Zeile beschwert Agda, dass es nicht für die zweiten Vorsprünge aus der paarweise lösen kann. Interessanterweise ist die letzte Zeile Wechsel in den folgenden eta-äquivalenter Ausdruck bedeutet, dass sie sie lösen kann:

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

Jetzt natürlich weiß ich, dass manchmal Agda nicht für alle impliziten Argumente lösen kann und ein bisschen mehr Hilfe braucht aber Ich verstehe nicht, welche neuen Informationen ich mir dabei biete ...

Ich mache eine Menge Gleichstellung und vermeide es, diese hässlichen Eta-Erweiterungen überall in meinem Code hinzuzufügen. Ich habe mich gefragt, ob jemand irgendwelche Vorschläge hat, etwas Ähnliches dem ursprünglichen Code zu erlauben, zu bestehen?

Ich habe in irrelevance untersucht, aber die zweite Projektion wird an anderer Stelle verwendet, auch wenn es rechnerisch irrelevant für die Gleichheit ist.

Answer 1

Ich rate, aber ich denke, das Problem ist, dass die Reihenfolge der impliziten Argumente keine Rolle spielt für (ein Teil der) Vereinheitlichung. Betrachten

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

Hier k erhält etwas vom Typ {n m : ℕ} -> n ≡ m und f vom Typ {m n : ℕ} -> n ≡ m (m kommt vor n), aber Agda vereint glücklich, diese beiden Ausdrücke, da jedes implizite Argument eine Metavariable während Ausarbeitung wird und metas sind nicht geordnet bis sie eingeführt wurden - sie sind nach ihrer Instanziierung sortiert (z. B. können Sie α zu β -> β und dann β zu α instanziieren, da dies α ≡ α -> α ergeben würde und die Behandlung solcher Schleifen (equirecursive-Typen genannt) ein ungesunder Albtraum ist). Also, wenn Sie

≋-sym = symmetric ≈-sym 

Agda schreiben sind verwirrt, weil es jeden

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

bedeuten könnte (na ja, nicht ganz, denn der zweite Ausdruck ist schlecht getippt, aber Agda nicht Rückzieher und Dies unterscheidet sich von dem flipped Beispiel können solche Probleme nicht deshalb)

lösen, weil flipped explizit angibt, wie n und m verwendet werden, so Vereinigung von

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

Ergebnisse in n1 ≡ n2 und m1 ≡ m2 und damit das Problem gelöst ist. Wenn Sie diese Spezifikation

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

fallen lassen, werden Sie ungelöste Metas zurück erhalten.

Das genaue Problem mit Ihrer Definition ist, dass nur die ersten Projektionen von Paaren in der RHS von _≈_ erwähnt werden, so dass Agda nicht wissen, wie man die zweiten Projektionen vereinheitlicht. Hier ist eine Abhilfe:

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 ist ein Dummy-Datensatz, der nur einen Einwohner haben, die automatisch geschlossen werden kann. Aber Sing erlaubt b₁ und b₂ in der RHS von _≈_ in einer inferenzfreundlichen Weise zu erwähnen, die diese Metas in ≋-sym lösbar macht.

Obwohl es scheint, dass (a₁ , b₁) ≈ (a₂ , b₂) = a₁ ≡ a₂ × Sing b₁ gibt schon Agda genug Hinweise, wie Metas in ≋-sym zu lösen.

Sie können auch ein Muster Synonym definieren den Code etwas schöner zu machen:

pattern refl₁ = (refl , _) 

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