Buenas noches. Tengo esta definición de subtree. No estoy pudiendo demostrar la transitividad. ¿Me podrían dar una pista de cómo empezar la demo? No me doy cuenta sobre qué hacer la inducción. Gracias.
Inductive is_SubTree : Tree_ -> Tree_ -> Prop :=
| SubTree_refl : forall t, is_SubTree t t
| SubTree_left : forall (a:A) (t_izq t_der t : Tree_),
is_SubTree t_izq t -> is_SubTree (consT a t_izq t_der) t
| SubTree_right : forall (a:A) (t_izq t_der t : Tree_),
is_SubTree t_der t -> is_SubTree (consT a t_izq t_der) t
Lemma trans_subtree : forall (t1 t2 t3 :Tree_) ,
is_SubTree t1 t2 /\ is_SubTree t2 t3 -> is_SubTree t1 t3.
Hola
Es conveniente hacer inducción en una de las hipótesis inductivas (de is_SubTree).
Dado que no tengo todas tus deficiones, copio abajo una solución donde considero en este caso que el primer argumento es subárbol del segundo (en tu caso lo formalizaste al revés, pero no está mal).
Saludos, Carlos
==========
Variable A : Set.
Inductive Tree_ : Set :=
| nullT : Tree_
| consT : A -> Tree_ -> Tree_ -> Tree_.
Inductive isSubTree: Tree_->Tree_->Prop:=
baseTree : forall t : Tree_, isSubTree t t
| indTreeDer : forall t1 t2 t3 : Tree_, forall a :A, isSubTree t1 t2 -> isSubTree t1 (consT a t3 t2)
| indTreeIzq : forall t1 t2 t3 : Tree_, forall a :A, isSubTree t1 t2 -> isSubTree t1 (consT a t2 t3).
Theorem isSubTreeTrans : forall t1 t2 t3 : Tree_, (isSubTree t1 t2) -> (isSubTree t2 t3) -> (isSubTree t1 t3).
Proof.
intros.
induction H0.
assumption.
constructor.
apply IHisSubTree; assumption.
apply indTreeIzq.
apply IHisSubTree; assumption.
Qed.
Muchas gracias!
Saludos.
Saludos.