[Práctico 4] Ejercicio 17

[Práctico 4] Ejercicio 17

de Federico Martin Peña Santucci -
Número de respuestas: 5

Buenas noches,

En el segundo punto del ejercicio 17.2 se pide demostrar que:

para todas listas l1, l2: Si l1 « l2 entonces existe una lista l3 tal que l2 = l3++l1.

Nuestra definición de posfijo es

Inductive posfijo (A:Set): list A -> list A -> Prop :=
    posfijo0 : forall l1, posfijo A l1 l1
  | posfijoS : forall (l1 l2: list A)(a:A),
              posfijo A l1 l2 -> posfijo A l1 (cons A a l2).

No estamos logrando demostrar dicho lema. En principio, estamos haciendo los siguientes pasos:

Lemma correccionPosfijo2 :
    forall (A:Set)(l1 l2: list A),
    posfijo A l1 l2 -> (exists l3:list A, l2 = append A l3 l1).
Proof.
  intros A l1 l2 h1.
  destruct h1.
  exists (nil A).
  simpl.
  reflexivity.
Luego no sabemos como seguir. Queremos hacer inducción sobre l3 pero entendemos que no podemos hacer esto hasta que tengamos un testigo para el "existe", y no tenemos claro como encontrarlo.

Desde ya muchas gracias,

Saludos
En respuesta a Federico Martin Peña Santucci

Re: [Práctico 4] Ejercicio 17

de Carlos Luna -

Hola.

La definición de posfijo es correcta (la primera lista es posfijo de la segunda).

La prueba no sale por análisis de casos (hacés destruct), sino por inducción. Sugiero hacer elim h1. El caso base sale fácil y para el caso inductivo usar la información del existe que se genera para probar la tesis inductiva (usando la eliminanción del existencial). Observar cuál es el testigo para la prueba del goal.

Saludos, Carlos  

En respuesta a Carlos Luna

Re: [Práctico 4] Ejercicio 17

de Federico Martin Peña Santucci -
Buenas tardes,

También sobre el ejercicio 17, pero esta vez la parte que pide probar:

si l1 « l2 y l2 « l1 entonces l1 = l2.
Mirando esta entrada del foro, se sugiere trabajar con estos dos lemas auxiliares: 

Lemma list_append_nil : forall (A : Set) (l1 l2 : list A), l1 = l2 +++ l1 -> l2 = nil A.
Lemma list_append_nil2 : forall (A : Set) (l1 l2 : list A), l1 +++ l2 = nil A -> l1 = nil A /\ l2 = nil A.

Utilizando estos lemas salió la prueba, pero se nos está complicando demostrar el primer lema.  Probando distintas cosas, si estaría saliendo la pueba de list_append_nil con estos dos otros lemas auxiliares: 

Lemma aux1:  forall (A : Set) (l1:list A)(a:A),   ~ (cons A a l1) = l1.
Lemma aux2:  forall (A : Set) (l1 l2 :list A)(a:A),  ~ append A (cons A a l2) l1 = l1.

Pero esta vez no estaría saliendo la prueba de aux2. Queriamos saber si agregar aux1 y aux2 es complicarla más, o si tienen alguna sugerencia para el encare del lema list_append_nil2 o aux2. En caso que no salga, sería válido ponerlo como axioma?

Desde ya muchas gracias,

Saludos!






En respuesta a Federico Martin Peña Santucci

Re: [Práctico 4] Ejercicio 17

de Carlos Luna -

Hola.

Es compleja la prueba de lista_append_nil (una alternativa es razonando sobre el largo de las listas).

Pueden asumir esta propiedad como un axioma para completar la prueba principal.

Saludos, Carlos