Contexte insuffisamment évalué dans la clause `with`

Question

Je suis bloqué sur la preuve suivante.

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

Je travaille avec des nombres naturels Γ interprétés comme des contextes, à la de Bruijn, et en utilisant des éléments de Fin Γ comme identifiants.(Pour les besoins de ma question, il n'est pas nécessaire de les comprendre comme des contextes et des identifiants, mais cela peut aider à l'intuition.)

Un renommage est un morphisme de contexte :

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

Je définis maintenant les deux opérations très simples suivantes.La première, close-var, produit un renommage qui supprime un nom du contexte, le mappant à un nom existant dans le contexte restant.La deuxième, open-var, produit un changement de nom qui fait l'inverse, en insérant un nouveau nom dans le contexte à un emplacement particulier.Pour localiser un point d'insertion ou de suppression dans le contexte, je compare sur toℕ, car je n'ai pas encore compris comment l'utiliser 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

La seule partie non triviale de ces définitions est le dernier cas de close-var qui doit contraindre un contexte plus large à un contexte plus petit.

Pour les arguments fixes, les renommages obtenus à partir de close-var et open-var former un isomorphisme (j'en suis assez certain).Cependant, je n'arrive pas à donner un sens aux objectifs suivants :

   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> _ _ _ = {!!}

Le premier cas devrait être impossible, mais il me semble incapable d'utiliser y≡z et y≮suc-z pour en tirer une contradiction, comme je l'ai fait dans le cas immédiatement précédent.Je pense que c'est parce que le modèle lui-même est absurde, mais je ne sais pas comment en convaincre Agda.

Un deuxième problème, peut-être lié, est qu'il ne semble pas y avoir suffisamment de réduction pour les quatre objectifs restants.Ils contiennent tous with des modèles tels que tri< .a .¬b .¬c.Mais je m'attendais à l'imbriqué with clauses permettant une exécution suffisante pour les éliminer.Qu'est-ce que je fais mal?

(À titre de contrôle d'intégrité, il est facile de vérifier :

   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

et ainsi de suite.)

Answer 1

Imbriqué with les clauses sont acceptables.Le problème est que dans la définition de close-var, vous correspondez non seulement sur le résultat de compare (toℕ y) (toℕ z), mais aussi sur les arguments y et z eux-mêmes.Et bien sûr, Agda ne peut pas réduire quelque chose sans savoir quelle équation de fonction utiliser.

Dans le deuxième trou, close-var le motif devrait-il correspondre inject₁ z, mais vous ne le faites pas (et ne pouvez pas).Vous devez également faire abstraction de cela, puis faire correspondre suffisamment les modèles pour convaincre Agda qu'il peut choisir une équation en toute sécurité.

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

---

Quant au premier trou, si le code ci-dessus ne vous aide pas, prouvez simplement un lemme simple :

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

Et puis, vous pouvez dériver une contradiction via :

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

(je n'ai pas regardé StrictTotalOrder enregistrements, mais il y a de fortes chances que ce lemme soit déjà là).