Блог

У меня есть следующее:

 open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma
open import Agda.Primitive

_×_ : {n m : Level} (A : Set n) (B : Set m) → Set (n ⊔ m)
X × Y = Σ X (λ _ → Y)

ℕ² : Set
ℕ² = ℕ × ℕ 

canonical : ℕ² → ℕ²
canonical (x , 0) = (x , 0)
canonical (0 , y) = (0 , y)
canonical (suc x , suc y) = canonical (x , y)

p1 : (a : ℕ) → (a , 0) ≡ canonical (a , 0) -- works
p1 a = refl

p2 : (a : ℕ) → (0 , a) ≡ canonical (0 , a) -- doesn't work
p2 a = refl

p3 : (a : ℕ) → (0 , a) ≡ canonical (0 , a) -- works
p3 0 = refl
p3 (suc a) = refl
 

Когда я пытаюсь ввести проверку, agda выдает ошибку в p2

 zero != fst (canonical (0 , a)) of type ℕ
when checking that the expression refl has type
(0 , a) ≡ canonical (0 , a)
 

Почему Agda требует, чтобы я выполнял сопоставление с образцом для второго элемента пары, как в p3? Почему p1 проверяет тип, но не p2?

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

 canonical xy = case xy of
  (x , y) -> case y of
    zero -> (x , 0)
    suc y -> case x of
      zero -> (0 , suc y)
      suc x -> canonical (x , y)
 

В частности, функция будет вычисляться только тогда, когда известно, что второй аргумент равен или zero или suc . Agda предоставляет мягкое предупреждение, когда это происходит, предоставляя светло-серый фон второму предложению. Вы также можете превратить это в ошибку, включив --exact-split флаг (с {-# OPTIONS --exact-split #-} помощью pragma в верхней части вашего файла.

Если вы хотите узнать больше о переводе в дерево обращений, я рекомендую нашу статью о разработке зависимого сопоставления с образцом. Вас также может заинтересовать возможное решение этой проблемы (которое, к сожалению, не вошло в основную версию Agda) или --rewriting флаг, который позволяет вам добавлять правило вычисления canonical (0 , y) = (0 , y) , сначала проверяя его, а затем регистрируя его как правило перезаписи.