Coq引理select_perm'证明求助：该引理的最优证明启动方式是什么？

由于select是基于列表结构递归定义的函数，该引理的最优启动方式是对列表参数做结构归纳，具体启动步骤如下：

• 第一步：引入前两个全称参数，对列表l执行结构归纳，再引入剩余参数与等式假设，保证归纳假设的全称强度足够覆盖两种递归分支的需求：

intros x l; induction l as [| h t IH]; intros y r H.

• 第二步：处理空列表基准分支
  对空列表的情况，直接化简select x []可得(x, []) = (y, r)，注入等式后目标退化为自反的置换关系，直接调用reflexivity即可证明：

- simpl in H; injection H as -> ->; reflexivity.

• 第三步：处理非空列表的归纳分支
  此时目标中的select x (h::t)会自动展开为两个布尔分支的匹配结构，直接对x <=? h做布尔情况拆分，再对递归调用的返回值做解构即可用上归纳假设：

- simpl in H; destruct (x <=? h) eqn:E.
  + destruct (select x t) as [j l'] eqn:Sel; inversion H; subst.
    (* 此时可直接应用归纳假设IH得到Permutation (x::t) (j::l')，再结合Permutation_cons扩展即可得到目标 *)
  + destruct (select h t) as [j l'] eqn:Sel; inversion H; subst.
    (* 此时将归纳假设IH中的x替换为h即可得到对应递归调用的置换性质，再配合Permutation_swap等标准库引理即可拼接出目标 *)

后续证明只需调用Coq标准库Coq.Sorting.Permutation中已有的基础置换引理即可完成，不需要额外证明辅助引理。

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