[Practico 4] [Ejercicio 17]

[Practico 4] [Ejercicio 17]

de Damian Augusto Langone Fusari -
Número de respuestas: 3

Buenas, tengo un par de consultas con respecto a este ejercicio.


Cuando pide definir la funcion ++, es necesario definir el operador infijo usando Infix o simplemente se puede utilizar la funcion append definida en el ejercicio 4.4?


Por otro lado, para demostrar l1 << l2 y l2 << l1 -> l1 = l2 defini lo siguiente:


Theorem prueba_posfijo2 : forall (A:Set) (l1 l2: list A), posfijo A l1 l2 /\ posfijo A l2 l1 -> l1 = l2.


No veo bien como arrancar, siempre genero hipotesis del tipo posfijo, pero tengo que probar igualdades sin posfijo.


Gracias.

En respuesta a Damian Augusto Langone Fusari

Re: [Practico 4] [Ejercicio 17]

de Carlos Luna -

Hola.

Podés usar Infix para definir un operador de concatenación, pero no es obligatorio; podés usar append.

Sobre el teorema prueba_posfijo2, sugiero que lo dejen pendiente ya que no han visto la táctica "inversion" que es necesaria, además de la inducción. No es necesario que entreguen entonces esta prueba en la entrega 4. Después de que vean "inversion" sugiero que vuelvan a este ejercicio, así lo pueden resolver.

Saludos, Carlos

 


En respuesta a Carlos Luna

Re: [Practico 4] [Ejercicio 17]

de Damian Augusto Langone Fusari -

Hola Carlos,

Vimos en teorico la tactica inversion pero no vemos como aplicarla en este caso. Otra duda que tenemos es si es necesario hacer induction en todas las variables de tipo list A.

Te agradezco si nos podes guiar un poco.

Gracias, saludos.

En respuesta a Damian Augusto Langone Fusari

Re: [Practico 4] [Ejercicio 17]

de Carlos Luna -

Hola.

Este ejercicio déjenlo por ahora, es difícil (explicarlo por mail no es simple). Como dije antes, no es necesario entregarlo como parte del práctico.

Familiarícense primero con el uso de inversion haciendo los primeros ejercicios del práctico 5.

Recuerden que inversion no sustituye a induction.

Saludos, Carlos