Unzureichend bewerteter Kontext innerhalb der 'with'-Klausel

Question

Ich stecke auf dem folgenden Beweis fest.

module Temp where

   open import Data.Empty
   open import Data.Fin hiding (compare)
   open import Data.Nat hiding (compare); open import Data.Nat.Properties
   open import Function
   open import Level
   open import Relation.Binary
   open import Relation.Binary.PropositionalEquality

Ich arbeite mit natürlichen Zahlen Γ, die als Kontexte ausgelegt sind, ein de Bruijn-Indizes und die Verwendung von Elementen von Fin Γ als Identifikatoren.(Für die Zwecke meiner Frage muss man diese nicht als Kontexte und Bezeichner verstehen, aber es kann bei der Intuition helfen.)

Eine Umbenennung ist ein Kontextmorphismus:

   Ren : Rel ℕ Level.zero
   Ren Γ Γ′ = Fin Γ → Fin Γ′

Ich definiere jetzt die folgenden zwei sehr einfachen Operationen.Der erste, close-var, ergibt eine Umbenennung, die einen Namen aus dem Kontext entfernt und ihn einem vorhandenen Namen im verbleibenden Kontext zuordnet.Zweiten, open-var, ergibt eine Umbenennung, die das Gegenteil bewirkt und an einer bestimmten Stelle einen neuen Namen in den Kontext einfügt.Um einen Einfüge- oder Löschpunkt im Kontext zu finden, vergleiche ich weiter toℕ, da ich noch nicht verstanden habe, wie man es benutzt Data.Fin.compare.

   open StrictTotalOrder strictTotalOrder
   open DecTotalOrder decTotalOrder renaming (refl to ≤-refl; trans to ≤-trans)
   open import Data.Fin.Props using (bounded)

   close-var : ∀ {Γ} → Fin Γ → Fin (suc Γ) → Fin (suc Γ) → Fin Γ
   close-var _ y z with compare (toℕ y) (toℕ z)
   close-var _ _ zero | tri< () _ _
   close-var _ _ (suc z) | tri< _ _ _ = z
   close-var x _ _ | tri≈ _ _ _ = x
   close-var _ zero _ | tri> _ _ ()
   close-var _ (suc y) z | tri> _ _ z<suc-y = 
      fromℕ≤ (≤-trans z<suc-y (bounded y))

   open-var : ∀ {Γ} → Fin (suc Γ) → Fin Γ → Fin (suc Γ)
   open-var y z with compare (toℕ y) (toℕ z)
   ... | tri< _ _ _ = suc z
   ... | tri≈ _ _ _ = suc z
   ... | tri> _ _ _ = inject₁ z

Der einzige nicht triviale Teil dieser Definitionen ist der letzte Fall von close-var was sich von einem größeren Kontext in einen kleineren zwingen muss.

Für feste Argumente werden die Umbenennungen von erhalten close-var und open-var bilden Sie einen Isomorphismus (ich bin mir ziemlich sicher).Ich bin jedoch nicht in der Lage, die folgenden Ziele zu verstehen:

   close∘open≡id : ∀ {Γ} (x : Fin Γ) (y : Fin (suc Γ)) (z : Fin Γ) → 
                   (close-var x y ∘ open-var y) z ≡ z
   close∘open≡id _ y z with compare (toℕ y) (toℕ z)
   close∘open≡id _ y z | tri< _ _ _ with compare (toℕ y) (suc (toℕ z))
   close∘open≡id _ _ _ | tri< _ _ _ | tri< _ _ _ = refl
   close∘open≡id _ _ _ | tri< y<z _ _ | tri≈ y≮suc-z _ _ = 
      ⊥-elim (y≮suc-z (≤-step y<z))
   close∘open≡id _ _ _ | tri< y<z _ _ | tri> y≮suc-z _ _ = 
      ⊥-elim (y≮suc-z (≤-step y<z))
   close∘open≡id _ y z | tri≈ _ _ _ with compare (toℕ y) (suc (toℕ z))
   close∘open≡id _ _ _ | tri≈ _ _ _ | tri< _ _ _ = refl
   close∘open≡id _ _ _ | tri≈ _ y≡z _ | tri≈ y≮suc-z _ _ rewrite y≡z = 
      ⊥-elim (y≮suc-z ≤-refl)
   close∘open≡id _ _ _ | tri≈ _ y≡z _ | tri> y≮suc-z _ _ = {!!}
   close∘open≡id _ y z | tri> _ _ _ with compare (toℕ y) (toℕ (inject₁ z))
   close∘open≡id _ _ _ | tri> _ _ _ | tri< _ _ _ = {!!}
   close∘open≡id _ _ _ | tri> _ _ _ | tri≈ _ _ _ = {!!}
   close∘open≡id _ _ _ | tri> _ _ _ | tri> _ _ _ = {!!}

