coq - 清除列表但只有一个元素的函数的幂等性证明

Question

我是一个初学者，我被 Coq 关于 nat 列表的证明困住了。

我有一个 list reg of nat 和一个函数 clear_regs，它将每个值更改为 0 并保持第三个值(索引 2)不变。

我想证明forall regs, clear_regs regs = clear_regs (clear_regs regs)。

我目前有两个功能，但我不知道一个是否比另一个更好。

(1) 第一个是用辅助递归函数定义的，该函数采用(降序)索引并检查它是否是第三个值。如果是这种情况，它会保留其值，否则会生成 0。

(2) 第二个将 (fun x => 0) 映射到 reg 并用 (nth 2 reg 0) 更新第三个值。我正在使用 let 指令来保持它的值。

我尝试了归纳之类的方法，但它似乎并没有将证明引向正确的路径。我真的不知道我应该如何处理这个问题。有人可以帮助我吗？

Answer 1

我有两条评论，首先，您关于“注册 2 号”的说法似乎有点特别。为什么是2？如果数字或寄存器为 1 会怎样？

试图证明这种过于具体的引理通常会使 Coq 中的证明复杂化。您最好尝试证明一个更一般的引理，例如“对于 n 寄存器机器，将 k < n 寄存器设置两次是幂等的。”该结果的证明在库中为 set_set_nth。您可以将设置与“置零”寄存器操作结合起来。我做了你所说的证明，你可以在这里比较任意 2 如何使大小推理复杂化:

From mathcomp
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Implicit Type (reg : seq nat).

(* You could also use take/drop to perform surgery *)
Definition clear_regs reg :=
  set_nth 0 (nseq (size reg) 0) 2 (nth 0 reg 2).

Definition idem A (f : A -> A) := forall x, f (f x) = f x.

Lemma clear_regs_idem : idem clear_regs.
Proof.
(* We reduce equality of lists to equality of their elements, `eq_from_nth` *)
move=> reg; apply: (@eq_from_nth _ 0).
  by rewrite !size_set_nth !size_nseq maxnA maxnn.

(* Now we need to use the fact that nth (set s x) = x, plus a bit of case reasoning *)
move=> i i_sz; rewrite !nth_set_nth /=; case: eqP => [//|].
by rewrite !nth_nseq; case: ifP; case: ifP.
Qed.

请注意，证明是无归纳的，因为所有需要的归纳都封装在更高级别的 seq 引理中!我猜你可能很难通过单一归纳来证明这个引理，因为你可能需要建立一个非常复杂的归纳假设。因此，最好组合几个较小的。

另一种可能更好的方法是为您的寄存器使用更强的表示。特别是，我选择使用 mathcomp 具有的一种很好的数据类型，称为“有限支持的函数”，即来自有限数据类型的映射。我们用映射 'I_n.+1 -> nat 表示 n 个寄存器，其中 'I_n 是小于 n 的自然数的类型。即使在您的临时案例中，您也可以看到它运行良好:

From mathcomp
Require Import choice fintype finfun.

Section Regs.

Variable k : nat.
Definition reg := {ffun 'I_k.+1 -> nat}.

Implicit Type (r : reg).

Definition clearr r : reg :=
  [ffun idx => if idx == (inord 2) then r (inord 2) else 0].

Lemma clearr_idem : idem clearr.
Proof. by move=> x; apply/ffunP=> j; rewrite !ffunE eqxx. Qed.

ffunP 引理是映射可扩展性:两个映射是相等的，当且仅当它们映射到相同的元素，其余是常规的(eqxx 将重写 x == x 为 真。

这里有可运行代码:https://x80.org/collacoq/omemesamoy.coq让我知道任何问题。

问候，E.