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

[Fer]

Creo que es política de este foro que no se den las soluciones a las prácticas.

Lo que intentamos evitar es que la gente ande copiándose las prácticas y además, no aprendiendo nada. Además, nos evitamos problemas con los profesores. Si la gente postea sus dudas, y entre todos se resuelve, se aprende. Si uno lo hace y los demás copian, no. Y bueno, para explicar las cosas de la práctica, claro que se puede postear código, pero no todo tal cual. Mejor a poder ser, pequeños cachos y tal.


Bue, me enrollo, pero supongo que sabréis a lo que me refiero.

[Fonso]

¡Muchas gracias!

Es realmente frustrante tener delante de las narices algo tan obvio y no saber como se demuestra... Ahora estoy peleándome con div_ent_2; doy por supuesto que en este teorema también hemos de utilizar el esquema inductivo que definimos previamente ¿es correcto? Es que estoy llegando a objetivos realmente absurdos, como que 3=1, así que debo estar haciendo algo mal.

Gracias por la ayuda.

[susana]

Ahora estoy peleándome con div_ent_2; doy por supuesto que en este teorema también hemos de utilizar el esquema inductivo que definimos previamente ¿es correcto? Es que estoy llegando a objetivos realmente absurdos, como que 3=1, así que debo estar haciendo algo mal.

Este teorema es muy sencillo si observáis bien lo que os piden y lo que tenéis demostrado hasta este momento.
Ojo, no puedes usar Esquema! Porque Esquema es un principio de inducción alternativo a nat_ind, que se usa cuando quieres demostrar algo que es una Prop. En este caso tienes que demostrar algo que es un Set, por lo que deberías usar un Esquema2 que fuese alternativo a nat_rec. Si bien hacer esto es fácil, demostrar ese Esquema2 es mucho más difícil, así que desaconsejo ir por ese camino... Y obviamente menos aún por el camino de la inducción de toda la vida, como comentaba en un post anterior, en el que decía que para demostrar cosas de esta práctica, al comportarse de forma diferente los pares y los impares, no funciona bien.

Así que para este teorema, repito: fijaos bien qué os pide y qué tenéis demostrado. Cuando te des cuenta, verás que es mucho más sencillo!

[jotha]

Estoy intentando hacer lo que tu me comentaste de pensar en nuevas hipotesis, pero voy a dejar para mas adelante el "Esquema", ahora estoy con el "compr" y llege a lo siguiente:

2 subgoals
x:nat
IHx: div2P x (div2 x)
H: 2 * div2 x = x
-------------------------------------(1/2)
1+2*div2(Sx)=Sx


-------------------------------------(2/2)
1+2*div2x=x->div2P(Sx)(div2(Sx))

Ahora me planteo introducir la hipotesis de que "si x es igual a 2*div2x, quiere decir que es un numero par, por lo que su sucesor sera
impar, con lo cual Sx=2*div2Sx+1".

Ya lo he tanteado, pero se me presenta el problema de demostrar mi hipotesis, yo se que es cierta, pero no se como decirle al coq q lo es.

No se si voy por buen camino o no.

Gracias por la ayuda.

[susana]

Creo que llegaste ahí aplicando la inducción normal, ¿es así? Si usas Esquema, como te indica la práctica, creo que ya no tendrás ese problema de distinguir entre pares e impares.

[InaDmO]

Pues yo no encuentro manera. Estoy en el th y llego hasta donde dice en la practica, luego hago el rewrite de la hipotesis en el objetivo, pero ahi me quedo atascado:

...
------------------
2*S y = S(S(2*y))

¿como y cuando se supone que se usa "ring"? pq a mi no me hace absolutamente nada y supongo que sera que no lo estoy aplicando al objetivo correcto.

PD: con "auto" me sale la demostracion.. pero claro...xD

[susana]

Pues yo no encuentro manera. Estoy en el th y llego hasta donde dice en la practica, luego hago el rewrite de la hipotesis en el objetivo, pero ahi me quedo atascado:

...
------------------
2*S y = S(S(2*y))

¿como y cuando se supone que se usa "ring"? pq a mi no me hace absolutamente nada y supongo que sera que no lo estoy aplicando al objetivo correcto.

