coq - 在 Coq 中解决合并排序拆分证明

Question

我目前正在编写 Software Foundations 教科书 Verified Functional Algorithm 的第 3 卷，但我一直坚持一个练习的证明。

您可以在此处找到我目前正在处理的有关 Mergesort 的章节：https ://softwarefoundations.cis.upenn.edu/vfa-current/Merge.html

到目前为止，这是我被困的地方：

(** **** Exercise: 3 stars, standard (split_perm)  *)

(** Here's another fact about [split] that we will find useful later on.  
*)

Lemma split_perm : forall {X:Type} (l l1 l2: list X),
    split l = (l1,l2) -> Permutation l (l1 ++ l2).
Proof.
  induction l as [| x | x1 x2 l1' IHl'] using list_ind2; intros.
- inv H. simpl. reflexivity.
- inv H. simpl. reflexivity.
- inv H. 

这是我最后一个策略“inv H”的结果。

1 subgoal
X : Type
x1, x2 : X
l1' : list X
IHl' : forall l1 l2 : list X, split l1' = (l1, l2) -> Permutation l1' (l1 ++ l2)
l1, l2 : list X
H1 : (let (l1, l2) := split l1' in (x1 :: l1, x2 :: l2)) = (l1, l2)
______________________________________(1/1)
Permutation (x1 :: x2 :: l1') (l1 ++ l2)

关于我应该如何继续证明我的目标的任何线索？Permutation (x1 :: x2 :: l1') (l1 ++ l2)

Answer 1

我认为第一步是摆脱split l'，destruct (split l')然后倒置H1应该简化你的目标