How to assign a natural number to variable in Coq? -

how can assign natural number register (a register represented natural number).

for example how load natural number n register k? how can compare 2 natural numbers , assign register?

my thinking define inductive type n, k natural numbers i'm not sure constructors should like....

i'm doing like:

inductive assign (n, k : nat) type := | load k => k | load k n =>  

one way represent state of registers function register number stored natural number. can define register type indexed natural numbers follows:

inductive register : type :=   r : nat -> register. 

this not strictly necessary, having separate type registers prevents confusion between registers , natural numbers store. state function register nat, , in empty state can consider every register hold value zero.

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

the assignment operation can implemented function takes state , returns new state specified register taking on new value. define need prove quick theorem establishing register equality decidable:

require import coq.arith.eqnat.  theorem eq_register_decide : forall r1 r2 : register, {r1 = r2} + {r1 <> r2}. proof.   intros r1 r2. destruct r1 [n1]. destruct r2 [n2].   destruct (eq_nat_decide n1 n2) [heq | hneq].   (* case 1: n1 = n2 *)     left. replace n2 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' n else st k'. 

here's example showing works. can assign value 5 register 0 , read 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 inspired update function defined in imp chapter of software foundations pierce et al. there solve similar problem use "variables" instead of "registers."