[Práctico 4] - Ejercicio 4.16.2

[Práctico 4] - Ejercicio 4.16.2

de Jairo Yamil Bonanata Silva -
Número de respuestas: 4

Hola, haciendo elim en l3 este ejercicio se resuelve fácilmente. Sin embargo si hacemos induction en l3 llegamos a una hipótesis inductiva con la que no podemos llegar a nada. ¿No entiendo por qué?

 

Esta es la prueba correcta con elim:

Lemma es_correcto_posfijo1 : forall (A : Set) (l1 l2 l3 : list A),
l2 = append A l3 l1 -> posfijo A l1 l2.
Proof.
intros.
rewrite H.
elim l3.
simpl.
apply vacio.
simpl.
intros.
apply no_vacio.
assumption.
Qed.

Sin embargo cuando la hago con iduction llego en le paso inductivo llego a:

H : l2 = append A (cons A a l3) l1
IHl3 : l2 = append A l3 l1 -> posfijo A l1 (append A l3 l1)
______________________________________(1/1)
posfijo A l1 (append A (cons A a l3) l1)

Saludos,
Jairo.

 

En respuesta a Jairo Yamil Bonanata Silva

Re: [Práctico 4] - Ejercicio 4.16.2

de Jairo Yamil Bonanata Silva -

Mando la definición que me quedó de posfijo.

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

Saludos,
Jairo.

En respuesta a Jairo Yamil Bonanata Silva

Re: [Práctico 4] - Ejercicio 4.16.2

de Carlos Luna -

Hola.

elim e induction no hacen exactamente lo mismo sobre objetos inductivos; esto puede verse en el manual de Coq (online). En particular, en un caso se abstrae en la HI las condiciones involucradas y en la otra no.

La definición de posfijo es correcta.

Saludos, Carlos

En respuesta a Carlos Luna

Re: [Práctico 4] - Ejercicio 4.16.2

de Jairo Yamil Bonanata Silva -

Hola,
Perdón que parezca tonta la pregunta. ¿Pero a que te refieres con se abstrae? Yo entiendo la abstracción como en el cálculo lambda. ¿Es correcto?

Saludos,
Jairo.