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.
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
Hola,
Lo que me queda la duda es si hay que definirlo como un fixpoint o como un inductive.
Saludos,
Jairo.
Como un Inductive (es una relación inductiva entre árboles).
Saludos, Carlos
Sí, lo definí así, sin embargo no me doy cuenta de cómo sale.
Saludos,
Jairo.
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
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!
Hola.
Que todo árbol es subárbol de si mismo sería el caso base de la definición inductiva de la relación.
Saludos, Carlos
Yo lo definí así. Lo que no sé es si se puede definir utilizando la igualdad. ¿Estaría bien este segundo caso?
Saludos,
Jairo.
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
Sí, lo hice así. Quería saber si era correcta la otra forma. Gracias!
Saludos,
Jairo.
