使用 lambda 参数重写 Coq

Question

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

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 的直接归纳，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 是一个 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.

我们要证明的定理：

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 和y 是lambda 参数，这是不可能的。请注意，由于引理inject_correct_index，我们永远不会得到None 分支。

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

Answer 1

有一种在活页夹下重写的方法：setoid_rewrite 策略（参见 Coq 参考手册的 §27.3.1）。

但是，如果不假设公理与功能扩展性公理 (functional_extensionality) 一样强大，则无法在 lambdas 下直接重写。

否则，我们可以证明：

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

更多详情请参阅here。

不过，如果你愿意接受这样的公理，那么你可以使用 Matthieu Sozeau 在this Coq Club 帖子中描述的方法在 lambdas 下重写，如下所示：

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.