Hola!
Me consultaron directamente a mi correo por los mappings/funciones parciales. Dado que en Coq las funciones son totales, una forma de trabajar con una función parcial de un tipo A a un tipo B, es mediante el uso del tipo option (totalizando la función):
Inductive option (T : Type) : Type :=
Some : T -> option T | None : option T
Definition partial a b := a -> option b.
Notation "a ⇸ b" := (partial a b) (at level 51, right associativity).
Por ejemplo, la memoria sería una mapping parcial y para que vean la forma de trabajar con el tipo option copio abajo el ejemplo del update de la memoria:
Definition system_memory := madd ⇸ page.
Definition update mem addr page : system_memory :=
fun addr' => if madd_eq addr' addr
then Some page
else mem addr'.
Esta es una forma de trabajar, pero no la única.
Saludos, Carlos