使用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节）。

但是，如果不假设公理与功能扩展公理（）一样强大，就不可能在lambdas下直接重写functional_extensionality。

否则，我们可以证明：

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

有关更多详细信息，请参见此处。

不过，如果你愿意接受这样的公理，那么你可以使用由马修Sozeau中所描述的方法这勒柯克俱乐部后下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.