#coq
Вопрос:
Следующая гипотеза может быть полезна для достижения цели? Простая инверсия H2 не работает.
H1:f1 (length (a :: l))=0.
H2: false = true ->
f1 (length (a :: l))=0.
Комментарии:
1. Было бы полезно, если бы вы разместили окно своих целей: в нем должно быть написано что-то вроде
1 subgoal, <your hypotheses here> ,_________<long horizontal line>_______(1/1),<your goal here>. Прямо сейчас мне не ясно, каковы ваши гипотезы и что вы пытаетесь доказать.2. Опубликуйте свой код: все, что необходимо для вопроса, включая все определения, цель, которую вы хотите доказать, и ваши доказательства до сих пор. То, что вы разместили здесь, само по себе не имеет смысла. Все, что я могу сказать, — это то, что гипотеза формы
false = true -> …никоим образом вам не поможет.
Ответ №1:
H2 является типом функции, а не индуктивным типом. Инверсию можно выполнять только на индуктивных типах.
Кроме того, вы H2 бесполезны, так как его можно использовать только в том случае, если у вас есть доказательство false = true (в этом случае вы уже можете доказать любую теорему, которую хотите).