[Practico 5] Ejercicio 3, partes 3 y 5

[Practico 5] Ejercicio 3, partes 3 y 5

de Bruno Lartigau Antonini -
Número de respuestas: 2

Buenas, realizando estas partes del ejercicio 3 quedé en una situación similar en ambos casos.

Parte 3:


Parte 5:


Estuve viendo los foros y ya apliqué case_eq (equal x a) como se sugirió, pero no se cómo seguir. 

Dado que las situaciones son similares, entiendo que de resolver una parte la otra será análoga.

Saludos,

Bruno Lartigau

En respuesta a Bruno Lartigau Antonini

Re: [Practico 5] Ejercicio 3, partes 3 y 5

de Carlos Luna -

Hola.

No es trivial saber bien que tácticas aplicaste hasta llegar acá y si todas las definiciones que diste están bien, pero en la primera prueba podrías introducir como hipótesis MemL x (deleteAll x (consL a l)) para hacer inversión en ella (dado que MemL es inductiva y está instanciada en un constructor). Para probar False tenés IHl. Cuando quieras reducir/aplicar una definicial (como deleteAll en una hipótesis hh podés hacer simpl in hh o simpl in * para hacer reducciones en todas).

El caso de equal con false es similar y también tenés equal2.

Espero esto te ayude!

Saludos, Carlos