Как доказать в Coq утверждения о заданных множествах

Как одно доказательство утверждения, как следующее в COQ.

Require Import Vector.
Import VectorNotations.
Require Import Fin.

Definition v:=[1;2;3;4;5;6;7;8].
Lemma L: forall (x: Fin.t 8), (nth v x) > 0.

Или, скажем, у вас есть заданный список чисел, и вы хотите доказать, что ни один номер не появляется дважды в этом списке.

Возможно, нужно написать алгоритм с леммой в качестве типа. Но я понятия не имею, как это сделать.

Кстати, это не домашнее задание.

2 ответа

Вот быстрое и грязное доказательство:

Proof.
Require Import Program.
dependent destruction x.
auto.
dependent destruction x.
compute.
auto.
dependent destruction x.
compute.
auto.
dependent destruction x.
compute.
auto.
dependent destruction x.
compute.
auto.
dependent destruction x.
compute.
auto 10.
dependent destruction x.
compute.
auto 10.
dependent destruction x.
compute.
auto 10.
dependent destruction x.
Qed.

Мы используем dependent destruction тактика от Program модуль. Это основывается на аксиоме JMeq, но это не должно быть проблемой.

Позвольте мне предложить решение с использованием библиотеки math-comp:

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
From mathcomp Require Import fintype tuple.

Definition v := [tuple of [:: 1;2;3;4;5;6;7;8]].

Lemma L : forall x, tnth v x > 0.
Proof. exact/all_tnthP. Qed.

all_tnthP лемма заменит ваш предикат его вычислимой версией, что, в свою очередь, заставит Coq проверить, что все элементы в кортеже больше 0, завершив доказательство.

Другие вопросы по тегам