(* Ejercicio 4.14. Demuestre que la función inverse del ejercicio 4.5 da como resultado un árbol
que cumple con la propiedad de ser espejo del dado (utilice la definición de espejo del
ejercicio 4.1).
*)
Defini inverse y mirror de la siguiente manera.
Inductive bintree (A:Set) : Set :=
empty: bintree A
| node: A -> bintree A ->bintree A -> bintree A.
Arguments empty {A}.
Inductive mirror (A : Set) : bintree A -> bintree A -> Prop :=
| mirror_empty : mirror empty empty
| mirror_node :
forall (a : A) (t1l t1r t2l t2r : bintree A),
mirror t1l t2r ->
mirror t1r t2l ->
mirror (node a t1l t1r) (node a t2l t2r).
Fixpoint inverse (A:Set)(t:bintree A): bintree A:=
match t with
| empty => empty
| node v l r => node v (inverse r) (inverse l)
end.
Lemma mirror_inverse : forall (A : Set) (t:bintree A),
mirror t (inverse t).
Proof.
induction t; simpl ; intros.
constructor.
case t1; case t2;simpl;constructor;constructor.
apply IHt1.
Por qué no puedo utilizar la hipotesis inductiva???