Buenas,
Tenía algunas consultas sobre unos ejercicios particulares, así como una más general precisamente sobre generalización.
La pregunta sobre generalización es más bien sobre una funcionalidad de Coq. Supóngase que se tiene la función que dado un operador de dos argumentos naturales devuelve el operador con los argumentos intercambiados:
Definition fswap (f: nat -> nat -> nat) := fun (m n: nat) => f n m.
Puedo demostrar, por ejemplo:
Lemma fswap_id: forall (f: nat -> nat -> nat) (m n: nat), (fswap (fswap f)) m n = f m n.
Proof. cbv delta beta; reflexivity. Qed.
Se quiere generalizar esta definición, y se puede hacer por ejemplo:
Definition fswap' (X: Set) (f: X -> X -> X) := fun (m n: X) => f n m.
En este caso puedo demostrar:
Lemma fswap_id': forall (X: Set) (f: X -> X -> X) (m n: X), (fswap' X (fswap' X f)) m n = f m n.
Proof. cbv delta beta; reflexivity. Qed.
La versión anterior tiene la particularidad de que hay que pasar el parámetro de la generalización como argumento. Según he visto, usando otra sintaxis, el parámetro de la generalización puede ser inferido por los demás argumentos, evitando tener que agregar un argumento redundante. Por ejemplo:
Definition fswap'' {X: Set} (f: X -> X -> X) := fun (m n: X) => f n m.También puede demostrarse para este caso:
Lemma fswap_id'' {X: Set}: forall (f: X -> X -> X) (m n: X), (fswap'' (fswap'' f)) m n = f m n.Proof. cbv delta beta; reflexivity. Qed.
La consulta es en definitiva si esta versión de la generalización está permitida, y si es efectivamente equivalente a la otra versión salvando el detalle sintáctico.
--
Además tengo un par de preguntas sobre los ejercicios de exact y el de AVL. Primero sobre exact:
Supóngase que tengo una prueba que quiero reducir a una linea:
Proof. intros. exact(...). Qed.
¿Hay forma de incorporar la introducción de términos en la táctica exact? De lo contrario la única forma de reducir la prueba anterior a una linea sería:
Proof. intros; exact(...). Qed.
¿Sería esto lo que se espera en los ejercicios 3.14 y 3.15 cuando se pide completar en una linea una demostración a la que no se le han introducido los términos (ejemplo, 3.14.3 ó 3.15.4)?
--
Finalmente, tengo una duda sobre el ejercicio 3.12, de definición de AVL. Se pide definir addAVLi (i=1..k), pero no estoy seguro de cuál se supone que sería la semántica de i (que supongo sería un índice), así como tampoco estoy seguro de cuál sería la cota superior k (podría ser cantidad de nodos, hojas, etcétera dependiendo de la semántica del constructor), o si debería explicitar la cota definiendo otro conjunto para indexar en i que no sean los naturales.
Agrego que la forma en que definiría un AVL (altura n+1) dadas las definiciones anteriores sería en base a un árbol completo (altura n) al que se le agrega un nivel que puede estar o no completo. Pero en este caso faltaría definir el uso del índice, que podría ser una codificación (en bits, por ejemplo) sobre las posiciones a completar, un valor placeholder a ignorar en un vector constructor para el último nivel o cualquier otra cosa (si uno fuera a implementar el constructor). En fin, quería pedir alguna orientación respecto a los requerimientos del ejercicio.
Saludos.