Con respecto a los ejercicios 13,14 y 15, cuando hablan de "...complételas en un sólo renglón utilizando la táctica exact...", se refieren a que sólo se puede usar exact o podriamos hacer algo de la forma intros;exact ?
Gracias.
Buenas, con respecto al ejercicio 8, hice el Check pero no logro entender el tipo resultante. Creo que no estoy entendiendo la representación del array, ni como funciona 'add' ya que al intentar realizar lo pedido en la parte 2 siempre obtengo error de tipo.
Con respecto a los ejercicios 13,14 y 15, cuando hablan de "...complételas en un sólo renglón utilizando la táctica exact...", se refieren a que sólo se puede usar exact o podriamos hacer algo de la forma intros;exact ?
Gracias.
Con respecto a los ejercicios 13,14 y 15, cuando hablan de "...complételas en un sólo renglón utilizando la táctica exact...", se refieren a que sólo se puede usar exact o podriamos hacer algo de la forma intros;exact ?
Gracias.
Hola Alfredo.
En el ejercicio 8:
Parameter ArrayNat : forall n:nat, Set.
el tipo de ArrayNat es nat -> Set. Esta definición nos permite definir un Set paramétrico en los naturales (arreglos de naturales de cierto largo).
Parameter add : forall n:nat, nat -> ArrayNat n -> ArrayNat (n + 1).
formaliza un operador que permite agregar un elemento de tipo nat a un arreglo de naturales de largo n, generando un arreglo de largo n+1.
Por ejemplo, un elemento de tipo ArrayNat 1 puede ser: add 0 8 empty. Esto es, un arreglo de largo 1 que tiene como único elemento al 8.
Con respecto a los ejercicios 13-15, solo se puede usar exact (no intros;exact). Tené en cuenta qué término permite construir un intro; por ejemplo analizá:
Lemma Ej: A -> A.
Proof.
exact (fun x : A => x).
Qed.
Saludos, Carlos