Agda rewrite не меняет цели в _*_ доказательстве коммутативности

Question

РЕШЕНО: У меня есть решение после следования совету белого волка. Если вы заинтересованы в моем решении, не стесняйтесь сообщать мне.

---

Я пытаюсь написать доказательство в Агде для коммутативности для умножения:

lem3 : (x y : ℕ) → (x * y) ≡ (y * x)
lem3 0 y rewrite pr3a y = refl
lem3 (suc x) y rewrite lem3 x y | pr3b x y = refl

где мы имеем:

pr3a : (x : ℕ) → (x * 0) ≡ 0
pr3a 0 = refl
pr3a (suc x) with (x * 0) | pr3a x
... | .0 | refl = refl

pr3b : (x y : ℕ) →  y + y * x ≡ y * suc x
pr3b 0 0 = refl
pr3b 0 (suc y) rewrite pr3b 0 y = refl
pr3b (suc x) y = {!!}

У меня проблемы с подачей этой конечной цели. Ожидаемый тип y + y * suc x ≡ y * suc (suc x)и я ожидал, что с помощью rewrite дал бы мне y * suc (suc x) ≡ y * suc (suc x) как цель. Тем не мение:

pr3b (suc x) y rewrite pr3b x y = {!!}

ожидает той же цели, что и раньше: y + y * suc x ≡ y * suc (suc x),

Насколько я понимаю, что rewrite будет эффективно заменить RHS в LHS для х = х, давая y * suc x ≡ y * suc xи затем используйте x = suc x, чтобы дать y * suc (suc x) ≡ y * suc (suc x), Я неправильно понимаю, как rewrite работает или я сделал какую-то другую ошибку?

Answer 1

Ваша цель y + y * suc x ≡ y * suc (suc x), Ваша индукционная гипотеза y + y * x ≡ y * suc x, Я могу проверить это, поставив pr3b x y внутри цели и набрав Cc C-.

Goal: y + y * suc x ≡ y * suc (suc x)
Have: y + y * x ≡ y * suc x

Это означает, что с перезаписью вы сможете заменить y * suc x с y * x, Тем не менее, вы видите, что обе стороны поменялись местами, поэтому вы должны переписать с симметрией так

pr3b : (x y : ℕ) →  y + y * x ≡ y * suc x
pr3b 0 0 = refl
pr3b 0 (suc y) rewrite pr3b 0 y = refl
pr3b (suc x) y rewrite sym $ pr3b x y = {!!}

Это способствует достижению цели y + (y + y * x) ≡ y * suc (suc x), Это конкретное доказательство требует завершения ассоциативности и коммутативности.

редактировать

Я думаю, что вы должны попытаться доказать это путем индукции на y вместо x,