[Práctico 4] Ejercicio 18

[Práctico 4] Ejercicio 18

de Jairo Yamil Bonanata Silva -
Número de respuestas: 10

Hola, estoy trancado con este ejercicio.

Section Ejercicio18.

Variable A : Set.

Inductive Tree_ : Set :=
   | nullT : Tree_
   | consT : A -> Tree_ -> Tree_ -> Tree_.

La idea es definir un predicado inductivo:

Inductive isSubTree : Tree_ -> Tree_ -> Prop := ...

Yo definí dicho predicado, pienso que es correcto, pero no logro probar la parte 3 que pide la transitividad. ¿Alguna pista?

Saludos,
Jairo.

En respuesta a Jairo Yamil Bonanata Silva

Re: [Práctico 4] Ejercicio 18

de Carlos Luna -

Hola.

Claramente es un ejercicio que sale por inducción. Uno podría aplicar inducción en alguno de los árboles involucrados o en alguna de las hipótesis inductivas que refieren a isSubTree.

Sugiero por ejemplo hacer inducción en la hipótesis isSubTree t2 t3.

Saludos, Carlos

En respuesta a Carlos Luna

Re: [Práctico 4] Ejercicio 18

de Jairo Yamil Bonanata Silva -

Hola,

Lo que me queda la duda es si hay que definirlo como un fixpoint o como un inductive.

Saludos,
Jairo.

En respuesta a Jairo Yamil Bonanata Silva

Re: [Práctico 4] Ejercicio 18

de Carlos Luna -

Como un Inductive (es una relación inductiva entre árboles).

Saludos, Carlos

En respuesta a Carlos Luna

Re: [Práctico 4] Ejercicio 18

de Jairo Yamil Bonanata Silva -

Sí, lo definí así, sin embargo no me doy cuenta de cómo sale.

Saludos,
Jairo.

En respuesta a Jairo Yamil Bonanata Silva

Re: [Práctico 4] Ejercicio 18

de Carlos Luna -

Hola.

isSubTree debe ser una relación binaria inductiva entre árboles binarios.

Tener en cuenta que todo árbol es subárbol de si mismo. Por otra parte, si un árbol A1 es subárbol de otro A2, a1 es subárbol de un árbol más grande estructuralmente que A2.

La prueba de que isSubTree es tranistiva puede salir de varias formas, pero con la sugerencia del mail previo resulta muy accesible.

Saludos, Carlos

 

En respuesta a Jairo Yamil Bonanata Silva

Re: [Práctico 4] Ejercicio 18

de Romina Diana Romero Riva -

Hola.

¿Está bien si defino isSubTree diciendo que todo árbol es subárbol de sí mismo (además de otros casos)? Porque no estoy segura de que sea una definición inductiva bien hecha.

Gracias.

Saludos!

En respuesta a Romina Diana Romero Riva

Re: [Práctico 4] Ejercicio 18

de Jairo Yamil Bonanata Silva -

Yo lo definí así. Lo que no sé es si se puede definir utilizando la igualdad. ¿Estaría bien este segundo caso?

Saludos,
Jairo.

En respuesta a Jairo Yamil Bonanata Silva

Re: [Práctico 4] Ejercicio 18

de Carlos Luna -

No hace falta la igualdad (aunque no estaría mal tampoco usar la igualdad). Podés poner:

Inductive isSubTree : Tree -> Tree -> Prop :=
  eq_subtree : forall t:Tree, isSubTree t t
  | ...

Saludos, Carlos