(* 2. Redemuestre el lema anterior usando (verificando) la función inverse del práctico 4 (la
cual, dado un árbol binario construye otro que es su espejo).
El lema que piden demostrar sería de la forma:
Lemma MirrorC_2: forall (A:Set) (t t':bintree A),
mirror t t'->inverse t=t'.
Hola.
La idea es probar el mismo lema pero usando la función inverse para generar el testigo en cada caso. Esto es, verificar que inverse satisface la especificación mirror.
Una opción es, al arrancar la prueba, dar como testigo (con exists) a inverse(t), y realizar la prueba en cada caso siguiendo la lógica de inverse.
Una alternativa (mejor) es usar la función inverse pera haciendo inducción funcional sobre ella:
Hint Constructors mirror.
Functional Scheme inverse_ind := Induction for inverse Sort Prop.
Lemma MirrorC : forall (A : Set) (t : bintree A), {t2 : bintree A | mirror A t t2}.
Proof.
intros A t; exists (inverse A t); functional induction inverse A t; auto.
Qed.
Saludos, Carlos
