Modifying, working with, and applying let expressions in Coq

I'm not sure how to apply the let expression in coq. This is from the selection sort example in PF.

Once the select function is defined, this lemma is proved.

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

These are some use cases to see how it works.

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

How can I further evaluate this to expose the actual Permutation - something along the lines of Compute ((select_perm 3 [10;32;4;6;5]) (select 3 [10; 32; 4; 6; 5]))?

I'm not sure how to use this lemma in applying the below theorem.

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:?.

With the corresponding goals, I want to apply select_perm somehow (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))

Or, correspondingly, prove via transitivity assert (Permutation (a :: l) (n :: l0)) and somehow bring the following Heqp into a let expression in with the new goal . Is there an easy way to treat let expressions like function application in coq?

Edit:

I have found an adhoc alternative solution by modifying select_perm to select_perm'

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

And inducting over the length of the list rather than the list itself (can provide that code if necessary), but would rather just use Appel's original definition...

Solution

Yes, this is a tricky matter. Here is the structure I propose. To make a workable, self-example, I just assume the existence of functions select and selsort and of the relation Permutation.

I actually introduce in my goal the instance of the theorem that I wish to use (as you suggested), and then I can rewrite with Heqp. The last two lines are where things actually happen.

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).
rewrite Heqp.

What makes this tricky is that Coq uses the let ... := ... in ... syntax, but this is actually a pattern-matching expression: you need the expression to be explicitly an application of the pair constructor for the let expression to transform itself in a simpler form.

The goal you obtain has the following shape, I suppose you need a lemma stating that Permutation is transitive to proceed.

  Permutation (a :: l) (n :: l0) ->
  Permutation (a :: l) (n :: selsort l0 (length l))