sorting - Coq 中的排序列表

Question

我定义一个排序列表如下:

Require Import Coq.Lists.List.
Import ListNotations.

Inductive SortedList : list nat -> Prop :=
| sort0 : SortedList []
| sort1 : forall a, SortedList [a]
| sort2 : forall z1 z2 l, z1 <= z2 -> SortedList (z2 :: l) -> SortedList (z1 :: z2 :: l).

而且我认为下面的定理是正确的。

Theorem SortedList_sep:
  forall l1 l2,
  SortedList (l1 ++ l2) -> SortedList l1 /\ SortedList l2.

但是我无法证明这个定理。谁能给我一些想法？

Answer 1

这是一种方法。我尽量让它简单易行。

Require Import List.
Import ListNotations.


Inductive SortedList : list nat -> Prop :=
| sort0 : SortedList []
| sort1 : forall a, SortedList [a]
| sort2 : forall z1 z2, forall l, z1 <= z2 -> SortedList (z2 :: l) -> SortedList (z1 :: z2 :: l).


Theorem SortedList_sep1:
  forall l1 l2,
  SortedList (l1 ++ l2) -> SortedList l1.
Proof.
  induction l1;
    firstorder.
  - now constructor.
  - destruct l1.
    now  constructor.
    rewrite <- ?app_comm_cons in *.
    inversion H.
    constructor.
    + now trivial.
    + apply IHl1 with l2.
      rewrite <- ?app_comm_cons in *.
      now trivial.
Qed.

Theorem SortedList_sep2:
  forall l1 l2,
    SortedList (l1 ++ l2) -> SortedList l2.
Proof.
  induction l1;
    firstorder.
  rewrite <- app_comm_cons in *.
  inversion H.
  - apply IHl1.
    rewrite <- H2.
    now constructor.
  - apply IHl1.
    rewrite H1 in H3.
    now apply H3.
Qed.

Theorem SortedList_sep:
  forall l1 l2,
  SortedList (l1 ++ l2) -> SortedList l1 /\ SortedList l2.
Proof.
  firstorder.
  now apply SortedList_sep1 with l2.
  now apply SortedList_sep2 with l1.
Qed.

这里是一个“代码高尔夫”版本，它更短，但不太“容易理解”。

Theorem SortedList_sep:
  forall l1 l2,
  SortedList (l1 ++ l2) -> SortedList l1 /\ SortedList l2.
Proof.
  induction l1; firstorder; try destruct l1; inversion H;
    rewrite <- ?app_comm_cons in *; try constructor; firstorder.
Qed.