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

[susana]

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

Prueba con rewrite <- H

[susana]

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... )

Jajaja. Por supuesto, lo que importa es demostrarlo. Y lo que dije que eran 3 sentencias más era llegar al subobjetivo, no demotrarlo todo
Además, yo soy más partidaria de las demostraciones largas pero con pasos simples (que se entienda bien qué se hace en cada paso) y no acabar la demostración en menos pasos.

[SeñorAl]

Muxas gracias. Al final me habia venido la inspiracion!!, ahora estoy peleandome con el compr, jejeje
una cosa, Susana, podrias poner tu correo, para alguna pregunta mas concreta sobre codigo, q igual no es apropiado ponerla aqui?
Gracias

[Fer]

una cosa, Susana, podrias poner tu correo, para alguna pregunta mas concreta sobre codigo, q igual no es apropiado ponerla aqui?
Gracias

Los MPs (mensajes privados) son tus amigos.

[César]

Da igual que pongáis trozos grandes de código, el año pasado en el foro (moderado por el profesor) se pegaban trozos enormes de código y no hubo ningún problema. Con que sepáis por qué se hacen las cosas...

[esramar]

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.

me referia a que no se ni por donde empezar a enfocarla, pero bueno, prefiero ir matandome yo y plantear dudas concretas y de paso me sirve para ir estudiando la asignatura. el problema es que ahora estoy enferma (y como no saben que me pasa, tengo para rato), asi que voy a empezar a perderme una de clases que a ver como me las voy apañando. si el libro de coq es tan util como decis, espero no tener problemas.


EDITO: el examen final, mas o menos, ¿como es?

[susana]

No puedo responderte exactamente a eso, porque yo no lo voy a poner Pero por lo que sé se está intentando que la parte de coq se pueda hacer en algún laboratorio. Por tanto es posible que el profesor os tantée para saber qué día os vendría bien, porque debería ser antes del examen oficial. Es decir, se necesita un día que venga bien a todo el mundo y sea antes de los exámenes... La idea es que se haga práctico, en varias tandas si es necesario (se convocaría a los alumnos a diferentes horas, por ejemplo un grupo que haga el examen a las 10 y otro a las 12 o algo parecido, o por la tarde, no sé), pero el mismo día todos. Y después faltaría hacer la parte de combinatoria.

[esramar]

Me referia mas que nada a eso, a que parte iba por practica, que parte iba por teoria... por tener una idea.

¿entonces, el pdf ese va a ser el enunciado final de la practica?

[Hadrian]

Freire dijo este jueves en clase que en una semana, más o menos, estará decidido si el examen será sobre el ordenador y cuando será la fecha, porque cómo tiene que ser antes de los exámenes, es díficil encontrar un día, ya que hay clases. Una opción, que no sé si está barajando, es que se haga el sábado, como ya hizo Valderruten con el examen práctico de Algoritmos.

[susana]

Me referia mas que nada a eso, a que parte iba por practica, que parte iba por teoria... por tener una idea.

¿entonces, el pdf ese va a ser el enunciado final de la practica?

Sí, el pdf es el enunciado de la práctica, que hay que entregar antes del 20 de enero (creo que lo avisó en clase), es obligatorio entregarla para poder presentarse al examen.
Y lo de qué parte será por práctica y qué por teoría: la parte de combinatoria será en papel, y la de coq será en ordenador si se puede, y si no, en papel. Es lo que supongo, pero todo esto mejor lo comentáis con el prof. Freire. Comentadle a él lo del sábado, por si os va mejor ese día.

Yo os ayudo y resuelvo las dudas que queráis

[jotha]

Buenas a todos, de puta madre por parte de los "jefes del web" lo del foro, el año pasado se resolvieron muchas dudas con un foro similar.

Yo ya he conseguido demostrar el primer teorema y si alguien lo necesita, no me importaria colgar la forma en que lo hice yo y explicarlo.

Yo estoy enganchado en el "Esquema", llego a un punto del que no doy salido, aplico induccion sobre "n" y me queda en el 1ºsubgoal P0 q es trivial, pero despues con P(Sn) no se seguir, se q con P0 tengo P2 y con P1 tengo P3, es decir, a demostrar tengo Pn y P(Sn), pero por mas vueltas que doy no resuelvo.

Ahh, tb tengo resuelto el "th´", en el cual el razonamiento es similar al "th".

Si alguien puede echarme un cable lo agradeceria.

Saludos a todos.

[susana]

Yo ya he conseguido demostrar el primer teorema y si alguien lo necesita, no me importaria colgar la forma en que lo hice yo y explicarlo.

Creo que es mejor no colgar la solución y que todo el mundo lo intente hacer por su cuenta. En el examen os mandarán resolver cosas similares, así que un poco de práctica (nunca mejor dicho) siempre está bien.

Yo estoy enganchado en el "Esquema", llego a un punto del que no doy salido, aplico induccion sobre "n" y me queda en el 1ºsubgoal P0 q es trivial, pero despues con P(Sn) no se seguir, se q con P0 tengo P2 y con P1 tengo P3, es decir, a demostrar tengo Pn y P(Sn), pero por mas vueltas que doy no resuelvo.

