How to assign a natural number to variable in Coq?

Question

How can I assign a natural number to a register (a register is represented by natural number).

For example how do I load a natural number n to register k? How can I compare two natural numbers and assign to a register?

My thinking is to define an inductive type with n, k as natural numbers but I'm not sure what the constructors should be like....

I'm doing something like:

Inductive assign (n, k : nat) Type :=
| load k => k
| load k n => 

Answer 1

One way to do this is to represent the state of all registers as a function from the register number to the stored natural number. We can define a register type indexed by natural numbers as follows:

Inductive register : Type :=
  R : nat -> register.

This is not strictly necessary, but having a separate type for registers prevents confusion between the registers and the natural numbers they store. A state then is just a function from register to nat, and in the empty state we can consider every register to hold the value zero.

Definition state := register -> nat.
Definition empty_state : state := fun _ => 0.

The assignment operation can now be implemented as a function that takes a state and returns a new state with the specified register taking on a new value. To define this we need to prove a quick theorem establishing that register equality is decidable:

Require Import Coq.Arith.EqNat.

Theorem eq_register_decide : forall r1 r2 : register, {r1 = r2} + {r1 <> r2}.
Proof.
  intros r1 r2. destruct r1 as [n1]. destruct r2 as [n2].
  destruct (eq_nat_decide n1 n2) as [Heq | Hneq].
  (* Case 1: n1 = n2 *)
    left. replace n2 with n1. reflexivity. apply eq_nat_eq. apply Heq.
  (* Case 2: n1 <> n2 *)
    right. intros contra. inversion contra.
    apply Hneq. apply eq_eq_nat. apply H0.
Qed.

Definition assign (st : state) (k : register) (n : nat) : state :=
  fun k' => if eq_register_decide k k' then n else st k'.

Here's an example showing that this works. We can assign the value 5 into register 0 and successfully read it back out again:

Example assign_five_to_r0 : (assign empty_state (R 0) 5) (R 0) = 5.
Proof.
  unfold assign. destruct (eq_register_decide (R 0) (R 0)).
  reflexivity. exfalso. apply n. reflexivity.
Qed.

This code is inspired by the update function defined in the Imp chapter of Software Foundations by Pierce et al. There they solve a similar problem but use "variables" instead of "registers."