4º [EI] Matemáticas Discretas 2 (MD2)

[susana]

Si no estoy equivocada, durante las últimas clases de prácticas se estuvo siguiendo el texto de "Coq in a hurry" que es un pdf cortito que como bien indica es para ver rápidamente Coq.
Una vez que sepas las bases, a lo mejor te sirve de ayuda la siguiente página: http://www.seas.upenn.edu/~cis500/cis50 ... edule.html. Podrías intentar hacer los primeros ejercicios.

[ishinay]

No conocía yo este último enlace... y mira que está bien...

[susana]

Enlace a la práctica (que es para antes del 20 de enero): http://www.dc.fi.udc.es/staff/freire/md ... actica.pdf

[Fer]

Enlace a la práctica (que es para antes del 20 de enero): http://www.dc.fi.udc.es/staff/freire/md ... actica.pdf

Si puedes subirla al directorio de prácticas, te lo agradecería, que no sé cómo poner exactamente en los títulos y tal.

[susana]

El pdf creo que es provisional todavía, que se van a cambiar algunos ejercicios del final, por lo que esperaré a que sea definitivo para subirlo.

[esramar]

Enlace a la práctica (que es para antes del 20 de enero): http://www.dc.fi.udc.es/staff/freire/md ... actica.pdf

lo acabo de leer, y me he quedado igual :S

[susana]

lo acabo de leer, y me he quedado igual :S

¿Te refieres a que no sabes cómo hacer la práctica?
Si quieres vete diciendo hasta dónde llegas, y te puedo dar consejos, pistas, para que intentes seguir.
Yo la hice ayer. Hubo dos lemas/teoremas que cuestan un poco más, "peleando un poco" (pero comprendiendo cada paso de la demostración) podéis hacerla sin problema, y creo que puede ayudar a entender bien la asignatura de cara al examen final.

[Hadrian]

lo acabo de leer, y me he quedado igual :S

¿Te refieres a que no sabes cómo hacer la práctica?
Si quieres vete diciendo hasta dónde llegas, y te puedo dar consejos, pistas, para que intentes seguir.
Yo la hice ayer. Hubo dos lemas/teoremas que cuestan un poco más, "peleando un poco" (pero comprendiendo cada paso de la demostración) podéis hacerla sin problema, y creo que puede ayudar a entender bien la asignatura de cara al examen final.

Puedo preguntar cúanto tiempo te llevó hacerla? xD Y sobre todo, cúanto tiempo le llevaría a alguien como nosotros, que no conozca Coq tan a fondo como tú. xD

[susana]

Puedo preguntar cúanto tiempo te llevó hacerla? xD Y sobre todo, cúanto tiempo le llevaría a alguien como nosotros, que no conozca Coq tan a fondo como tú. xD

Pues lo básico me llevó muy poco, media hora como mucho. Pero el teorema Esquema me llevó un poco más. Creo que es el más complicado, porque no es trivial. De todas formas, yo hice las demostraciones paso por paso, sin usar auto e intuition, que eso ahorra tiempo Creo que es recomendable saber lo que se está haciendo antes que probar auto en cada línea a ver si lo resuelve . Pero en un examen si dejan hacerlo también es una opción para salir del paso, no lo niego.
No sé cuánto os puede llevar hacerlo, pero yo creo que para el día 20 es tiempo suficiente.
Pero ya sabéis, si tenéis cualquier duda, planteadla y así se irá entendiendo poco a poco.

[ishinay]

Pues yo ya me he quedado en el primer "Lemma th...". Dice:

Código: Seleccionar todo

Lemma th : forall x y : nat, div2P x y -> div2P (S (S x )) (S y).

en este momento, el primer subobjetivo es 2 * Sy=S(Sx).
En esta situación:

x:nat
y:nat
H0:2*y=x \/ 1+2*y=x
H:2*y=x
===============
2*Sy = S(Sx)

¿Cómo que "el primer subobjetivo es 2*Sy=S(Sx)?? Antes tendrás que haber hecho algo como deltareducción y betareducción ¿no? y si haces "intros" el resultado no es el que se muestra, que yo no veo por ningún lado un:

Código: Seleccionar todo

1+2*Sy=S(Sx)

que sería la primera parte de la OR al unfoldear y betareducir "div2P (S(x)) (S y)"
¿Qué es todo esto?
(betareducción y deltareducción:página 34 del libro de Coq)

[ishinay]

Puedo preguntar cúanto tiempo te llevó hacerla? xD Y sobre todo, cúanto tiempo le llevaría a alguien como nosotros, que no conozca Coq tan a fondo como tú. xD

Pues lo básico me llevó muy poco, media hora como mucho. Pero el teorema Esquema me llevó un poco más. Creo que es el más complicado, porque no es trivial. De todas formas, yo hice las demostraciones paso por paso, sin usar auto e intuition, que eso ahorra tiempo Creo que es recomendable saber lo que se está haciendo antes que probar auto en cada línea a ver si lo resuelve . Pero en un examen si dejan hacerlo también es una opción para salir del paso, no lo niego.
No sé cuánto os puede llevar hacerlo, pero yo creo que para el día 20 es tiempo suficiente.
Pero ya sabéis, si tenéis cualquier duda, planteadla y así se irá entendiendo poco a poco.

Ah, no, Susana de mi año no, pero ¿qué Susana eres??? jejeje

[susana]

