Coq: Списки отсортированных списков также сортируются?

Question

Я пытаюсь доказать, что если список (L1 ++ a :: L2), который StronglySorted равен «меньше или равен», означает, что список (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.

И я остался с гипотезы и цели . Есть идеи как закончить доказательство?

Answer 1

Вы можете сначала неформально убедить себя, что эта гипотеза у вас есть (по модулю записи)

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

подразумевает цель

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

так что вы на правильном пути. Вышеуказанное следствие доказывается другой индукцией на L1.

Этот подход оправдан, потому что StronglySorted фактически определяется аналогично двойной индукции: каждый суффикс строго отсортирован (первая индукция), а заголовок меньше, чем другие элементы (вторая индукция для каждого шага первого).