Список натуральных чисел в coq

Question

У меня есть список натуральных чисел, элементы в списке расположены в порядке убывания. Я хочу написать лемму о списке, что первый элемент h больше, чем все элементы списка. Пусть список есть [h; h1; t]. 0 h1? Пожалуйста, объясните мне, как написать h больше, чем все элементы в конце списка.

Answer 1

До express, что заданный список натуральных чисел находится в порядке убывания, вы можете использовать существующие функции в модуле List Coq.

Require Import List Lia.

Definition desc (l : list nat) : Prop :=
  forall i j, i <= j -> nth j l 0 <= nth i l 0.

Что я сделал? Я только что выразил, что значение в ранге i должно быть больше, чем значение в ранге j для любого j больше, чем i. Это умно в тонком смысле. Выражение nth j l 0 фактически представляет значение в ранге i в l, если i меньше длины списка или 0 в противном случае . Бывает, что 0 меньше любого другого натурального числа, поэтому это определение работает. Если бы вместо этого вы запросили список чисел в строго в порядке убывания , то мне пришлось бы написать более точное определение, включающее только ранги, которые меньше длины списка (вы можете использовать функцию length за это). Я позволю вам сделать это в качестве упражнения.

Когда вы пишете логический предикат, такой как desc, важно проверить это определение, чтобы убедиться, что вы действительно захватили понятие ты имел в виду. Чтобы проверить мое собственное определение, я написал следующий код:

Definition sample1 := 1 :: 2 :: 3 :: nil.

Definition sample2 := map (fun x => 10 - x) sample1.

Lemma s2_desc : desc sample2.
Proof.
intros [ | [ | [ | [ | ]]]] [ | [ | [ | [ | ]]]];
  intros ilej; simpl; lia.
Qed.

Lemma s1_n_desc : ~desc sample1.
Proof.
intros abs; generalize (abs 0 1 (le_S _ _ (le_n _))).
  compute; lia.
Qed.

Доказательство s2_desc является доказательством грубой силы, оно фактически проверяет все пары рангов, меньших 4, и проверяет это во всех в этих случаях сравнения между натуральными числами (рангами или значениями в списке) дают логически доказуемые формулы.

Доказательство s1_n_desc используется для проверки того, что мое определение desc действительно отвергает список, который явно не удовлетворяет критерию. Хорошо, что я написал это доказательство, потому что оно помогло мне обнаружить ошибку в моем коде desc, которая не была обнаружена предыдущим доказательством: я написал nth 0 l i вместо nth i l 0!

Последнее, но не менее важное, мое решение начинается с Require Import List Lia. Это означает, что мы используем два существующих модуля Coq. Первый предоставляет часто используемые функции для списков, второй предоставляет автоматизированный инструмент c для выполнения простых доказательств сравнения чисел (фактически, натуральных чисел или целых чисел).

В качестве следующего шага можно также напишите логическую функцию, которая точно вычисляет значение true, когда ее ввод находится в порядке убывания, и разработайте доказательства тестов для проверки того, что обе функции ведут себя соответственно.

Answer 2

Вам нужно определить, что вы подразумеваете под descending, и использовать это в своем доказательстве. У @Yves есть, пожалуй, самый лучший способ сделать это. Вот еще одно определение, которое просто записывает простое индуктивное определение. Список нисходящий, если хвост нисходящий, а первый элемент больше или равен второму элементу.

Одна приятная вещь с индуктивными определениями состоит в том, что вы можете выполнять индукцию по ним, что дает вам много информации в каждом случае доказательства, с очень небольшой работой.

Require Import List.

Inductive descending : list nat -> Prop :=
  desc_nil : descending nil
| desc_1 n : descending (cons n nil)
| desc_hd n m l :
    m <= n ->
    descending (cons m l) ->
    descending (cons n (cons m l)).

Lemma head_gt l d:
  descending l -> forall m, In m l -> m <= hd d l.
Proof.
  induction 1; intros k H'.
  now exfalso; apply in_nil in H'.
  now replace k with n; [ | inversion H'].
  now inversion H';
    [ subst; apply le_n
    | eapply PeanoNat.Nat.le_trans; auto].
Qed.

Answer 3

Вам нужно сказать

Для любого натурального числа и любого списка, например h::t, если список нисходящий и число находится в хвосте, то оно меньше головы.

Таким образом, на языке Coq вы можете написать

Lemma head_is_max : forall n h t, desc (h::t) -> In n t -> h >= n.

, если des c является логическим предикатом, который вы можете написать

Lemma head_is_max : forall n h t, desc (h::t) = true -> In n t -> h >= n.

Выполнение индукции на t будет работать для доказательства.

---

Более изощренным способом вы можете использовать предикат в списке, который утверждает, что все элементы списка имеют заданное свойство c, которое вы можете определить это как

Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop :=
  match l with
    | [] => True
    | h :: t => P h /\ All P t
  end.

Так что All P l означает P x для всех x s в l. Теперь мы можем написать упомянутую лемму как

Lemma head_is_max : forall h t, desc (h::t) -> All (fun n => h >= n) t.