Agda: Почему я не могу найти совпадение с образцом по ссылке?

Я пытаюсь доказать что-то о делимости целых чисел. Сначала я попытался доказать, что делимость рефлексивна.

∣-refl : ∀{n} → n ∣ n

Потому что я определил делимость на основе вычитания ...

data _∣_ : ℤ → ℤ → Set where
  0∣d : ∀{d} → zero ∣ d
  n-d∣d : ∀{n d} → (n - d) ∣ d → n ∣ d

... это кажется простым, если я использую тот факт, что n-n=0:

∣-refl {n} with n-n≡0 n 
... | refl = n-d∣d 0∣d

Но Agda отказывается от сопоставления с образцом по исх. Даже если не существует другой нормальной формы n-n=0 n. Я доказал это с помощью другой функции. Мне просто нужно использовать тот факт, что n-n=0.

C:\Users\ebolnme\Desktop\agda\Integers.agda:118,7-11
n + neg n != zero of type ℤ
when checking that the pattern refl has type n + neg n ≡ zero

Примечания:

  • a - b определяется a + (neg b)
  • Я уже доказал n-n≡0 : (n : ℤ) → n - n ≡ zero

pattern-matching agda
person Boldizsár Németh    schedule 19.12.2013    source источник

Ответы (1)


arrow_upward
7
arrow_downward

Доказательство равенства не о чем говорить. Когда вы выполняете сопоставление с образцом в конструкторе, он может уточнить другие аргументы (и их типы). В вашем случае n-n≡0 n должен уточнить n - n, но такого выражения нет, и Agda выдает вам это (немного озадачивающее) сообщение об ошибке.

Вы можете исправить это, введя выражение в with:

∣-refl : ∀ {n} → n ∣ n
∣-refl {n} with n - n | n-n≡0 n
... | ._ | refl = ?

Мы можем более подробно рассказать о левой части, это хорошо показывает, как происходит уточнение:

∣-refl {n} with n - n | n-n≡0 n
∣-refl {n} | .zero | refl = ?

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

∣-refl {n} with n - n | n-n≡0 n
∣-refl {n} | .zero | refl = n-d∣d 0∣d

Проверка типов снова не согласна. Почему это так? n-d∣d должен иметь тип (n - n) ∣ n → n ∣ n, а 0∣d - тип 0 ∣ n. Но ждать! Разве мы не только что показали, что n - n на самом деле 0?

Проблема с сопоставлением с образцом и его уточнением заключается в том, что это происходит только один раз, правая часть не будет затронута вообще (это, кстати, одна из причин, по которой у нас есть inspect механизм). Как мы с этим справляемся?

Есть функция под названием subst, которая принимает что-то типа P a, доказательство того, что a ≡ b и дает нам P b. Обратите внимание: если мы заменим λ x → x ∣ n на P, zero на a и n - n на b, мы получим функцию, которая принимает zero ∣ n и дает нам n - n ∣ n (для подходящего доказательства, конечно).

И действительно:

∣-refl {n} = n-d∣d (subst (λ x → x ∣ n) (sym (n-n≡0 n)) 0∣d)

Это определение принято: тип subst ... 0∣d - n - n ∣ n, что подходит для ввода n-d∣d. Обратите внимание, что нам также нужно доказательство того, что zero ≡ n - n, но у нас есть n - n ≡ zero - здесь мы используем тот факт, что ≡ является симметричным (sym).

Для полноты, вот определение subst:

subst : ∀ {a p} {A : Set a} (P : A → Set p) {x y} →
  x ≡ y → P x → P y
subst _ refl p = p
person Vitus    schedule 19.12.2013
comment
Спасибо за полный ответ. Для меня основные моменты: 1) Вы можете найти соответствие по образцу в refl только в том случае, если есть выражение, равенство которого доказано. 2) Вы теряете информацию при сопоставлении, и можно использовать замену, чтобы избежать этого. Кстати, я заменил определение делимости на data _divides_ (d : ℤ) : ℤ → Set where div : ∀{k n} → k * d ≡ n → d divides n. Это лучше для моих целей, и о доказательствах легче писать. - person Boldizsár Németh; 20.12.2013
comment
@ BoldizsárNémeth: Отлично! В стандартной библиотеке есть целый модуль о делимости. Если вам нужно вдохновение или просто сравнение с вашим кодом, проверьте _ 1_. - person Vitus; 20.12.2013