Для использования reflexivity, я должен как-то преобразовать n + 1 в (S n).Coq: Как заменить термины «n + 1» на «S n»?
Это должно быть довольно простая трансформация, но я не знаю, как сказать Coq сделать это.
Как это сделать?
Поскольку они не равны, просто эквивалентны, вы можете использовать replace (n + 1) with (S n), который попросит вас подтвердить этот факт. Или вы можете использовать rewrite с правильной леммой из std lib, которая равна add_1_r iirc.
Как бы доказать, что 0 + (S j) = (S j) тогда? – user111854
Это нужно доказывать непосредственно с помощью 'reflexivity': определение' + 'выполняется путем рекурсии по первому аргументу, поэтому здесь Coq знает, как упростить' 0 + foobar' в 'foobar' без перезаписи. Проблема с вашим первоначальным вопросом заключается в том, что вы хотели переписать 'n + 1', а не' 1 + n'. Чтобы доказать, что '1 + n' равно' S n', вам не нужно ничего делать, это точно определение. – Vinz
Возможный дубликат [Как я могу переписать «+ 1» (плюс один) на «S» (succ) в Coq?] (Http://stackoverflow.com/questions/40313702/how-can-i-rewrite -1-plus-one-to-s-succ-in-coq) – gallais
'1 + n' равно« S n »по нормализации, поэтому, если у вас есть лемма, доказывающая коммутативность сложения, вы можете пойти' n + 1' => '1 + n' =>' S n'. – Cactus