[Practico 4][Ejercicio 19]

[Practico 4][Ejercicio 19]

de Carlos Augusto Rodriguez Gonzalez -
Número de respuestas: 1

Hola,

Este ejercicio me esta quedando demasiado simple por lo que presumo que debo estar errandole en lo que se esperaba, pero despues de leerlo varias veces no veo que estoy haciendo mal.

La funcion h la defini asi: Definition h := fun (A:Set) (n:nat) (a:ACom A n) => pot 2 n. (Esta es la funcion pot definida en el ej. 4.3)

Porlo tanto lo que se pide probar me queda trivial, Lemma numHojas : forall (A:Set) (n:nat) (t:ACom A n), h A n t = pot 2 n.

Cual es la idea del ejercicio?

Gracias,

Carlos.

En respuesta a Carlos Augusto Rodriguez Gonzalez

Re: [Practico 4][Ejercicio 19]

de Carlos Luna -
Hola.


La función h debe definirse recursivamente sobre un árbol (familia) de tipo ACom A n. 

Fixpoint h (A:Set) (n:nat) (tree: ACom A n): nat:=

   match tree with

      constructor1 ... =>  ...

      | constructor2 ...  => ...

   end.

Luego hay que probar que:

Lemma nombre (A:Set) : forall n:nat, forall tree : ACom A n, h A n t = pot 2 n.

Saludos, Carlos