Hola, no nos está saliendo este ejercicio:
Acá van las definiciones inductivas:
(*1*)
Inductive bintree (A:Set) : Set :=
| vacio_Bt : bintree A
| nodoB : A -> bintree A -> bintree A -> bintree A.
(* ejercicio 4.1.6 *)
Inductive mirror (A:Set) : bintree A -> bintree A -> Prop :=
| vaciosBts : mirror A (vacio_Bt A) (vacio_Bt A)
| no_vaciosBts : forall (a :A) (t1 t2 t3 t4: bintree A),
mirror A t1 t3 -> mirror A t2 t4 ->
mirror A (nodoB A a t1 t2) (nodoB A a t4 t3).
(* ejercicio 4.1.7 *)
Inductive isomorfo (A B : Set) : bintree A -> bintree B -> Prop :=
| vacionIso : isomorfo A B (vacio_Bt A) (vacio_Bt B)
| no_vaciosIso : forall (a : A) (b : B) (t1 t2 : bintree A) (t3 t4 : bintree B),
isomorfo A B t1 t3 -> isomorfo A B t2 t4 ->
isomorfo A B (nodoB A a t1 t2) (nodoB B b t3 t4).
No me está saliendo la transitiva, la prueba llegué a:
Theorem T3 : forall (A:Set)(t1 t2 t3 : bintree A),
isomorfo A A t1 t2-> isomorfo A A t2 t3-> isomorfo A A t1 t3.
Proof.
intros.
induction t1.
induction t3.
constructor.
inversion H.
rewrite <- H2 in H0.
inversion H0.
inversion H0.
rewrite <- H1 in H.
inversion H.
Saludos,
Jairo.