Ah, no, Susana de mi año no, pero ¿qué Susana eres??? jejeje

Yo acabé la carrera en el 2007, así que hice la asignatura como alumna en el curso 2005/06. Este año di las primeras prácticas de la asignatura, así que podéis preguntarme cualquier duda que tengáis.

Pues yo ya me he quedado en el primer "Lemma th...". Dice:

Código: Seleccionar todo

Lemma th : forall x y : nat, div2P x y -> div2P (S (S x )) (S y).

en este momento, el primer subobjetivo es 2 * Sy=S(Sx).
En esta situación:

x:nat
y:nat
H0:2*y=x \/ 1+2*y=x
H:2*y=x
===============
2*Sy = S(Sx)

¿Cómo que "el primer subobjetivo es 2*Sy=S(Sx)?? Antes tendrás que haber hecho algo como deltareducción y betareducción ¿no? y si haces "intros" el resultado no es el que se muestra, que yo no veo por ningún lado un:

Código: Seleccionar todo

1+2*Sy=S(Sx)

que sería la primera parte de la OR al unfoldear y betareducir "div2P (S(x)) (S y)"
¿Qué es todo esto?
(betareducción y deltareducción:página 34 del libro de Coq)

Efectivamente, para obtener ese subobjetivo hay que hacer algunas cosas antes. Vas por buen camino con respecto a lo que comentas de "unfoldear" div2P. Usando tres tácticas sencillas más (de las que expliqué casi el segundo día de clase) llegas al subobjetivo que se indica en el enunciado

[ishinay]

Hola, Susana. Ahora ya sé a ciencia cierta quién eres, como que nos conocemos. Con esto añado que tú no eres EN ABSOLUTO un ejemplo de relación alumno-asignatura

Yo ya aprobé MD2 el año pasado. Lo que preguntaba lo preguntaba para demostrar que, como siempre, las exposiciones de Freire siguen siendo una puta mierda y que el enunciado ese deja bastante que desear. ¿Podrías echarnos una mano y aclarar un poco la práctica, teniendo en cuenta que el resto de gente no tenemos mucha idea?
Lo haría yo, pero creo que me costará muchísimo y estoy seguro que tú lo harías 100 veces mejor que yo.
¿A qué me refiero con "aclaraciones"? El decir "en este momento..." es una trola, ya que hay que hacer cosas para llegar a ello... pues eso
Muchas gracias!

[susana]

Es cierto que esa frase es un poco confusa, igual se entendía mejor si pusiese que después de una serie de pasos llegamos a ese subobjetivo o algo así, pero el resto de la práctica creo que se entiende bien.

Otra frase que a lo mejor no entendéis del todo, para el teorema compr pone:
"Usaremos ahora el resultado Esquema haciendo la eliminación de x como nat pero, en lugar de usar el esquema de inducción estandar (nat ind), usando
justamente este nuevo."

Como sabéis (o eso espero! jeje), cuando hacéis elim H lo que estáis usando es el principio inductivo del tipo inductivo que estáis eliminando. Es decir, si T es un tipo inductivo (de esos que tienen constructores, vamos), T_ind es el principio inductivo que sirve para probar teoremas sobre el tipo T. El típico ejemplo es el del tipo nat, y nat_ind es el principio inductivo de toda la vida: pruebas lo que quieres demostrar para el 0, pruebas que si se cumple para n también se cumple para S(n) y ya está la demostración para todo n. Se cumple para 0 -> se cumple para 1 (1 = S (0)) -> se cumple para 2 (2 = S (S(1))) ->...-> se cumple para todo n.

En el caso de la práctica el tipo inductivo que utilizamos sigue siendo nat, pero nat_ind no nos vale para hacer las demostraciones, ya que la división entera entre 2 no se comporta igual para los impares que para los pares. Por tanto, no se puede hacer una demostración que implique esta división entre 2 con el principio inductivo de toda la vida, porque que se cumpla para el 2 no significa que se cumpla para el 3. Entonces la idea es utilizar otro principio inductivo que tenga en cuenta esto. Demuestras que se cumple para el 0, demuestras que se cumple para el 1 y demuestras que si se cumple para n, se cumplirá para S(S(n)). Entonces si demuestras todo esto, demostrarás que se cumple para todo n. Si se cumple para 0-> se cumple para 2 (2 = S(S(2))) -> se cumple para 4 ...-> se cumple para todos los pares y lo mismo para los impares: si se cumple para 1-> se cumple para 3 -> ...
Esta es la idea por la que es necesario utilizar otro principio inductivo que no sea el "de toda la vida".

Al principio este principio inductivo se admite como probado (ponéis Admitted) y luego lo tendréis que intentar demostrar. Yo creo que es la demostración más compleja, por eso recomiendo que la dejéis para el final.

Entonces para demostrar compr lo que tenéis que hacer es utilizar ese nuevo principio inductivo en lugar de nat_ind.

[SeñorAl]

Una pregunta que tengo:
Si en una hipotesis tengo H:2*y = x,
Como puedo hacer para que en el objetivo me sustitya la donde aparezca la x por 2*y?
porque el rewrite sustitye donde este un 2*y por x.
Gracias

Vale, ya cai yo solito....

Una cosa Susana... Lo que importa es demostrarlo, no?
pq a mi me ocupo creo q 8 sentencias mas... y no 3 como a ti...(uno q no es tan weno... )