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

Question

I'm a beginner and I'm stuck with a proof with Coq about lists of nat.

I have a list reg of nat and a function clear_regs that change every values to 0 and leave the third value (index 2) unchanged.

I want to show that forall regs, clear_regs regs = clear_regs (clear_regs regs).

I currently have two functions but I don't know if one is better than the other.

(1) The first is defined with an auxiliary recursive function taking an (descending) index and checking if it's the third value. If it's the case it keep its value otherwise it generates a 0.

(2) The second one map (fun x => 0) to reg and update the third value with (nth 2 reg 0). I'm using the let instruction to keep its value.

I tried things like induction but it doesn't seems to lead the proof to the right path. I don't really know how I should handle the problem. Can someone help me ?

Answer 1

I have two comments, first, your statement about "register number 2" seems a bit adhoc. Why 2? What happens if the number or registers is 1?

Trying to prove this kind of too-specific lemmas usually complicate proofs in Coq. You would do better trying to prove a more general lemma, such as "for a n-register machine, setting the k < n register twice is idempotent." A proof of that result is in the library as set_set_nth. You could combine setting with a "set zero" register operation. I did the proof as you stated it you can compare how the arbitrary 2 complicates size reasoning here:

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.

Note that the proof is induction-free as all the needed induction is encapsulated in the higher-level seq lemmas! I guess you may have had a hard time doing a single induction to prove this lemma as you would likely need to setup a quite complicated induction hypothesis. Thus, it is better to compose several smaller ones.

A different and likely better approach is to use a stronger representation for your registers. In particular, I've chosen to use a nice datatype mathcomp has which is called "finitely supported functions", that is, a map from a finite datatype. The, we represent n registers by a map 'I_n.+1 -> nat where 'I_n is the type of natural numbers less than n. Even in your adhoc case, you can see that it works quite well:

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.

The ffunP lemma is map extensionality: two maps are equal iff they map to the same elements, the rest is routine (eqxx will rewrite x == x to true.

Here you have runnable code: https://x80.org/collacoq/omemesamoy.coq let me know of any questions.

Regards, E.

Answer 2

Here I have defined clear_reg with a helper function with a counter to find the k th element. I prove that the helper function is idempotent and use it in a trivial proof for 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.