#coq
#coq
Вопрос:
У меня есть список натуральных чисел. После сокращения одного элемента из списка я хочу доказать следующее соотношение.
Theorem reduce_elements:forall (n:nat) (l:list nat),
(length (n :: l) =? 0) = false->
(length l =? 0) = false.
Ответ №1:
Это утверждение не выполняется:
Require Import Coq.Arith.Arith.
Theorem reduce_elements:forall (n:nat) (l:list nat),
(length (n :: l) =? 0) = false->
(length l =? 0) = false.
Admitted.
Goal False.
pose proof (reduce_elements 0 nil eq_refl).
simpl in H.
congruence.
Qed.
Я заметил, что вы несколько раз обращались к Stack Overflow с просьбой помочь доказать ложные утверждения. Я предлагаю вам попробовать набросать эти доказательства на бумаге, прежде чем пытаться решить их с помощью Coq: это поможет вам лучше понять вашу проблему.
Комментарии:
1. Я пытаюсь закрыть оператор false, вставив правильный оператор. Например, a<=b (я знаю, что это какое-то ложное утверждение). Правильное утверждение — b<=a . На основе противоречия, как их связать? Один из способов — доказать a> b. Какой-нибудь другой способ, который может быть полезен в этой ситуации?