在Coq中修改，使用和应用let表达式

Question

我不确定如何在coq中应用let表达式。这来自PF中的选择排序示例。

一旦定义了选择函数，就证明了这个引理。

Lemma select_perm: forall x l,
  let (y,r) := select x l in
   Permutation (x::l) (y::r).

这些是一些用例，以了解其工作原理。

Compute select_perm  3 [10;32;4;6;5].
     = select_perm 3 [10; 32; 4; 6; 5]
     : let (y, r) := select 3 [10; 32; 4; 6; 5] in
       Permutation [3; 10; 32; 4; 6; 5] (y :: r)

Compute select 3 [10; 32; 4; 6; 5].
  = (3, [10; 32; 4; 6; 5])
       : nat * list nat

我如何进一步评估它以显示实际的排列-类似于Compute ((select_perm 3 [10;32;4;6;5]) (select 3 [10; 32; 4; 6; 5]))的内容？

我不确定在应用以下定理时如何使用该引理。

Lemma selsort_perm:
  forall n,
  forall l, length l = n -> Permutation l (selsort l n).
Proof.
  intros.
  generalize dependent n.
  induction l; intros.
  - subst.
    simpl.
    constructor.
  - subst. simpl.
    destruct (select a l) eqn:?.

有了相应的目标，我想以某种方式应用select_perm（apply (select_perm a l)）。

  a : nat
  l : list nat
  IHl : forall n : nat, length l = n -> Permutation l (selsort l n)
  n : nat
  l0 : list nat
  Heqp : select a l = (n, l0)
  ============================
  Permutation (a :: l) (n :: selsort l0 (length l))

或者，相应地，通过传递性assert (Permutation (a :: l) (n :: l0))证明，并以新的目标以某种方式将以下Heqp引入let表达式中。是否有一种简单的方法来处理coq中的let表达式（如函数应用程序）？

编辑：

我已经通过将select_perm修改为select_perm'找到了一个特别的解决方案

Lemma select_perm': forall x l,
   Permutation (x::l) ((fst (select x l)) :: (snd (select x l))).

并根据列表的长度而不是列表本身进行归纳（如果需要，可以提供该代码），而是宁愿使用Appel的原始定义...

Answer 1

是的，这是一个棘手的问题。这是我建议选择的结构。为了提供一个可行的自我示例，我只假设存在函数select和selsort以及关系Permutation。然后，我实际上在目标中介绍了希望使用的定理的实例，最后销毁了let构造内部的表达式。这是例子。您只对最后两行感兴趣。

Require Import List.

Section playground.

Variable select : nat -> list nat -> nat * list nat.

Variable Permutation : list nat -> list nat -> Prop.

Lemma select_perm: forall x l,
  let (y,r) := select x l in
   Permutation (x::l) (y::r).
Proof.
Admitted.

Variable selsort : list nat -> nat -> list nat.

Lemma goal_at_hand (a : nat) (l : list nat)
  (IHl : forall n : nat, length l = n -> Permutation l (selsort l n))
  (n : nat) (l0 : list nat) (Heqp : select a l = (n, l0)),
  Permutation (a :: l) (n :: selsort l0 (length l)).
Proof.
generalize (select_perm a l).
destruct (select a l) as [y r] eqn:tmp1.

使这个棘手的原因在于Coq使用let ... := ... in ...语法，但这实际上是一个模式匹配的表达式：您需要破坏该表达式以隔离名为y和r的两个部分。