Блог

Я пытаюсь доказать некоторые леммы, которые являются взаимно рекурсивными, но , к сожалению, не являются структурно рекурсивными, поэтому мне приходится использовать Data.Nat.Induction.Acc , в результате чего половина моего кода посвящена явному упоминанию доказательств таких фактов, как m ≤ m ⊔ n . В идеале я хотел бы как можно больше скрыть эти технические детали, и на первый взгляд неявные аргументы кажутся многообещающими (и гораздо более легкими, чем полное метапрограммирование/размышление). Но, увы, я застрял на этом пути.

В качестве модельного примера рассмотрим некоторые взаимно рекурсивные деревья:

 open import Data.Nat.Base
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; sym)

mutual
  data U : Set where
    U-only    : U
    U-with-Vs : (v₁ v₂ : V) → U
  
  data V : Set where
    V-only    : V
    V-with-Us : (u₁ u₂ : U) -> V
 

наряду с некоторыми функциями, дающими что-то меньшее (для очевидного определения размера), но не структурно меньшее:

 mutual
  iso-U : U → V
  iso-U U-only = V-only
  iso-U (U-with-Vs v₁ v₂) = V-with-Us (iso-V v₁) (iso-V v₂)

  iso-V : V → U
  iso-V V-only = U-only
  iso-V (V-with-Us u₁ u₂) = U-with-Vs (iso-U u₁) (iso-U u₂)
 

Теперь давайте определим эти очевидные меры размера и докажем, что iso это не меняет этот размер:

 mutual
  size-U : U → ℕ
  size-U U-only = zero
  size-U (U-with-Vs v₁ v₂) = suc (size-V v₁ ⊔ size-V v₂)

  size-V : V → ℕ
  size-V V-only = zero
  size-V (V-with-Us u₁ u₂) = suc (size-U u₁ ⊔ size-U u₂)

mutual
  size-U-iso-V : ∀ v
               → size-U (iso-V v) ≡ size-V v
  size-U-iso-V V-only = refl
  size-U-iso-V (V-with-Us u₁ u₂) rewrite size-V-iso-U u₁ | size-V-iso-U u₂ = refl

  size-V-iso-U : ∀ u
               → size-V (iso-U u) ≡ size-U u
  size-V-iso-U U-only = refl
  size-V-iso-U (U-with-Vs v₁ v₂) rewrite size-U-iso-V v₁ | size-U-iso-V v₂ = refl
 

Наконец мы напишем бессмысленную и бесполезную функцию, которая все еще моделирует то, что мне нужно делать в моем реальном коде:

 open import Data.Nat.Induction

module Explicit where
  mutual
    count-U : (u : U) → Acc _<_ (size-U u) → ℕ
    count-U U-only _ = zero
    count-U (U-with-Vs v₁ v₂) (acc rec) =
      let ineq = m≤m⊔n (size-V v₁) (size-V v₂)
          ineq' = subst (_≤ size-V v₁ ⊔ size-V v₂) (sym (size-U-iso-V v₁)) ineq
          r₁ = rec _ (s≤s ineq')
          r₂ = rec _ (s≤s (n≤m⊔n _ _))
       in suc (count-U (iso-V v₁) r₁   count-V v₂ r₂)

    count-V : (v : V) → Acc _<_ (size-V v) → ℕ
    count-V V-only _ = zero
    count-V (V-with-Us u₁ u₂) (acc rec) =
      let r₁ = rec _ (s≤s (m≤m⊔n _ _))
          r₂ = rec _ (s≤s (n≤m⊔n _ _))
       in suc (count-U u₁ r₁   count-U u₂ r₂)
 

This typechecks, but all those r₁ s, r₂ s and whatever they require in count-U are completely irrelevant to the logic of these functions, and I’d like to get rid of them.

Let’s give it a shot with instance arguments? Here’s my attempt:

 module Instance where
  instance
    m≤m⊔n' : ∀ {m n} → m ≤ m ⊔ n
    m≤m⊔n' {m} {n} = m≤m⊔n m n

    n≤m⊔n' : ∀ {m n} → n ≤ m ⊔ n
    n≤m⊔n' {m} {n} = n≤m⊔n m n

    acc-rec : ∀ {a z} → ⦃ Acc _<_ z ⦄ → ⦃ a < z ⦄ → Acc _<_ a
    acc-rec ⦃ acc rec ⦄ ⦃ a<z ⦄ = rec _ a<z
  
  mutual
    count-U : (u : U) → ⦃ Acc _<_ (size-U u) ⦄ → ℕ
    count-U U-only = zero
    count-U (U-with-Vs v₁ v₂) = suc ({! !}   count-V v₂)

    count-V : (v : V) → ⦃ Acc _<_ (size-V v) ⦄ → ℕ
    count-V V-only = zero
    count-V (V-with-Us u₁ u₂) = {! !}
 

Агде это не нравится, хотя, по-видимому, она рассматривает аргумент экземпляра в count-U качестве кандидата и не уверена, какую из двух лемм собирается ⊔ использовать:

 Failed to solve the following constraints:
  Resolve instance argument
    _124
      : (v₃ v₄ : V) ⦃ z : Acc _<_ (size-U (U-with-Vs v₃ v₄)) ⦄ →
        size-V v₄ < _z_122 (v₁ = v₃) (v₂ = v₄)
  Candidates
    λ {m} {n} → m≤m⊔n m n : ({m n : ℕ} → m ≤ m ⊔ n)
    λ {m} {n} → n≤m⊔n m n : ({m n : ℕ} → n ≤ m ⊔ n)
  Resolve instance argument
    _123
      : (v₃ v₄ : V) ⦃ z : Acc _<_ (size-U (U-with-Vs v₃ v₄)) ⦄ →
        Acc _<_ (_z_122 (v₁ = v₃) (v₂ = v₄))
  Candidates
    _ : Acc _<_ (size-U (U-with-Vs v₁ v₂))
    acc-rec : ({a z : ℕ} ⦃ _ : Acc _<_ z ⦄ ⦃ _ : a < z ⦄ → Acc _<_ a)
 

И даже если я оставлю только один экземпляр верхнего уровня предположительно правильной формы

     acc-rec : ∀ {m n} → ⦃ Acc _<_ (suc (m ⊔ n)) ⦄ → Acc _<_ n
    acc-rec ⦃ acc rec ⦄ = rec _ (s≤s (n≤m⊔n _ _))
 

Агда все равно будет жаловаться.

Я несколько раз перечитывал раздел о разрешении экземпляров в документах Agda, но я все еще не уверен, почему он ведет себя таким образом.

Что я делаю не так? Могу ли я добиться желаемого с помощью аргументов экземпляра? Или мне просто пойти и научиться метапрограммированию Agda?