Estoy trancado en este ejercicio al tratar de probar que es simétrica, llego siempre a lo mismo:
H0 : isomorfo A t1a t1b /\ isomorfo A t2a t2b
______________________________________(1/1)
isomorfo A t1b t1a /\ isomorfo A t2b t2a
Y de ahí no se como seguir, alguna ayuda?
Hola.
Es difícil ayudarte sin saber bien como definiste la relación isomorfo ni como encaraste esta prueba. No obstante, en este punto de la demostración te surge probar que la relación es simétrica (condición que se cumple).
Saludos, Carlos
Hola Carlos, puedo poner el código de isomorfo acá?
Lo que tengo que probar es isomorfo t1 t2 -> isomorfo t2 t1, lo que hago en un principio es:
intros.
elim H.
apply iso0.
intros.
apply isoN.
y ahí llego a la parte que comentaba, no se para donde arrancar.
Hola.
H corresponde a "isomorfo t1 t2"? o estás haciendo iunducción en uno de los árboles? Las dos estrategias pueden resultar.
Podés subir la definición de isomorfo; no hay problema.
Saludos, Carlos
Hola carlos, gracias por contestar, H: isomorfo t1 t2.
Ahora encontré el "problema", pero no se por que pasa esto:
Inductive isomorfo(A:Set): bintree A->bintree A->Prop :=
iso0 : isomorfo A (emptyTree A) (emptyTree A)
|isoN : forall(a b:A)(t1a t2a t1b t2b: bintree A),
(isomorfo A t1a t1b ) /\ ( isomorfo A t2a t2b ) ->isomorfo A ( addTree A a t1a t2a ) ( addTree A b t1b t2b ).
Si cambio el "/\" por "->" en "(isomorfo A t1a t1b ) /\ ( isomorfo A t2a t2b )", me salen las hipótesis que necesito para terminar la prueba, si no, no aparecen, en este caso no es lo mismo usar el "/\" o el "->"??, no entiendo por que con el "/\" no me salen las hipótesis que deberían aparecer...
La prueba con "->" es
intros.
elim H.
apply iso0.
intros.
apply isoN.
assumption.
assumption.
en el "apply isoN" es que no me salen las hipótesis si uso "/\".
Hola.
Lógicamente son equivalentes; por comodidad es mejor usar -> en vez de /\, para no tener que desarmar la conjunción.
Pasame por mail aparte las definiciones que tenés de este ejercicio, así veo bien esto.
Saludos, Carlos