Der erste Fall sollte unmöglich sein, aber ich scheine nicht in der Lage zu sein zu verwenden y≡z und y≮suc-z um einen Widerspruch abzuleiten, wie ich es im unmittelbar vorhergehenden Fall getan habe.Ich denke, das liegt daran, dass das Muster selbst absurd ist, aber ich weiß nicht, wie ich Agda davon überzeugen soll.

Ein zweites, und vielleicht verwandtes Problem ist, dass es nicht so aussieht, als ob unter den vier verbleibenden Zielen genügend Reduktionen stattgefunden haben.Sie alle enthalten with muster wie tri< .a .¬b .¬c.Aber ich habe das Verschachtelte erwartet with klauseln, um eine ausreichende Ausführung zu ermöglichen, um diese zu beseitigen.Was mache ich falsch?

(Als Plausibilitätsprüfung ist es einfach zu überprüfen:

   sub : ∀ {Γ} (x : Fin Γ) (y : Fin (suc Γ)) → Ren Γ Γ
   sub x y = close-var x y ∘ open-var y

   Γ : ℕ
   Γ = 5

   ρ : Ren Γ Γ
   ρ = sub (suc (zero)) (suc (suc (suc zero)))

   ex₁ : ρ zero ≡ zero
   ex₁ = refl

   ex₂ : ρ (suc zero) ≡ suc zero
   ex₂ = refl

   ex₃ : ρ (suc (suc (zero))) ≡ suc (suc zero)
   ex₃ = refl

   ex₄ : ρ (suc (suc (suc (zero)))) ≡ suc (suc (suc zero))
   ex₄ = refl

und so weiter.)

Answer 1

Verschachtelten with klauseln sind in Ordnung.Das Problem ist, dass in der Definition von close-var, Sie passen nicht nur auf das Ergebnis von compare (toℕ y) (toℕ z), sondern auch auf die Argumente y und z untereinander.Und natürlich kann Agda nichts reduzieren, ohne sicher zu sein, welche Funktionsgleichung zu verwenden ist.

Im zweiten Loch, close-var sollte das Muster mit übereinstimmen inject₁ z, aber du tust es nicht (und kannst es nicht).Sie müssen auch darüber abstrahieren und dann Muster genug übereinstimmen, um Agda davon zu überzeugen, dass es sicher eine Gleichung wählen kann.

close∘open≡id x y z | tri> _ _ _
  with inject₁ z | compare (toℕ y) (toℕ (inject₁ z))
... | tri> _ _ _ | Fin.zero  | tri< () _ _
... | tri> _ _ _ | Fin.suc r | tri< _  _ _ = {!!}  -- goal is r ≡ z

---

Was das erste Loch betrifft - wenn der obige Code nicht hilft, beweisen Sie einfach ein einfaches Lemma:

≡→≤ : {x y : ℕ} → x ≡ y → x ≤ y
≡→≤ refl = ≤-refl

Und dann können Sie Widerspruch ableiten über:

y≮suc-z (s≤s (≡→≤ y≡z))

(Ich habe nicht in die StrictTotalOrder aufzeichnungen, aber die Chancen stehen gut, dass dieses Lemma bereits vorhanden ist).