[Práctico 5] Ejercicio 3.c

[Práctico 5] Ejercicio 3.c

de Lautaro Cardozo Ramirez -
Número de respuestas: 1

Buenas tardes!

Ejercicio:
Lemma DeleteAllNotMember : forall (l : List) (x : A), ~ MemL x (deleteAll x l).


Con Felipe estuvimos un rato dandole vueltas a esta prueba pero no llegamos a terminarla. Quería saber si vamos por buen camino y cómo podemos seguir.

En primer lugar, está bien esta definición de la función deleteAll?



Si esto está bien cómo podemos seguir desde acá?

Los pasos (más o menos) para llegar ahí fueron hacer inducción en la lista l, inversión para probar caso base, luego destruct de (equal x a) para el paso inductivo.


Gracias!

En respuesta a Lautaro Cardozo Ramirez

Re: [Práctico 5] Ejercicio 3.c

de Carlos Luna -

Hola.

La función deleteAll está bien definida.

En la parte de la prueba donde están perdieron (falta) en como hipótesis información sobre la comparación entre "x" y "a". De hecho, con las hipótesis que están no es posible demostrar el goal ya que falta en este caso la información que "x" es distinto de "a" (sino, no vale).

Cuando hagan el análisis de casos sugiero usar en vez de "destruct (equal x a)", lo siguiente: "case_eq (equal x a)". De esta manera, para ambos casos se genera la hipótesis correspondiente: "equal x a = true" y "equal x a = false".  

Saludos, Carlos