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

如何从这种证明状态出发？ (请注意，我并不是要简单地完成定理的证明，这完全无关紧要。)

Answer 1

有一种方法可以在活页夹下重写:setoid_rewrite策略(参见 Coq 引用手册的 §27.3.1)。

然而，直销 如果不假设一个与函数扩展性公理 ( functional_extensionality ) 一样强大的公理，就不可能在 lambda 下重写。

否则，我们可以证明:

(* 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.