Hola,
Estoy trancada en este ejercicio. Lo que intenté fue definirme una función "altura" para pasar del mundo de los árboles al de los naturales y pude probar que el orden con esa función es bien fundado pero no logro usar esa información en la prueba que se pide en este ejercicio. Intenté también probar que tree_sub es bien fundado sin usar nada auxiliar y tampoco llegué a nada (de ahí fue que se me ocurrió intentar ir a los naturales).
Alguna idea?
Gracias y saludos,
Noelia.
Esta prueba la podés hacer usando la definición de well_founded (con unfold) primero y luego inducción en el árbol. Los subgoals salen usando constructor e inversion, esencialmente. También se podría usar Acc_intro, pero no es necesario.
Otra alternativa es usar una función como la cantidad de nodos para demostrar que un orden es bien fundado sobre árboles, llevando el problema al dominio de los naturales. Esto de hecho es lo que pide el ejercicio 8.
Require Import Wf_nat.
Require Import Inverse_Image.
Fixpoint size e :=
...
Definition elt e1 e2 := size e1 < size e2.
Theorem well_founded_elt : well_founded elt.
Proof.
apply (wf_inverse_image BoolExpr nat lt size).
...
Saludos, Carlos
