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

[jpuig]

Aquí llego yo

Lo primero agradecer a Susana su labor, se merece un buen aplauso.
Yo ando aquí rebanándome los sesos en el teorema de div_ent_2, y no consigo demostrar algo que seguro que es una tonteria.
Usando exists n, simplemente tengo que demostrar que div2P n n, si "unfoldeo" y elijo left, tengo que demostrar que 2*n = n, lo que sólo es cierto para 0. No se qué hacer o qué hago mal...

Gracias por la ayuda.

[Fonso]

Aquí llego yo

Lo primero agradecer a Susana su labor, se merece un buen aplauso.
Yo ando aquí rebanándome los sesos en el teorema de div_ent_2, y no consigo demostrar algo que seguro que es una tonteria.
Usando exists n, simplemente tengo que demostrar que div2P n n, si "unfoldeo" y elijo left, tengo que demostrar que 2*n = n, lo que sólo es cierto para 0. No se qué hacer o qué hago mal...

Gracias por la ayuda.

Pues la solución es cambiar el exists. Es evidente que div2P n n solo se cumple para n = 0, así que no puedes demostrarlo para cualquier n. La clave del tema esta en utilizar un teorema anterior

[susana]

Pues la solución es cambiar el exists. Es evidente que div2P n n solo se cumple para n = 0, así que no puedes demostrarlo para cualquier n. La clave del tema esta en utilizar un teorema anterior

No podría haberlo dicho mejor Así que efectivamente tienes que encontrar ese p que cumple que div2P n p para todo n. Fíjate que no puede ser n. div2P x y es un predicado que es cierto cuando y es la división entera entre 2 de x. Es decir, tú estás diciendo que div2P n n es cierto para todo n. Esto no es cierto, ya que la división entera entre 2 de 11 es 5, por ejemplo. En este caso div2P 11 5 es cierto. div2P 11 11 no lo es.

Así que como bien dice Fonso, la clave es entender bien qué se ha demostrado en el lema anterior y actuar en consecuencia.

[javicha]

hola a todos!
estoy atascadisimo en el teorema evenodd, hago intros y ya no se como abordarlo.Tengo lo siguiente:

n:nat
y mi objetivo es: n=0 \/ n=1 \/ (exists p:nat, n= S(S(p)))

