Coq тактика сортировки списка?

Question

Для доказательства я хочу использовать тот факт, что для любого списка целых чисел существует отсортированная версия этого списка.Это кажется очевидным для меня, но я не мог найти тактику, которая делает что-то подобное.Я пытался создать свой собственный (ниже), но я застрял, поэтому, возможно, этот факт не так очевиден, как я думал (или, может быть, это даже не правда?)

Definition sorted := (StronglySorted (λ x y, x ≤ y)).
Lemma exists_sorted:  ∀ (L : list Z) (a : Z), ∃ L0 : list Z, sorted L0 ∧ (List.In a L ⇔ List.In a L0).
Proof.
  induction L.
  - intros.
    exists nil.
    split.
    + apply SSorted_nil.
    + tauto.
  - intros.
    pose proof (IHL a).
    destruct H as [L0 [H H0]].

иоттуда моя идея кажется немного круглой.Любой совет?

Answer 1

Резюме:

Require Import Orders Sorting ZArith.

Module ZOrder <: TotalLeBool.
Definition t := Z.
Definition leb := Z.leb.
Lemma leb_total : forall x y : t, leb x y = true \/ leb y x = true.
Proof.
intros x y; case (Zle_bool_total x y); auto.
Qed.

End ZOrder.

Module ZSort := Sort ZOrder.

Lemma Transitive_Zle_bool : Transitive (fun x y => is_true (x <=? y)%Z).
Proof.
intros x y z; unfold is_true; rewrite <- 3!Zle_is_le_bool; apply Z.le_trans.
Qed.

Lemma exists_sorted:  forall (L : list Z), exists L0 : list Z, 
 StronglySorted (fun x y => is_true (x <=? y)%Z) L0 /\ 
 (forall a: Z, List.In a L <-> List.In a L0).
Proof.
intros l; exists (ZSort.sort l).
split;[apply ZSort.StronglySorted_sort; apply Transitive_Zle_bool | ].
intros a; split; apply Permutation.Permutation_in.
  apply ZSort.Permuted_sort.
apply Permutation.Permutation_sym; apply ZSort.Permuted_sort.
Qed.

Это вопрос навигации по библиотекам Coq. Я не знаю, как вы пришли к понятию StronglySorted, но оно действительно присутствует в библиотеках, поставляемых с системой Coq.

Если вы введете только следующее

Require Import Sorted ZArith.

Тогда вы получите только определение того, что означает сортировка списка, но не определение функции сортировки. Вы видите это, потому что команда

Search StronglySorted.

возвращает только полдюжины теорем, которые в основном связаны с отношением между StronglySorted и Sorted и принципом индукции для StronglySorted.

Используя git grep в источниках дистрибутива Coq, я понял, что концепция StronglySorted использовалась в двух библиотеках, вторая называется Mergesort. Ага! сортировка слиянием - это имя алгоритма, поэтому он, вероятно, построит отсортированный список для нас. Теперь оба Mergesort Sorted включены в Sorting, так что это библиотека, которую мы буду использовать.

Require Import Sorting ZArith.

Теперь, если я наберу Search StronglySorted., я вижу, что к результатам добавляется новая теорема с именем NatSort.StronglySorted_sort. Сюжет утолщается. Утверждение этой теоремы длинное, но в основном оно выражает то, что если отношение, вычисляемое функцией Nat.leb, является транзитивным, то функция NatSort.sort действительно возвращает отсортированный список.

Ну, нам нужна не функция сортировки натуральных чисел, а функция сортировки целых чисел типа Z. Но если вы изучите файл Mergesort.v, вы увидите, что NatSort является экземпляром функтора в структуре, которая описывает функцию сравнения для натуральных чисел и доказательство того, что это сравнение всего в определенном смысле. Таким образом, нам нужно только создать такую ​​же структуру для целых чисел.

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

Теперь, это только частично удовлетворительный ответ, потому что StronglySorted (fun x y => (x <=? y)%Z) не совпадает с вашим sorted. Это показывает нам, что в библиотеке отсутствует лемма, выражающая StronglySorted R1 <-> StronglySorted R2, когда R1 и R2 эквивалентны.

Дополнение: чтобы получить утверждение с правильным соотношением в StronglySorted, вам нужно что-то близкое к следующему доказательству. Лемма StronglySorted_impl должна быть предусмотрена и в модуле Sorted, на мой взгляд.

Lemma StronglySorted_impl {A : Type} (R1 R2 : A -> A -> Prop) (l : list A) :
  (forall x y, List.In x l -> List.In y l -> R1 x y -> R2 x y) ->
  StronglySorted R1 l -> StronglySorted R2 l.
Proof.
intros imp sl; revert imp; induction sl as [ | a l sl IHsl Fl];
  intros imp; constructor.
  now apply IHsl; intros x y xin yin; apply imp; simpl; right.
clear IHsl sl; revert imp; induction Fl; auto.
constructor;[now apply imp; simpl; auto | ].
apply IHFl.
intros y z yin zin; apply imp; simpl in yin, zin.
  now destruct yin as [ ya | yin]; simpl; auto.
now destruct zin as [za | zin]; simpl; auto.
Qed.

Lemma exists_sorted':  forall (L : list Z), exists L0 : list Z, 
 StronglySorted (fun x y => (x <= y)%Z) L0 /\ 
 (forall a: Z, List.In a L <-> List.In a L0).
Proof.
intros L; destruct (exists_sorted L) as [L' [sl permP]].
exists L'; split; [ | exact permP].
apply (StronglySorted_impl (fun x y => is_true (x <=? y)%Z)); auto.
now intros x y _ _; apply Zle_bool_imp_le.
Qed.

Answer 2

На самом деле выбор порядка не так тривиален в конструктивной теории типов, если вы разрешите Z быть любым типом.Я рекомендую вам взглянуть на Коэла Кирилла (и других) finmap библиотека , в частности, учитывая тип T с принципом выбора и решаемым равенством, он точно делает то, что вы хотите, то естьскажем, для получения канонического порядка для любого списка T.

В частности, см. функцию сортировки здесь

Definition f (s : seq K) := choose (perm_eq (undup s)) (undup s).

, где

choose : forall T : choiceType, pred T -> T -> T

- это принцип выбора, undup удаляет дубликаты и perm_eq равенство с точностью до перестановки.

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

From mathcomp Require Import all_ssreflect all_algebra.

Open Scope ring_scope.
Import Num.Theory.

Lemma exists_sorted (N : realDomainType) (l : seq N) :
  exists l_sorted, sorted <=%R l_sorted /\ perm_eq l_sorted l.
Proof.
exists (sort <=%R l).
by split; [apply: (sort_sorted (@ler_total _))|apply/perm_eqlP/perm_sort].
Qed.

Definition exists_sorted_int := exists_sorted [realDomainType of int].

Фактически, вся теорема избыточна, так как вам лучше примитивной теорией.