Practico 4 - Ejercicio 11.5

Practico 4 - Ejercicio 11.5

de Daniel Alejandro Garcia Miranda -
Número de respuestas: 3

Buenas.,

estoy con problemas para demostrar el L5. Llego a esto:

A : Set

a : A

l : list A

IHl : length A (reverse_aux A l (nil A)) = length A l

______________________________________(1/1)

length A (reverse_aux A l (const A a (nil A))) = S (length A (reverse_aux A l (nil A)))


Y luego no se como seguir. Puede ser que mi definición de reverse este mal: 

Fixpoint reverse_aux (A:Set) (l acc : list A) : list A := 

  match l with 

    | nil   _        => acc

    | const _ x rest => reverse_aux A rest (const A x acc)

  end . 


Definition reverse (A: Set) (l:list A) : list A := 

  reverse_aux A l (nil A).

En respuesta a Daniel Alejandro Garcia Miranda

Re: Practico 4 - Ejercicio 11.5

de Carlos Luna -

Hola Daniel

Tu definición de reverse no está mal pero no es muy práctica para razonar inductivamente, ya que se  basa en otra función que va acumulando el resultado.

No obstante, en el contexto actual podrías usar IHl y luego probar (podría ser con un lema auxiliar) que "length A (reverse_aux A l (const A a (nil A)))" es el largo de l más 1 (por inducción en l).

Otra opción es definir inverse usando append (inverse (x:l) = (inverse l)++[x]) en vez de reverse_aux. Acá se pueden usar luego propiedades de append y length, como L4. 

Saludos, Carlos