Insufficiently evaluated context inside `with` clause

Question

I'm stuck on the following proof.

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

I'm working with natural numbers Γ construed as contexts, a la de Bruijn indices, and using elements of Fin Γ as identifiers. (For the purposes of my question one need not understand these as contexts and identifiers, but it may help with the intuition.)

A renaming is a context morphism:

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

I now define the following two very simple operations. The first, close-var, yields a renaming which removes a name from the context, mapping it to an existing name in the remaining context. The second, open-var, yields a renaming which does the reverse, inserting a new name into the context at a particular location. To locate an insertion or deletion point in the context, I compare on toℕ, as I haven't yet groked how to use 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

The only non-trivial part of these definitions is the last case of close-var which has to coerce from a larger context to a smaller one.

For fixed arguments, the renamings obtained from close-var and open-var form an isomorphism (I'm fairly certain). However I'm stuck making sense of the following goals:

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

The first case should be impossible, but I seem to be unable to use y≡z and y≮suc-z to derive a contradiction, as I did in the immediately preceding case. I think this is because the pattern itself is absurd, but I don't know how to convince Agda of this.

A second, and perhaps related, problem is that it doesn't look like enough reduction has occurred under the four remaining goals. They all contain with patterns such as tri< .a .¬b .¬c. But I was expecting the nested with clauses to permit enough execution to eliminate these. What am I doing wrong?

(As a sanity check, it's easy to verify:

   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

and so forth.)

Answer 1

Nested with clauses are okay. The problem is that in the definition of close-var, you match not only on the result of compare (toℕ y) (toℕ z), but also on the arguments y and z themselves. And of course, Agda cannot reduce something without being sure which function equation to use.

In the second hole, close-var should pattern match on inject₁ z, but you don't (and can't). You have to abstract over that as well and then pattern match enough to convince Agda that it can safely choose one equation.

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

---

As for the first hole - if the code above doesn't help, just prove a simple lemma:

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

And then, you can derive contradiction via:

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

(I didn't look into the StrictTotalOrder records, but chances are that this lemma is already there).