Para trabajar con mappings, pueden:
1) basarse en la biblioteca Maps.v que se incluye junto con la letra del práctico, o
2) directamente usar las funciones de Coq. Para definir una función parcial de un tipo A a un tipo B, puede usarse el tipo option:
Inductive option (T : Type) : Type :=
Some : T -> option T | None : option T
Esto es, f : A -> option B.
Volviendo a (1) copio abajo un ejemplo de uso de map_apply para definir (de cierta manera - es solo un ejemplo) la precondición de la acción chmod:
Definition PreConditionChmod (s : state) : Prop :=
aos_activity s = waiting /\
exists os,
Value _ os = map_apply os_ident_eq (oss s) (active_os s) /\
(hcall os) = None.
Saludos, Carlos