使用Lambda参数重写Coq [英] Coq rewriting using lambda arguments

问题描述

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

We have a function that inserts an element into a specific index of a list.

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 不固定）：

The following property of the aforementioned function is of relevance to the problem (proof omitted, straightforward induction on l with n not being fixed):

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] ：

And we have a computational definition of permutations, with iota k being a list of 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 ，则得出的目标如下：

By induction on l we can (eventually) get to following goal: length (permute (a :: l)) = S (length l) * length (permute l). If we now simply cbn, the resulting goal is stated as follows:

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

Here I would like to proceed by destruct (inject_into a x y), which is impossible considering x and y are lambda arguments. Please note that we will never get the None branch as a result of the lemma inject_correct_index.

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

How does one proceed from this proof state? (Please do note that I am not trying to simply complete the proof of the theorem, that's completely irrelevant.)

推荐答案

有在活页夹下重写的一种方法： setoid_rewrite 策略（请参见第27.3.1节）。

There is a way to rewrite under binders: the setoid_rewrite tactic (see §27.3.1 of the Coq Reference manual).

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

However, direct rewriting under lambdas is not possible without assuming an axiom as powerful as the axiom of functional extensionality (functional_extensionality).

否则，我们可以证明：

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

请参见此处了解更多详情。

不过，如果您愿意接受公理，那么您可以使用Matthieu Sozeau在此 Coq Club帖子在lambda下重写，如下所示：

Nevertheless, if you are willing to accept such axiom, then you can use the approach described by Matthieu Sozeau in this Coq Club post to rewrite under lambdas like so:

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.

这篇关于使用Lambda参数重写Coq的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！