Buenas,
Me queda la duda de cómo empezar a definir los tipos Var, Valor y Memoria.
Deberían ser inductivos? Deberían ser Parameters? Ninguna me termina de convencer.
También me queda la duda de si BEval es Inductive o un Fixpoint.
Saludos,
Joaquín
Hola.
Lo primero es decir que hay más de una opción para formalizar estas cosas.
Var es de tipo nat según la letra del práctico. Esto en Coq lo podés escribir como:
Definition Var := nat.
De manera similar Valor es bool.
Para la memoria se podrían pensar varias opciones (como una lista, una función u otra). La definición como función permite operar con la memoria de forma muy simple:
Definition Mem := nat -> Val.
Finlamente, BEval es una relación inductiva, donde cada constructor sería una de las reglas presentadas en la letra del práctico. Por ejemplo:
Inductive BEval : BoolExp -> Mem -> Val -> Prop :=
| EVar : forall mem var, BEval (VAR var) mem (lookup var mem)
...
Saludos, Carlos