No se si es porque estoy currando el domingo por la mañana o porque no tengo ni idea de coq (más bien esto último), pero probé con elim n, left, right... y no consigo avanzar nada, me quedan demostraciones imposibles tipo 0=S(S(0) o 0=1. No soy capaz de llegar ni al punto al que comentó Fonso en el foro.

A ver si alguien me puede orientar por donde tirar, que sólo me quedan por demostrar los dos últimos.

Gracias!!

[susana]

Esta demostración es larga, vas haciendo elims, left, rights quedándote con la parte que puedes demostrar y demostrándola. Parece que va a ser un camino sin fin, porque lo tienes que hacer varias veces, pero al final se acaba demostrando.

La idea para estas demostraciones en la que tienes un or es que, si no sabes con seguridad qué lado demostrar, el izquierdo o el derecho, intentes sacar todo el partido que puedas de las hipótesis que tengas en el contexto y que todavía no hayas usado. Es decir, sacar la máxima información de ellas para poder escoger el lado correcto para demostrar.

Para que te podamos ayudar, lo mejor es que indiques en qué punto estás atascado, es decir, qué tienes en tu contexto y qué tienes que demostrar. Mejor pon un punto donde el objetivo no sea ni 0=S(S(0) ni 0=1, ya que si llegas a estos puntos es que no has tomado la elección correcta en los "or".
Para poder copiar y pegar fácilmente los objetivos que tienes, si no te deja copiar y pegar la consola directamente, prueba a ir al menú Queries, y dale por ejemplo a Check. Ahí en vez de Check escribe Show y en el siguiente recuadro pon 1 para que te muestre el objetivo 1, el 2 para que te muestre el subobjetivo 2, etc tantos como subobjetivos tengas que demostrar, y dale a OK. Te mostrará el contexto y el objetivo, cópialo y pégalo aquí. Así será más fácil guiarte

[javicha]

aaahh! no sabia como copiarlo xDDDD. joer, eres un libro abierto susana, asi da gusto, que resuelves dudas hasta los domingos.
bueno, pues el caso es que aplico induccion en n, y tras resolver para el caso inicial 0, me queda esto:


subgoal 1 is:

n : nat
IHn : n = 0 \/ n = 1 \/ (exists p : nat, n = S (S p))
============================
S n = 0 \/ S n = 1 \/ (exists p : nat, S n = S (S p))


Voy a romperme un poco la cabeza con las pistas que me acabas de dar, a ver si consigo ir sacándolo poco a poco, que es el último que me queda.
Y repito, muchas muchas gracias por la ayuda!!!

[Fonso]

[quote="javicha"]
subgoal 1 is:

n : nat
IHn : n = 0 \/ n = 1 \/ (exists p : nat, n = S (S p))
============================
S n = 0 \/ S n = 1 \/ (exists p : nat, S n = S (S p))

quote]

Pues en este caso yo tiraría por el lado de la derecha, (exists p : nat, S n = S (S p)). Una vez ahí, toca lo de siempre, buscar un p que cumpla S n = S (S p) e introducirlo con exists. Es bastante evidente cual es ese p ¿no?

[javicha]

si!! acabado!!
gracias por la ayuda!!!

[susana]

si!! acabado!!
gracias por la ayuda!!!

Para eso estamos (incluso los domingos! jajaja)

[javicha]

por cierto, como se entrega la práctica? se manda por correo a Freire? se va a habilitar algún directorio?

[jpuig]

Hola de nuevo, estoy atascado en el Lemma de evenodd y no se cómo demostrar lo siguiente: n = S (n - 1), qué se os ocurre?
Además de ésto, en el div2_le, tampoco se me ocurre cómo demostrar: div2 (S n) <= S n

[Fonso]

por cierto, como se entrega la práctica? se manda por correo a Freire? se va a habilitar algún directorio?

Pués creo recordar que Freire dijo en clase que le enviásemos un mail indicando claramente en el asunto que se trata de la práctica de MD2.

Hola de nuevo, estoy atascado en el Lemma de evenodd y no se cómo demostrar lo siguiente: n = S (n - 1), qué se os ocurre?
Además de ésto, en el div2_le, tampoco se me ocurre cómo demostrar: div2 (S n) <= S n

Respecto a evenodd, sería bueno que nos dijeses que hipótesis tienes; a lo mejor Susana puede demostrar n = S (n - 1) así a pelo, pero a mí no se me ocurre como

Y lo de div2 (S n) <= S n, pues expliqué en un post anterior como lo resolví. No sé si habrá una forma más rápida de hacerlo, pero yo lo que hice fué introducir una hipótesis en la que decía que div2 (S n) <= S n es lo mismo que div2 (S n) < S n ó div2 (S n) = S n. A partir de eso, no es muy difícil acabar la demostración.

[susana]

Hola de nuevo, estoy atascado en el Lemma de evenodd y no se cómo demostrar lo siguiente: n = S (n - 1), qué se os ocurre?
Además de ésto, en el div2_le, tampoco se me ocurre cómo demostrar: div2 (S n) <= S n

Sobre lo primero, no es verdad que forall n, n= S(n-1). Fíjate que para n=0, la resta en los números naturales en Coq está definido de forma que 0-1=0, por lo que no se cumpliría que 0 = S (0-1), ya que S(0-1)=S 0 = 1. Por lo tanto, ese objetivo sólo se podrá demostrar si en tu contexto tienes alguna hipótesis de la que puedas deducir que n no es cero.

Con respecto a div2_le, si bien es cierto que se puede demostrar usando la inducción normal, es más recomendable que uséis Esquema para demostrar los teoremas y lemas que contienen a div2. De esta forma tendréis tres subobjetivos, que se convierten en cosas más fáciles de demostrar si utilizáis la táctica simpl div2:
- Uno para el 0, donde div2 0 = 0
- Uno para el 1, donde div2 1 = 1
- Otro para S (S n)), donde div2 (S (S n)) = S (div2 n).


Si aplicáis la inducción normal sólo tendréis dos subobjetivos pero más difíciles, ya que:
- div2 0 se puede simplificar a 0
- sin embargo el otro subobjetivo donde aparece div2 (S n) no se puede simplicar

EDITO: Las simplificaciones se hacen de acuerdo con la propia definición de la función div2, donde como veis hay 3 casos, 0, 1 y S (S n). Así, simpl div2 lo que hace es aplicar esa definición. Sin embargo, no sabe evaluar div2 (S n) ya que no encaja con ningún patrón del match de la función

[Jorge]

Después de esto no me va a respetar ni el tato, pero es que estoy muy perdido de dios y prefiero preguntar y pasar vergüenza a estar dos días dando vueltas.

Todavía estoy peleándome con th, y he llegado a esta situación:

Código: Seleccionar todo

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


Tengo la sensación de que la vida sería más fácil si supiese unfoldear S, porque parece jodidamente trivial.

Gracias y no me tiréis tomates.

[susana]

Fíjate a ver si escogiste el lado adecuado del or...
Una táctica muy cómoda para las S: ring_simplify