Creo que este teorema es el más difícil de demostrar, ya que es necesario introducir una hipótesis en la demostración que no está inicialmente. Piensa qué hipótesis te ayudaría a resolver el teorema más fácilmente e introdúcela. Al hacer eso tendrás que demostrar el objetivo original, que será más fácil ya que puedes hacer uso de la hipótesis, y después demostrar que esa hipótesis que introduces realmente se cumple. Lo difícil es saber qué introducir que hará que sea más fácil la demostración...

Ahh, tb tengo resuelto el "th´", en el cual el razonamiento es similar al "th".

Al poner la demostración de th' después de aux1 y aux2 entiendo que significa que es deseable que se usen estos lemas en la demostración

[jotha]

Pues creo que poner el codigo y discutir distintas formas de resolver un mismo problema es mas que util para entender como se hacen las cosas y por qué, ya q cunatos mas ejemplos ves y distintas formas de reolverlos acabas entendiendo como hacerlo y generalizarlo a otros problemas, es el principio de las RNAs, y en mi caso, funciona perfectamente, prueba de ello es el foro utilizado el año pasado, en el cual se resolvieron muchas dudas.

La idea no es copiar el codigo, sino ver como se hace y razonarlo uno mismo.

Lo de introducir una hipotesis esta bien, pero no se como hacerlo ni tengo claro cual.

Por ultimo, en cuanto al th´tienes razon del uso de los aux1 y 2, facilitan la demostracion, se presupone su uso.

Gracias por todo e invitar a la gente a q use este foro y comente sus dudas y exponga sus planteamientos, razonamientos y resoluciones a la practica.

[Fonso]

Buenas a todos,

Parece que el que más el que menos va sacando el tema este de la práctica. Una vez superado el susto inicial tras leer el enunciado, y siguiendo un poco las pistas que Susana ha dejado por aqui (gracias de corazón, esto no hay por donde cogerlo sino) he ido avanzando en las demostraciones, pero me he atascado al final de la demostración de compr, y la verdad es que me siento un poco estúpido:

Código: Seleccionar todo

1 subgoal
x : nat
n : nat
H : 1 + 2 * div2 n = n
_______________________ (1/1)
2 * div2 n + 3 = n + 2

Si no he metido la pata, el objetivo es la hipótesis sumando 2 a cada lado del signo igual, pero no se como leches decirselo a Coq A lo mejor es una estupidez, pero la verdad es que me he atorado ahí...

Si alguien sabe como hacerlo, agradecería la información.

A cuidarse!

[susana]

Creo que es política de este foro que no se den las soluciones a las prácticas. Está claro que siempre es bueno saber muchas formas de solucionar las cosas, ya sea en la práctica de operativos, programación o IS, pero también hay que tener cuidado con quien no quiere comparar formas de resolución, sino copiar las prácticas
Todo lo que sea exponer diferentes métodos está bien. Por ejemplo, tal y como yo demostré compr, no me llegaba a ese objetivo, así que siempre es bueno saber cómo lo hicieron otros y plantearse las mismas dudas que ellos.
Ahora mismo, por ejemplo, dada la duda de Fonso:

Buenas a todos,

Parece que el que más el que menos va sacando el tema este de la práctica. Una vez superado el susto inicial tras leer el enunciado, y siguiendo un poco las pistas que Susana ha dejado por aqui (gracias de corazón, esto no hay por donde cogerlo sino) he ido avanzando en las demostraciones, pero me he atascado al final de la demostración de compr, y la verdad es que me siento un poco estúpido:

Código: Seleccionar todo

1 subgoal
x : nat
n : nat
H : 1 + 2 * div2 n = n
_______________________ (1/1)
2 * div2 n + 3 = n + 2

puedo deciros cómo introducir una hipótesis que no tenéis en vuestra demostración (seguramente hay otras formas de hacerlo, pero esta es la más "pedestre", es decir, no necesitas saber ninguna táctica a mayores de cut, que es la que me interesaba mostrar)
Vamos a intentar demostrar lo que nos plantea Fonso. Uso "Goal" porque es una demostración rapidilla que no me interesa la prueba.

Código: Seleccionar todo

Goal(forall n:nat, 1+2* (div2 n) = n -> 2*div2 n +3 = n+2).
intros.
cut (2 * div2 n + 3 = 1+ 2* div2 n + 2).

Con esa sentencia cut (2 * div2 n + 3 = 1+ 2* div2 n + 2) lo que estoy haciendo es añadiendo esa hipótesis en mi demostración, de manera que ahora tengo dos subobjetivos:

Código: Seleccionar todo

subgoal 1 is:
 
  n : nat
  H : 1 + 2 * div2 n = n
  ============================
   2 * div2 n + 3 = 1 + 2 * div2 n + 2 -> 2 * div2 n + 3 = n + 2


El primer subojetivo añade la hipótesis a la demostración, ahora nuestra demostración será más fácil, ya que podemos hacer un rewrite.

Código: Seleccionar todo

subgoal 2 is:
 
  n : nat
  H : 1 + 2 * div2 n = n
  ============================
   2 * div2 n + 3 = 1 + 2 * div2 n + 2

Y el segundo subgoal será demostrar lo que introducimos, es decir 2 * div2 n + 3 = 1+ 2* div2 n + 2, que es inmediato.