Practico 4 - Ejercicio 15.2

Practico 4 - Ejercicio 15.2

de Bruno Rolando Boz -
Número de respuestas: 3

Buenas, 

Estoy trancado en este ejercicio.

En resumidas cuentas no me doy cuenta como probar:

isomorfo A B (empty_bintree A) (node B a t1 t2) -> False.

Es claro que no se puede construir una prueba de isomorfo A B (empty_bintree A) (node B a t1 t2) e imagino que tengo que poder llegar al absurdo pero no veo como.

Saludos.



 

En respuesta a Bruno Rolando Boz

Re: Practico 4 - Ejercicio 15.2

de Carlos Luna -

Hola.

No se bien como llegaste hasta acá, pero usando algo que veremos en el práctico siguiente (inversion), se prueba. 

Si aplicas inversion H, siendo H el antecedente mencionado, queda demostrado. En este caso inversion trata de ver (intuitivamente) como se prueba/construye esa instancia de isomorfo (que no es posible, es como tener False).

El ejercicio se puede demostrar sin usar isomorfo. Tener en cuenta que se puede hacer inducción no solo en un tipo dato inductivo (lista, árbol), sino también en una relación inductiva, como isomorfo.

Saludos Carlos 

En respuesta a Carlos Luna

Re: Practico 4 - Ejercicio 15.2

de Bruno Rolando Boz -
Demore un poco porque seguí de largo. Ahora estoy retomando ejercicios salteados.

Lo anterior lo precisaba  porque hacia inducción en uno de los arboles y luego de un case necesitaba probar que, si uno de los arboles era vacío y el otro no, entonces, no eran isomorfos.

Finalmente, probé hacer inducción en la relación isomorfo como recomendaste y lo resolví.

En un momento me surgió un problema similar a https://eva.fing.edu.uy/mod/forum/discuss.php?d=55952#p152958. 

Tuve que cambiar en la definición de isomorfo  (isomorfo A l1 r2) /\ (isomorfo A r1 l2) por  (isomorfo A l1 r2) -> (isomorfo A r1 l2). Sin el cambio no me aparecían las hipótesis inductivas.

2 goals
A, B : Set
a1 : A
a2 : B
l1, r1 : bintree A
l2, r2 : bintree B
H0_ : isomorfo A B l1 l2
H0_0 : isomorfo A B r1 r2
IHisomorfo1 : isomorfo B A l2 l1 (* Solo aparece si uso -> en la definición de isomorfo *)
IHisomorfo2 : isomorfo B A r2 r1 (* Solo aparece si uso -> en la definición de isomorfo *)
______________________________________(1/2)
isomorfo B A l2 l1
______________________________________(2/2)
isomorfo B A r2 r1
  
No entiendo porque al usar /\ no aparecen las hipótesis inductivas. ¿No debería ser equivalente?


En respuesta a Bruno Rolando Boz

Re: Practico 4 - Ejercicio 15.2

de Carlos Luna -

Hola Bruno.

Yo uso en general "->" en vez de "/\" para cosas del tipos A /\ B -> C; esto es: A -> B -> C.

Recomiendo usar la flecha (->), aunque el /\ debería funcionar ya que lógicamente es equivalente, pero puedo comprobar que en Coq, al menos en este caso, es como decís al hacer inducción en la hipóteis con isomorfo.

Saludos, Carlos