Contesto insufficientemente valutato all'interno del `con la clausola`

Question

Sono bloccato sulla prova seguente.

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

.

Sto lavorando con i numeri naturali γ interpretati come contesti, a indici la de bruijn e utilizzando elementi di Fin Γ come identificatori. (Ai fini della mia domanda non è necessario comprendere questi come contesti e identificatori, ma può aiutare con l'intuizione.)

Una ridenominazione è un morfismo di contesto:

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

.

Ora definisco le seguenti due operazioni molto semplici. Il primo, close-var, produce una ridenominazione che rimuove un nome dal contesto, mappandolo a un nome esistente nel contesto rimanente. Il secondo, open-var, produce una ridenominazione che fa il retro, inserendo un nuovo nome nel contesto in una posizione particolare. Per individuare un punto di inserimento o di cancellazione nel contesto, confronto su toℕ, poiché non ho ancora fatto l'uso di 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

.

L'unica parte non banali di queste definizioni è l'ultimo caso di close-var che deve costringere da un contesto più grande a uno più piccolo.

Per gli argomenti fissi, i Renami ottenuti da close-var e open-var formano un isomorfismo (sono abbastanza sicuro). Comunque sono bloccato con il senso dei seguenti obiettivi:

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

.

Il primo caso dovrebbe essere impossibile, ma sembro non essere in grado di utilizzare y≡z e y≮suc-z per derivare una contraddizione, come ho fatto nel caso immediatamente precedente. Penso che questo sia perché il modello stesso è assurdo, ma non so come convincere AGDA di questo.

Un secondo, e forse correlato, il problema è che non sembra che la riduzione abbastanza sia avvenuta sotto i quattro obiettivi rimanenti. Tutti contengono modelli with come tri< .a .¬b .¬c. Ma mi aspettavo che le clausole di with nidificate permetterecessero abbastanza esecuzione di eliminarli. Cosa sto facendo male?

(Come controllo sanitario, è facile verificare:

   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

.

E così via.)

Answer 1

Le clausole di with annidate sono a posto.Il problema è che nella definizione di close-var, si abbina non solo dal risultato di compare (toℕ y) (toℕ z), ma anche sugli argomenti y e z stessi.E naturalmente, AGDA non può ridurre qualcosa senza essere sicuro quale funzione è un'equazione da usare.

Nel secondo foro, close-var dovrebbe corrispondere modello su inject₁ z, ma non è (e non può).Devi astrarre anche quello e poi il modello corrisponde abbastanza per convincere AGDA che può scegliere in sicurezza un'equazione.

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

.

---

.

Come per il primo foro - se il codice sopra non aiuta, dimostra solo un semplice lemma:

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

.

E poi, puoi ricavare contraddizione tramite:

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

.

(Non ho esaminato i record StrictTotalOrder, ma è probabile che questo lemma sia già lì).