PD: con "auto" me sale la demostracion.. pero claro...xD

¿Tienes cargada la librería? (Require Import ArithRing)
Ring, por explicarlo fácilmente, lo que hace es resolver ecuaciones usando propiedades de sumas, multiplicaciones, propiedades distributivas, asociativas... en un anillo (en este caso para los naturales). Sobre ese subobjetivo debería funcionar (si no me equivoco)
Y ojo: usar auto es una solución totalmente válida también!
Si acabáis con auto está bien demostrado... otra cosa es que queráis detallar más y hacer la demostración más explícita (indicando que lemas aplicar o esas cuestiones)

[InaDmO]

En el enunciado pone "Require Export ArithRing.", pero vamos no me funciona de ninguna de las dos maneras:

Definition div2P (x y:nat):Prop := 2 * y = x \/ 1 + 2 * y = x.
Require Import ArithRing.
Lemma th: forall x y:nat, div2P x y -> div2P (S (S x)) (S y).
Proof.
...
rewrite <- H0. // Siendo H0:2 * y = x
ring.

y no hace absolutamente nada, es decir, no da error, se ejecuta pero no modifica nada. He probado a simplificar el subobjetivo antes de aplicar ring, pero mas de lo mismo. ¿ideas?

[susana]

En el enunciado pone "Require Export ArithRing."

Cierto, me confundí

Pues no sé por qué no te va. Si quieres pásame el código por MP y lo miro, a ver si saco alguna conclusión, pero en teoría se debería hacer así...

EDITO: De todas formas me extraña bastante, porque yo creo que ring o funciona o falla (ahora mismo no estoy 100% segura).

[jotha]

Pues a mi en esa misma situacion es "ring" el que me resuelve, como dice susana.

Yo hago el "Require Export ArithRing." antes del "th" y me funciona perfectamente.

A mi no se me ocurre xq puede no funcionar.

[jotha]

He seguido tu consejo de aplicar el Esquema en vez de la induccion normal en "compr".

El problema es que no se como resuelvo los dos casos base que me plantea el Esquema P0(div2P x 0) y P1(div2P x 1).

No se, este sera el camino, pero aun no lo veo.

[InaDmO]

Arreglado. Lo he probado desde linux y no hay problema.

[InaDmO]

He seguido tu consejo de aplicar el Esquema en vez de la induccion normal en "compr".

El problema es que no se como resuelvo los dos casos base que me plantea el Esquema P0(div2P x 0) y P1(div2P x 1).

No se, este sera el camino, pero aun no lo veo.

Facil, prueba a hacer unfold de div2P o div2

[susana]

Por poner otro ejemplo de cómo resolver la duda de Fonso:

Código: Seleccionar todo

Goal(forall n:nat, 1+2* (div2 n) = n -> 2*div2 n +3 = n+2).
intros.
replace (2* div2 n + 3) with (1 + 2* div2 n + 2) by ring.
rewrite H.
reflexivity.

La táctica replace hace lo mismo que cut. Si sólo pusiésemos replace (2* div2 n + 3) with (1 + 2* div2 n + 2), se generarían dos subobjetivos: en el primero se reemplaza lo que se indica (de forma que ya se podría utilizar directamente el rewrite), y el segundo mandaría resolver esa igualdad. Si usamos replace ... with ... by ring lo que se hace es que se indica que la segunda demostración se puede resolver con la táctica ring (es inmediato que esas dos cosas son iguales), por lo que simplemente reemplaza (2* div2 n + 3) con (1 + 2* div2 n + 2) en el subobjetivo y se puede continuar con la demostración.

[jotha]

He seguido tu consejo de aplicar el Esquema en vez de la induccion normal en "compr".

El problema es que no se como resuelvo los dos casos base que me plantea el Esquema P0(div2P x 0) y P1(div2P x 1).

No se, este sera el camino, pero aun no lo veo.

Facil, prueba a hacer unfold de div2P o div2

No si eso ya lo he probado, el problema es q tras hacer eso el goal es: 2*0=x \/1+2*0=x

y no se como resolverlo, ya q creo q no se puede decidir, si fuesen valores concretos si, pero asi no, o eso creo repito.