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

Question

我是初学者，我一直在用 Coq 证明 nat.

我有一个 list reg 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

我有两条评论，首先，您关于 "register number 2" 的陈述似乎有点临时。为什么是2？如果数字或寄存器为 1 会怎样？

试图证明这种过于具体的引理通常会使 Coq 中的证明复杂化。您最好尝试证明更一般的引理，例如 "for a n-register machine, setting the k < n register twice is idempotent." 该结果的证明在库中为 set_set_nth。您可以将设置与 "set zero" 注册操作结合起来。我做了你所说的证明，你可以在这里比较任意 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 的一个很好的数据类型 "finitely supported functions"，即来自有限数据类型的映射。然后，我们用映射 '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 重写为 true。

这里有可运行的代码：https://x80.org/collacoq/omemesamoy.coq如有任何问题，请告诉我。

问候，E.

Answer 2

这里我定义了 clear_reg 和一个带有计数器的辅助函数来查找第 k 个元素。我证明辅助函数是幂等的，并在 clear_reg.

的简单证明中使用它

Require Import Arith. (* for eq_nat_dec *)

Fixpoint clear_reg_aux (l:list nat) k (i:nat) :=
  match l with
    | nil => nil
    | cons x l' =>
      let x' := if eq_nat_dec i k then x else 0 in
      cons x' (clear_reg_aux l' k (i+1))
  end.
Definition clear_reg l := clear_reg_aux l 2 0.

Lemma cra_idem:
  forall l k n, clear_reg_aux l k n = clear_reg_aux (clear_reg_aux l k n) k n.
Proof.
  induction l.
  - auto.
  - intros k n. simpl. rewrite <- IHl. destruct (eq_nat_dec n k). auto. auto.
Qed.

Lemma clear_reg_idem: forall l, clear_reg l = clear_reg (clear_reg l).
  intros. unfold clear_reg. rewrite <- cra_idem. auto.
Qed.

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

Proof of idempotence for a function clearing a list but one element

coq