Using "rewrite" inside non-top-level goal requires auxiliary function?

Question

I have an Agda formalisation of pi-calculus with de Bruijn indices. Most of the setup is irrelevant to my problem, so I'll use empty types for renamings Ren and actions, and simply postulate a basic renaming sucᴿ, plus some useful operations and properties of renamings.

module Concur where

   open import Relation.Binary.PropositionalEquality
   -- de Bruijn indices:
   open import Data.Fin using () renaming (Fin to Name; module Fin to Name)
   open import Data.Nat as Nat using () renaming (ℕ to Cxt; module ℕ to Cxt)

   -- empty types will do here
   data Ren : Cxt → Cxt → Set where
   data Action (Γ : Cxt) : Set where

   postulate
      _∘_ : ∀ {Γ₁ Γ₂ Γ₃} → Ren Γ₂ Γ₃ → Ren Γ₁ Γ₂ → Ren Γ₁ Γ₃
      -- push a renaming under a binder
      suc : ∀ {Γ Γ′} → Ren Γ Γ′ → Ren (Cxt.suc Γ) (Cxt.suc Γ′)
      -- successor function on ℕ, qua renaming
      sucᴿ : ∀ {Γ} → Ren Γ (Cxt.suc Γ)
      -- apply a renaming to an action
      _*ᴬ_ : ∀ {Γ Γ′} → Ren Γ Γ′ → Action Γ → Action Γ′
      -- here's a useful property
      suc-comm : ∀ {Γ Γ′} (ρ : Ren Γ Γ′) (a : Action Γ) → 
                 suc ρ *ᴬ (sucᴿ *ᴬ a) ≡ sucᴿ *ᴬ (ρ *ᴬ a)

Now I'll define processes, transitions and the application of a renaming to process, but limiting myself just to two kinds of process and a single kind of transition.

   data Proc (Γ : Cxt) : Set where
      Ο : Proc Γ
      ν_ : Proc (Cxt.suc Γ) → Proc Γ

   data _—[_]→_ {Γ} : Proc Γ → Action Γ → Proc Γ → Set where
      ν_ : ∀ {P R} {a : Action Γ} → P —[ sucᴿ *ᴬ a ]→ R → ν P —[ a ]→ ν R

   infixl 0 _—[_]→_

   -- Apply a renaming to a process.
   _*_ : ∀ {Γ Γ′} → Ren Γ Γ′ → Proc Γ → Proc Γ′
   ρ * Ο = Ο
   ρ * (ν P) = ν (suc ρ * P)

Here's my problem. I want to use my useful property suc-comm to show that I can lift an arbitrary renaming ρ to a transition. In the ν-binder case, this involves recursing into the sub-transition E, using suc to push the renaming under the binder, and the suc-comm lemma to show that things commute in the right way.

   -- A transition survives an arbitrary renaming.
   _*¹_ : ∀ {Γ Γ′ P R} {a : Action Γ} (ρ : Ren Γ Γ′) →
          P —[ a ]→ R → ρ * P —[ ρ *ᴬ a ]→ ρ * R
   ρ *¹ (ν_ {a = a} E) rewrite sym (suc-comm ρ a) =
      ν {!suc ρ *¹ E!} -- rewriting here doesn't help

Unfortunately, and as indicated above, using rewrite to apply the lemma doesn't help because the goal isn't of a suitable type until I'm inside the ν. But I can only apply rewrite at the top level of a function body. So I seem to need an auxiliary function, so that I can rewrite in the correct context:

   _*²_ : ∀ {Γ Γ′ P R} {a : Action Γ} (ρ : Ren Γ Γ′) →
          P —[ a ]→ R → ρ * P —[ ρ *ᴬ a ]→ ρ * R
   aux : ∀ {Γ Γ′ P R} (a : Action Γ) (ρ : Ren Γ Γ′) →
         P —[ sucᴿ *ᴬ a ]→ R → suc ρ * P —[ sucᴿ *ᴬ (ρ *ᴬ a) ]→ suc ρ * R
   ρ *² (ν_ {a = a} E) = ν aux a ρ E
   aux a ρ E rewrite sym (suc-comm ρ a) = suc ρ *² E

Indeed this works, but it seems a bit awkward. Am I missing a trick here? Is there a way to avoid the auxiliary function, and somehow make use of the lemma inside the earlier goal?

Well, you could always do it explicitly using subst. You don't need auxiliary function, but it is no less awkward, I'm afraid. — Vitus

user3237465 user3237465 · Accepted Answer · 2014-07-21T08:29:06

You could inline rewrite, but it's still awkward:

 _*¹_ : ∀ {Γ Γ′ P R} {a : Action Γ} (ρ : Ren Γ Γ′) →
        P —[ a ]→ R → ρ * P —[ ρ *ᴬ a ]→ ρ * R
 ρ *¹ (ν_ {a = a} E) with suc ρ *ᴬ (sucᴿ *ᴬ a) | suc-comm ρ a | suc ρ *¹ E
 ... | ._ | refl | E' = ν E'

Or introduce suc ρ *¹ E first and then rewrite:

 _*¹_ : ∀ {Γ Γ′ P R} {a : Action Γ} (ρ : Ren Γ Γ′) →
        P —[ a ]→ R → ρ * P —[ ρ *ᴬ a ]→ ρ * R
 ρ *¹ (ν_ {a = a} E) with suc ρ *¹ E
 ... | E' rewrite suc-comm ρ a = ν E'

Using "rewrite" inside non-top-level goal requires auxiliary function?

1 Answers