Coq 使用 lambda 参数重写

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）。

然而，直接在 lambdas 下重写是不可能的，除非假设公理与函数扩展公理 (functional_extensionality) 一样强大。

否则，我们可以证明：

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

有关详细信息，请参阅 here。

不过，如果你愿意接受这样的公理，那么你可以使用 Matthieu Sozeau 在 this Coq Club post 中描述的方法在 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.

Coq 使用 lambda 参数重写

Coq rewriting using lambda arguments

coq

proof