Hola,
No sé cómo hay que definir Memoria, yo la definí cómo:
Definition Memoria := nat -> Valor.
Parameter LookUp : ...
Sin embargo con estas definiciones no se me ocurre cómo hacer en el ejercicio 6.3 para definir update. ¿La idea es simplemente un parámetro con el tipo y después axiomas?
Parameter update : Memoria -> nat -> Valor -> Memoria.
Saludos,
Jairo.
Hola.
La idea es dar definiciones, como funciones, para lookup y update (en vez de definir axiomas para operadores que se podría definir con Parameter). Por ejemplo:
Definition lookup(mem: Memoria)(v:Var): Valor := mem v.
Pensá la definición de update, teniendo en cuenta que el resultado es una nueva memoria, que puede ser definida con fun (w:Var) => ...
Saludos, Carlos
Claro. ¿La idea entonces sería utilizar operaciones booleanas Or y And para de esta forma hacer lo que queremos?
¿Se puede utilizar el equal definido al principio del práctico?
Parameter equal : A -> A -> bool.
Axiom equal1 : forall x y : A, equal x y = true -> x = y.
Axiom equal2 : forall x : A, equal x x <> false.
Saludos,
Jairo.
Hola.
Si, se puede usar equal con los dos axiomas referidos. También se puede definir una función equal para nat (las variables son naturales).
Saludos, Carlos
