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

Subforo de asignaturas del curso 2008-09.

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

Notapor jpuig » Vie, 16 Ene 2009 20:15

Aquí llego yo :lol:

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.
jpuig
Rakanishu
 
Mensajes: 11
Registrado: Vie, 16 Ene 2009 19:53

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

Notapor Fonso » Vie, 16 Ene 2009 21:52

jpuig escribió:Aquí llego yo :lol:

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 :wink:
Fonso
Rakanishu
 
Mensajes: 12
Registrado: Lun, 12 Ene 2009 14:23

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

Notapor susana » Vie, 16 Ene 2009 22:43

Fonso escribió: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 :wink:


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.
susana
Ojo de Fuego
 
Mensajes: 361
Registrado: Jue, 27 Nov 2008 17:05

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

Notapor javicha » Dom, 18 Ene 2009 11:29

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!!
javicha
Rakanishu
 
Mensajes: 15
Registrado: Lun, 12 Ene 2009 11:11

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

Notapor susana » Dom, 18 Ene 2009 12:44

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 ;)
susana
Ojo de Fuego
 
Mensajes: 361
Registrado: Jue, 27 Nov 2008 17:05

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

Notapor javicha » Dom, 18 Ene 2009 12:48

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!!!
javicha
Rakanishu
 
Mensajes: 15
Registrado: Lun, 12 Ene 2009 11:11

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

Notapor Fonso » Dom, 18 Ene 2009 13:00

[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? :lol:
Fonso
Rakanishu
 
Mensajes: 12
Registrado: Lun, 12 Ene 2009 14:23

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

Notapor javicha » Dom, 18 Ene 2009 13:10

si!! acabado!!
gracias por la ayuda!!!
javicha
Rakanishu
 
Mensajes: 15
Registrado: Lun, 12 Ene 2009 11:11

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

Notapor susana » Dom, 18 Ene 2009 13:14

javicha escribió:si!! acabado!!
gracias por la ayuda!!!

Para eso estamos ;) (incluso los domingos! jajaja)
susana
Ojo de Fuego
 
Mensajes: 361
Registrado: Jue, 27 Nov 2008 17:05

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

Notapor javicha » Dom, 18 Ene 2009 15:34

por cierto, como se entrega la práctica? se manda por correo a Freire? se va a habilitar algún directorio?
javicha
Rakanishu
 
Mensajes: 15
Registrado: Lun, 12 Ene 2009 11:11

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

Notapor jpuig » Dom, 18 Ene 2009 16:29

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
jpuig
Rakanishu
 
Mensajes: 11
Registrado: Vie, 16 Ene 2009 19:53

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

Notapor Fonso » Dom, 18 Ene 2009 16:49

javicha escribió: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.

jpuig escribió: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 :lol:

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.
Fonso
Rakanishu
 
Mensajes: 12
Registrado: Lun, 12 Ene 2009 14:23

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

Notapor susana » Dom, 18 Ene 2009 17:23

jpuig escribió: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
susana
Ojo de Fuego
 
Mensajes: 361
Registrado: Jue, 27 Nov 2008 17:05

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

Notapor Jorge » Dom, 18 Ene 2009 21:46

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.
Please allow me to introduce myself: I'm a man of wealth and taste.
Avatar de Usuario
Jorge
Achmel el Maldito
Veterano de guerra
 
Mensajes: 3441
Registrado: Dom, 01 Oct 2006 17:56
Ubicación: Göteborg / Coruña

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

Notapor susana » Dom, 18 Ene 2009 21:50

Fíjate a ver si escogiste el lado adecuado del or...
Una táctica muy cómoda para las S: ring_simplify
susana
Ojo de Fuego
 
Mensajes: 361
Registrado: Jue, 27 Nov 2008 17:05

AnteriorSiguiente

Volver a FIC Asignaturas 2008-09

¿Quién está conectado?

Usuarios navegando por este Foro: Bing [Bot] y 1 invitado

cron