Доказательство коммутативности сложения в Агде - PullRequest
Новая
       12

Доказательство коммутативности сложения в Агде

0 голосов
/ 11 сентября 2018

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

cong : ∀{A B : Set} (f : A → B) {x y : A} (eq : x ≡ y) → f x ≡ f y
cong f refl = refl

plus-assoc : ∀ x {y z} → (x + y) + z ≡ x + (y + z)
plus-assoc zero = refl
plus-assoc (suc x) = cong suc (plus-assoc x)

plus-zero : ∀ x → x + zero ≡ x
plus-zero zero = refl
plus-zero (suc x) rewrite plus-zero x = refl

plus-suc : ∀ x {y} → x + suc y ≡ suc (x + y)
plus-suc zero = refl
plus-suc (suc x) = cong suc (plus-suc x)

plus-comm : ∀ x {y} → x + y ≡ y + x
plus-comm zero = { }0
plus-comm (suc x) = { }1

Цель, которую находит Агда, 

Goal: .y ≡ .y + zero

Это, очевидно, очень похоже на плюс-ноль, но если я не знаю, как переписать с .y.

Вторая цель 

Goal: suc (x + .y) ≡ .y + suc x
——————————————————————————————————————————
.y : Nat
x  : Nat

Если я попробую переписать с plus-suc, то вот так: 

plus-comm (suc x) rewrite plus-suc x = { }1

Я получаю эту ошибку: 

Cannot rewrite by equation of type {y : Nat} →
                               x + suc y ≡ suc (x + y)
when checking that the clause
plus-comm (suc x) rewrite plus-suc x = ? has type
(x : Nat) {y : Nat} → x + y ≡ y + x

Я не могу понять эту ошибку. Есть какие-нибудь подсказки? Я мог бы переписать все это без неявных переменных, поскольку это, кажется, усложняет ситуацию, но мне дали код как есть, и поэтому я хотел бы сохранить его, как есть, если это возможно.

Спасибо!

1 Ответ

0 голосов
/ 11 сентября 2018

Вы можете оставить функции доказательства с y в качестве неявного аргумента, но вам нужно и можете использовать его в определении. 

pcomm : ∀ x {y} → x + y ≡ y + x
pcomm zero {y} = {!!}
pcomm (suc x) {y} = {!!}

Вы также можете указать неявные аргументы при вызове функции, например, pcomm x {y}. В функции отсутствует ключевой аргумент для завершения перезаписи.

Совет: если функция имеет много неявных аргументов, и вам нужно только указать конкретный аргумент, вы можете сделать следующее. 

-- f {C = X}
f : ∀ {A B C : Set} → Set
f {C = C} = C
...