Hola Gabriel.
Celebro tu interés y entusiasmo con el curso, aunque la idea es ir de a poco para ir discutiendo mejor los conceptos y evitar confundir a otras y otros estudiantes, ya que en particular no se dio aún la primera clase.
No obstante, en esta oportunidad respondo brevemente las 6 cuestiones que formulás:
1. Las diferentes versiones de Coq pueden nombrar a las variables de manera diferente. Esto no pasa con la misma versión aunque sea en diferentes plataformas. Se sugiere hacer intros con nombres de variable para no depender de nada. No obstante, no es algo para preocuparse ahora; la corrección que hacemos al inicio del curso contempla estas diferencias.
2. La respuesta corta a tu primera presgunta es si, aunque en los primeros prácticos recomendamos usar las tácticas que se vean en clase, con el ojetivo de entender los conceptos básicos. A medida que avance el curso veremos formas más "eficientes" de hacer pruebas, usando lemas auxilares, resultados anteriores e incluso biliotecas de Coq (como sucede con la programación en los lenguajes de programación).
3. Es así. Veremos y dscutiremos el uso de táticas automáticas (como tauto) en la clase, analizando en particular sus alcances. Si bien muchos ejercicios del práctico 1 se podrían hacer con tácticas automáticas, la idea es que aprendar primero las tácticas básicos, sino luego se complica entender los conceptos del curso. Iremos indicando donde usar tácticas automáticas; con mayor libertad en la segunda parte del curso, cuando entiendan donde sirven y para qué.
4. El ej. 11 pide resolver el lema sin usar tácticas automáticas primero y luego usando tauto. Hacé las dos pruebas.
5. Si, se resuelve con lógica clásica.
6. Esto lo veremos más adelante. Modularizar es una opción, separando por ejemplo cosas en archivos diferentes o en secciones diferentes de un mismo archivo (si ponés el problema 11 en una sección y el 12 en otra, no deberías tener ese problema). No obstante, habría que ver tu formalización del problema 11, ya que para derivar la contradicción se precisan hipótesis: H1 /\ ... /\ Hn -> ...
Nos vemos mañana en la clase.
Saludos, Carlos