Coq rewriting using lambda arguments

Question

We have a function that inserts an element into a specific index of a list.

Fixpoint inject_into {A} (x : A) (l : list A) (n : nat) : option (list A) :=
  match n, l with
  | 0, _        => Some (x :: l)
  | S k, []     => None
  | S k, h :: t => let kwa := inject_into x t k
                   in match kwa with
                      | None => None
                      | Some l' => Some (h :: l')
                      end
  end.

The following property of the aforementioned function is of relevance to the problem (proof omitted, straightforward induction on l with n not being fixed):

Theorem inject_correct_index : forall A x (l : list A) n,
    n <= length l -> exists l', inject_into x l n = Some l'.forall (A : Type) (x : A) (l : list A) (n : nat),
n <= length l ->
exists l' : list A, inject_into x l n = Some l'

And we have a computational definition of permutations, with iota k being a list of nats [0...k]:

Fixpoint permute {A} (l : list A) : list (list A) :=
  match l with
  | []     => [[]]
  | h :: t => flat_map (
                  fun x => map (
                               fun y => match inject_into h x y with
                                        | None => []
                                        | Some permutations => permutations
                                        end
                             ) (iota (length t))) (permute t)
  end.

The theorem we're trying to prove:

Theorem num_permutations : forall A (l : list A) k,
    length l = k -> length (permute l) = fact k.forall (A : Type) (l : list A) (k : nat),
length l = k -> length (permute l) = fact k

By induction on l we can (eventually) get to following goal:

1 subgoal

  A : Type
  a : A
  l : list A
  k : nat
  IHl : length (permute l) = fact k
  H : length (a :: l) = S k
  H1 : length l = k
  ============================
  length (permute (a :: l)) =
  S (length l) * fact (length l)

If we now simply cbn, the resulting goal is stated as follows:

1 subgoal

  A : Type
  a : A
  l : list A
  k : nat
  IHl : length (permute l) = fact k
  H : length (a :: l) = S k
  H1 : length l = k
  ============================
  length
    (flat_map
       (fun x : list A =>
        map
          (fun y : nat =>
           match inject_into a x y with
           | Some permutations => permutations
           | None => []
           end) (iota (length l))) (permute l)) =
  fact (length l) + length l * fact (length l)

Here I would like to proceed by destruct (inject_into a x y), which is impossible considering x and y are lambda arguments. Please note that we will never get the None branch as a result of the lemma inject_correct_index.

How does one proceed from this proof state? (Please do note that I am not trying to simply complete the proof of the theorem, that's completely irrelevant.)

Answer

There is a way to rewrite under binders: the setoid_rewrite tactic (see §27.3.1 of the Coq Reference manual).

However, direct rewriting under lambdas is not possible without assuming an axiom as powerful as the axiom of functional extensionality (functional_extensionality).

Otherwise, we could have proved:

(* classical example *)
Goal (fun n => n + 0) = (fun n => n).(fun n : nat => n + 0) = (fun n : nat => n)
  Fail setoid_rewrite <- plus_n_O.The command has indeed failed with message:
setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X73==[
         |- Relation_Definitions.relation (nat -> nat)]
         (internal placeholder) {?r}
 ?X74==[(do_subrelation:=Morphisms.do_subrelation)
         |- Morphisms.Proper
              (Morphisms.respectful
                 (Morphisms.pointwise_relation nat eq)
                 (Morphisms.respectful ?r
                    (Basics.flip Basics.impl))) eq]
         (internal placeholder) {?p}
 ?X75==[
         |- Morphisms.ProperProxy ?r
              (fun n : nat => n)]
         (internal placeholder) {?p0}
TYPECLASSES:?X73 ?X74 ?X75
SHELF:||
FUTURE GOALS STACK:?X75 ?X74 ?X73 ?X69||?X58 ?X57 ?X56
?X55 ?X54
(fun n : nat => n + 0) = (fun n : nat => n)
Abort.

See here for more detail.

Nevertheless, if you are willing to accept such axiom, then you can use the approach described by Matthieu Sozeau in this Coq Club post to rewrite under lambdas like so:

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.

Generalizable All Variables.

Instance pointwise_eq_ext {A B : Type} `(sb : subrelation B RB eq)
  : subrelation (pointwise_relation A RB) eq.A, B: Type
RB: relation B
sb: subrelation RB eq
subrelation (pointwise_relation A RB) eq
Proof.A, B: Type
RB: relation B
sb: subrelation RB eq
subrelation (pointwise_relation A RB) eq
  intros f g Hfg.A, B: Type
RB: relation B
sb: subrelation RB eq
f, g: A -> B
Hfg: pointwise_relation A RB f g
f = g apply functional_extensionality.A, B: Type
RB: relation B
sb: subrelation RB eq
f, g: A -> B
Hfg: pointwise_relation A RB f g
forall x : A, f x = g x
  intro x; apply sb, (Hfg x).
Qed.

Goal (fun n => n + 0) = (fun n => n).(fun n : nat => n + 0) = (fun n : nat => n)
  setoid_rewrite <- plus_n_O.(fun n : nat => n) = (fun n : nat => n)
  reflexivity.
Qed.