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

Question

Как доказать в 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

coq dependent-type induction

Источник

user4430564 19 дек '15 в 19:39

2 ответа

Другие вопросы по тегам coq dependent-type induction

user495796 21 дек '15 в 13:08 2015-12-21 13:08 · Answer 1 · 2015-12-21 13:08

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

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, но это не должно быть проблемой.

user1955696 26 фев '16 в 00:42 2016-02-26 00:42 · Answer 2 · 2016-02-26 00:42

Позвольте мне предложить решение с использованием библиотеки 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, завершив доказательство.