[Práctico 5] Ejercicio 6.3

[Práctico 5] Ejercicio 6.3

de Marco Nicolas Rodriguez Alvariza -
Número de respuestas: 2
Hola,

¿Podemos usar eqGen y el axioma eqGen1 del ejercicio 4 para definir la función update?

¿Hay algún comparador de la biblioteca estándar de Coq que sea útil para este caso? En principio, había utilizado Nat.eqb, pero después tenía que demostrar a mano cosas como Nat.eqb x x = true o Nat.eqb v1 v2 = true <-> v1 = v2. Si bien esas demostraciones son sencillas, a esta altura del curso me gustaría utilizar herramientas de la biblioteca estándar para no re inventar la rueda sobre problemas sencillos.

Saludos,
Nicolás
En respuesta a Marco Nicolas Rodriguez Alvariza

Re: [Práctico 5] Ejercicio 6.3

de Carlos Luna -

Hola.

Si, la idea es que puedan usar las bibliotecas estándar de Coq. Para este caso sugiero Coq.Arith.EqNat (Require Import Coq.Arith.EqNat.).

Para update se puede entonces usar la función beq_nat. En en la biblioteca EqNat hay también resultados (propiedades) que se pueden usar.

Saludos, Carlos