[Práctico 6] Ejercicio 4.2

[Práctico 6] Ejercicio 4.2

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

Buenas,


No tenemos claro como encarar el ejercicio 4.2. Utilizando el siguiente lema logramos demostrarlo, pero no estaríamos pudiendo demostrar dicho lema: 

Lemma Ej4Aux: forall (l1 l2: list) (a: A), perm l1 l2 -> perm (cons a l1) (append l2 (cons a nil)).

Tienen alguna sugerencia sobre como encarar el ejercicio?

La implementación de reverse que utilizamos es la siguiente:

Fixpoint reverse (l : list) {struct l} : list := 
  match l with 
    | nil => nil
    | cons a l1 => append (reverse l1) (cons a nil)
  end.

Desde ya muchas gracias,

Saludos!


En respuesta a Federico Martin Peña Santucci

Re: [Práctico 6] Ejercicio 4.2

de Carlos Luna -

Hola.

Para probar el lema:

Lemma Ej6_4 : forall (l1 : list), {l2 : list | perm l1 l2}.

Sugiero los siguientes pasos clave:

  • usar exists (reverse l1), luego de introducir l1 al conetxto
  • hacer inducción en l1 (induction l1; simpl).
  • el caso base sale fácil y para el caso inductivo es útil usar perm_trans, eligiendo l2 adecuadamente.

Incluir antes: Hint Constructors perm. De esta manera el uso de auto permite probar algunas cosas automáticamente por aplicación de los constructores de perm (no en el caso de perm_trans ya que hay una lista intermediaria).

Saludos, Carlos