Coq中split_perm引理证明受阻求助（软件基础VFA归并排序章节）

证明思路 #

你当前的证明差两步就能串起来，核心是把手里的归纳假设用透，再配合置换的传递性即可：

1. 你已经拆分得到 split l1' = (l, l0)，这个条件正好可以触发归纳假设IHl'，直接拿到l1'和l ++ l0的置换关系
2. 给上面的置换关系两边都加上x2，得到x2 :: l1'和x2 :: (l ++ l0)的置换关系
3. 用Permutation_cons_app可以直接证明x2 :: (l ++ l0)和l ++ x2 :: l0是置换的，最后用置换的传递性把两步拼起来就完成目标了

对应Coq代码步骤 #

你在当前证明状态下依次执行以下策略即可：

(* 实例化归纳假设，直接拿到l1'和l ++ l0的置换关系 *)
specialize (IHl' l l0 eq_refl).
(* 用置换传递性，中间过渡态选x2 :: (l ++ l0) *)
apply Permutation_trans with (l' := x2 :: (l ++ l0)).
- (* 证明x2::l1' 和 x2::(l++l0) 置换，直接给置换关系加头元素即可 *)
  apply perm_skip.
  exact IHl'.
- (* 直接用现成的cons_app置换引理 *)
  apply Permutation_cons_app.

内容的提问来源于stack exchange，提问作者John Regis