coq - Coq：排序列表的子列表也排序？

Question

我试图证明，如果一个列表（L1 ++ a :: L2）被“小于或等于”强排序意味着列表（L1 ++ L2）也被排序（因为它只是一个排序列表减去一个元素）。到目前为止我有

Definition sorted := (StronglySorted (λ x y, x ≤ y)).
Lemma sorted_sublist : ∀ (L1 L2 : list Z) (a : Z), 
                      sorted (L1 ++ a :: L2) ⇒ sorted (L1 ++ L2).
Proof.
  intros.
  induction L1.
  - simpl.
    simpl in H.
    apply StronglySorted_inv in H.    
    destruct H.
    exact H.
  - apply StronglySorted_inv in H.
    destruct H.
    apply IHL1 in H.
    apply SSorted_cons.
    exact H.
    fold (L1 ++ L2).
    fold (L1 ++ a :: L2) in H0.

我只剩下 假设和目标了。任何想法如何完成证明？

标签： coq

Answer 1

您可以首先非正式地说服自己您有这个假设（以符号为模）

H0 : Forall (fun y : Z => (a0 <= y)%Z) (L1 ++ a :: L2)

暗示目标

Forall (fun y : Z => (a0 <= y)%Z) (L1 ++ L2)

所以你在正确的道路上。上述含义可以通过对 的另一个归纳来证明L1。

这种方法是合理的，因为StronglySorted实际上通过双重归纳类似地定义：每个后缀都是强排序的（第一次归纳），并且头部小于其他元素（第一步的每个步骤的第二次归纳）。