Я пытаюсь доказать коммутативность agda. Я попытался изучить стандартную библиотеку, но есть много сложных вещей, которые я не мог понять. Я так пробовал -
comm : (a b : Q) -> (a + b) === (b + a)
проблема здесь в +, который не определен над Q в библиотеке. Разве мы не можем доказать это, не указав + над Q. Пожалуйста, помогите мне.
Вы не можете доказать это, не определив сначала +.
Если вы запутались при изучении стандартной библиотеки, я предлагаю вам сначала попытаться доказать что-то более простое, чтобы лучше познакомиться с Agda, прежде чем заниматься этим.
Конечно, вы не можете доказать коммутативность неопределенной функции _+_; в качестве глупого контрпримера, ожидаете ли вы, что сумеете доказать (a - b) == (b - a)? Если нет, то почему? _-_ на данном этапе является такой же неопределенной функцией, как и _+_; просто у него другое название ...
Обратите внимание, что вы можете определить сложение для ℚ, используя математику начальной школы:
n ÷ p + m ÷ q = (n * q + m * p) ÷ (p * q)
и упростив его, разделив как n * q + m * p, так и p * q их НОД. Я уже объяснил детали этого последнего шага в этом ответе.
