(* Defina la función ++ entre listas de elementos de un tipo genérico y pruebe la corrección
de la relación posfijo del ejercicio anterior demostrando que:
para todas listas l1, l2 y l3: Si l2 = l3++l1 entonces l1 « l2.*)
Lemma PF1 : forall (A:Set)(l1 l2 l3 : list A) ,l2 = append l3 l1 -> l1 « l2.
Proof.
intros.
...y trato de hacer inducción sobre l3 pero no me funciona...ya probé inducción con otros pero debería ser l3...estoy trancado!!!
Sugerencias??
Hola.
Te recomiendo primero reescribir l2 en el goal y luego eliminarla del contexto, para evitar que aparezca luego al hacer inducción en l3. La táctica para sacar una hipótesis del contexto es clear (por ejemplo clear H, donde H es la hipótesis con la igualdad que vincula a l2).
En resumen, probá empezando la prueba con:
intros A l1 l2 l3 H.
rewrite H; clear H.
induction l3.
...
Saludos, Carlos
Buenas tardes!
Siguiendo este mismo hilo ya que es del Ejercicio 17. Nos faltan dos ejercicios con los que nos quedamos trancados.
El primero es:
Pruebe que para todas listas l1, l2 y l3 se cumple que si l1 « l2 y l2 « l1 entonces l1 = l2.
Intentamos hacer inducción en una de las hipótesis pero no pudimos llegar a nada.
Theorem e_4_17_4 : forall (A: Set) (l1 l2: list A), l1 << l2 /\ l2 << l1 -> l1 = l2.
Proof.
intros; elim H; intros.
induction H0.
...
Qed.
--------------------
Y el segundo ejercicio es el de la funcion ultimo.
Nuestra definicion de la funcion es la siguiente:
Fixpoint ultimo (A :Set) (l : list A ) {struct l}: list A :=
match l with
| (nil _)=> nil A
| (cons _ a (nil _)) => (cons _ a (nil _))
| (cons _ b l2) => ultimo A l2
end.
Con esta definición no hemos podido llegar a demostrar el teorema pedido.
Esta definición está bien?
Si está bien, como podemos seguir la prueba que sigue?
Theorem e_4_17_4 : forall (A: Set) (l1 : list A), ultimo A l1 << l1.
Proof.
intros.
induction l1.
simpl.
exact (equal A (nil A)).
Qed.
Hola.
Sobre la primer consulta, la prueba no es trivial. Para no usar inversion en este práctico sugiero que intenten aplicar resultados previos. En particular, el lema que establece "para todas listas l1, l2: Si l1 « l2 entonces existe una lista l3 tal que l2 = l3++l1." sobre cada una de las dos hipótesis (luego de hacer intros). Luego, la prueba sale usando reescrituras y propiedades del append, esencialmente.
Sobre la segunda consulta, sugiero definir la función "ultimo" como sigue:
Fixpoint ultimo (A : Set) (xs : list A) : list A :=
match xs with
| nil _ => nil A
| cons _ x xs' =>
match xs' with
| nil _ => cons A x (nil A)
| cons _ x' xs'' => ultimo A xs'
end
end.
De esta manera queda más claro que si la lista no es vacía hay un análisis de casos para ver si la lista es unitaria o tiene al menos dos elementos. La prueba tiene que seguir los casos de la función, para poder aplicar la definición en cada caso. Esto es:
Lemma ultimo_is_postfix : forall (A : Set) (xs : list A), ultimo A xs << xs.
Proof.
intros. induction xs.
(* caso: lista vacía *)
destruct xs.
(* caso: xs = nil; lista original unitaria *)
(* caso: xs = cons x xs; lista original con al menos dos elementos *)
Qed.
Saludos, Carlos
Carlos, qué tal?
Con respecto al primero. eliminar ese lema dos veces fue algo que intentamos varias veces. Al eliminar y reescribir terminamos en algo así
Pero tampoco sabemos cómo seguir.
Desde acá probamos reemplazando x con (nil A), quedando trivial la prueba de este goal. Pero no nos sale la prueba de que x = nil A. Probamos induction x para esto último pero se nos complica el caso inductivo.
Gracias de nuevo.
Hola.
Mirando tus hipótesis, de H2 y H3 tendrías que x0 +++ x (o x +++ x0) debería ser nil. Con lo cual, tanto x0 como x deberían ser nil.
Luego, para probar propiedades que vinculen a append (+++) sugiero hacerlas aparte, como lemas auxiliares (con las hipótesis adecuadas).
Considerá:
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.
El primer lema no es trivial. Si no te sale ponelo como axioma para completar la prueba.
Saludos, Carlos
Buenas tardes!
Siguiendo este mismo hilo ya que es del Ejercicio 17. Nos faltan dos ejercicios con los que nos quedamos trancados.
El primero es:
Pruebe que para todas listas l1, l2 y l3 se cumple que si l1 « l2 y l2 « l1 entonces l1 = l2.
Intentamos hacer inducción en una de las hipótesis pero no pudimos llegar a nada.
Theorem e_4_17_4 : forall (A: Set) (l1 l2: list A), l1 << l2 /\ l2 << l1 -> l1 = l2.
Proof.
intros; elim H; intros.
induction H0.
...
Qed.
--------------------
Y el segundo ejercicio es el de la funcion ultimo.
Nuestra definicion de la funcion es la siguiente:
Fixpoint ultimo (A :Set) (l : list A ) {struct l}: list A :=
match l with
| (nil _)=> nil A
| (cons _ a (nil _)) => (cons _ a (nil _))
| (cons _ b l2) => ultimo A l2
end.
Con esta definición no hemos podido llegar a demostrar el teorema pedido.
Esta definición está bien?
Si está bien, como podemos seguir la prueba que sigue?
Theorem e_4_17_4 : forall (A: Set) (l1 : list A), ultimo A l1 << l1.
Proof.
intros.
induction l1.
simpl.
exact (equal A (nil A)).
Qed.
