使用 lambda 参数重写 Coq

我们有一个函数可以将元素插入到列表的特定索引中。

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.

上述函数的以下性质与问题相关（证明省略，直接归纳l with n未修复）：

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

我们有一个排列的计算定义，其中iota k成为 nat 列表[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.

我们试图证明的定理：

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

通过感应l我们（最终）可以达到以下目标：length (permute (a :: l)) = S (length l) * length (permute l)。如果我们现在简单地cbn，最终目标表述如下：

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)) =
length (permute l) + length l * length (permute l)

在这里我想继续destruct (inject_into a x y)，考虑到这是不可能的x and y是 lambda 参数。请注意，我们永远不会得到None引理的分支inject_correct_index.

如何从这个证明状态出发呢？ （请注意，我并不是想简单地完成定理的证明，这是完全无关的。）

有一种方法可以在binders下重写：setoid_rewrite战术（见§27.3.1Coq 参考手册）。

然而，direct如果不假设一个公理与函数外延性公理一样强大，那么在 lambda 下重写是不可能的（functional_extensionality).

否则，我们可以证明：

(* classical example *)
Goal (fun n => n + 0) = (fun n => n).
  Fail setoid_rewrite <- plus_n_O.
Abort.

See here了解更多详情。

然而，如果您愿意接受这样的公理，那么您可以使用Matthieu Sozeau 在thisCoq Club 帖子在 lambda 下重写如下：

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.
Proof. intros f g Hfg. apply functional_extensionality. intro x; apply sb, (Hfg x). Qed.

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