RewriteUnderLambda.v

(* http://stackoverflow.com/questions/43849824/coq-rewriting-using-lambda-arguments/ *)

Require Import Coq.Lists.List. Import ListNotations.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.
Generalizable All Variables.

Instance subrel_eq_respect {A B : Type} `(sa : subrelation A RA eq)
`(sb : subrelation B eq RB) :
   subrelation eq (respectful RA RB).
Proof. intros. intros f g Hfg. subst. intros a a' Raa'. apply sb.
f_equal. apply (sa _ _ Raa'). Qed.

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

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.

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

Variable iota : nat -> list nat.  (* no implementation *)

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.

Variable factorial : nat -> nat. (* no implementation *)

Theorem num_permutations : forall A (l : list A) k,
  length l = k -> length (permute l) = factorial k.
Proof.
  induction l.
  - admit.
  - cbn; intros.
    (* the first version of the question stated explicitly the following *)
    assert (forall x y, inject_into a x y = Some x) as Hr. { admit. }
    setoid_rewrite Hr.
Admitted.