Почему `sym` необходимо использовать в этом случае при использовании` rewriting`? - PullRequest
Новая
       9

Почему `sym` необходимо использовать в этом случае при использовании` rewriting`?

0 голосов
/ 09 февраля 2020

Учитывая определение натуральных чисел по Пеано: 

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

Мы можем различными способами доказать свойство ∀ (m : ℕ) → zero + m ≡ m + zero.

Например: 

comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) =
  begin
    zero + suc n
  ≡⟨⟩
    zero + suc (zero + n)
  ≡⟨⟩
    suc (zero + n)
  ≡⟨ cong suc (comm-+₀ n) ⟩
    suc (n + zero)
  ≡⟨⟩
    suc n + zero
  ∎

И более компактно: 

comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) = cong suc (comm-+₀ n)

Если мы хотим, мы можем даже использовать rewrite и для go cong: 

comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) rewrite comm-+₀ n = refl

Но подождите! Это не работает Agda скажет нам, что выражение неверно, потому что не может доказать следующее: 

suc (n + 0) ≡ suc (n + 0 + 0)

Если мы представим Agda симметричное переписывание свойства, sym (comm-+₀ n), оно выполнит проверку без ошибок.

Итак, мой вопрос: зачем нам sym в этом случае? Доказательство прекрасно работало без других стратегий. Работает ли перезапись одновременно на обеих сторонах, а не только на левой?

1 Ответ

2 голосов
/ 11 февраля 2020

В каждом случае цель, когда m имеет форму suc n, равна: 

suc n ≡ suc (n + 0)

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

cong suc (comm-+₀ n)

Однако при использовании rewrite с равенством a ≡ b вы напрямую изменяете цель, заменяя все вхождения из a на b В вашем случае использование rewrite для количества comm-+₀ n, тип которого n ≡ n + 0, приводит к замене каждого вхождения n на n + 0, превращая таким образом цель с 

suc n ≡ suc (n + 0)

на 

suc (n + 0) ≡ suc (n + 0 + 0)

это не то, что вы хотите сделать. Поскольку перезапись заменяет все вхождения с левой стороны на правую, обратное равенство с использованием sym заменит вместо этого единственное вхождение n + 0 на n, таким образом преобразуя цель из 

suc n ≡ suc (n + 0)

в 

suc n ≡ suc n

, что является вашим ожидаемым поведением и позволяет вам завершить использование refl напрямую. Это объясняет, почему вам нужно использовать sym.

Подводя итог:

  • rewrite напрямую взаимодействует с типом цели.
  • rewrite переписывает слева направо.
  • rewrite переписывает все случаи, которые он находит в типе цели.

Подробнее о rewrite можно найти здесь:

https://agda.readthedocs.io/en/v2.6.0.1/language/with-abstraction.html#with -запись

...