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

[esramar]

La practica hay que hacerla toda o con un porcentaje determinado ya te dejan presentarte al examen¿?

[susana]

La practica hay que hacerla toda o con un porcentaje determinado ya te dejan presentarte al examen¿?

Venga... quedan unos días y si te pones no es tan difícil

[jpuig]

La práctica creo recordar que tiene que ser compilable en Coq no? Eso quiere decir que simplemente nuestro fichero .v no tiene que dar errores al compilarlo con coqc? O es necesario hacer algo más? Gracias

[susana]

La práctica creo recordar que tiene que ser compilable en Coq no? Eso quiere decir que simplemente nuestro fichero .v no tiene que dar errores al compilarlo con coqc? O es necesario hacer algo más? Gracias

Exacto, comprueba que has demostrado todo, y no has dejado ningún Admitted por ahí.

[Jorge]

Gracias Susana, era justo lo que necesitaba

Ahora me he atascado en lo que yo supongo es también una tontería...

Código: Seleccionar todo

[...]
H1 : 2 * div2 n = n
_____________________ (1/2)
2 * div2 (n + 2) = n + 2


¡Esto se demuestra sólo! ¿Cómo le digo a Coq que tome n como n+2?

[susana]

Gracias Susana, era justo lo que necesitaba

Ahora me he atascado en lo que yo supongo es también una tontería...

Código: Seleccionar todo

[...]
H1 : 2 * div2 n = n
_____________________ (1/2)
2 * div2 (n + 2) = n + 2


¡Esto se demuestra sólo! ¿Cómo le digo a Coq que tome n como n+2?

Hay dos cosas que aclarar aquí. H1 lo que te dice es que para un n determinado, 2*div2 n = n. No te está diciendo que forall n:nat, 2*div2 n = n. En el segundo caso como bien dices se podría hacer que n valiese n+2 y ya estaría demostrado. Pero H1 en este caso no es ninguna función que acepte parámetros, así que no puedes cambiar ahí la n por n+2.
Lo que sí te permite H1 es, si consigues poner en el objetivo algo que tenga 2*div2 n, entonces podrías sustituir con el rewrite esa expresión por n.

Y esto es lo malo de usar la táctica ring_simplify... (todo tiene su lado malo, jeje). Al hacer ring_simplify y eliminar tus odiadas S, tienes div2 (n+2) en vez de div2 ( S (S n)). Esto te impide usar la táctica de simpl div2, ya que div2 lo sabe simplicar cuando tiene como parámetro 0, 1 ó S (S n) (fíjate en como está definida la función).

[Jorge]

Perfecto, ya tengo compr liquidado ¡Muchísimas gracias!

[Hadrian]

Estoy con la práctica a vueltas y la verdad es que estas ocho páginas que lleva el hilo me han ayudado mucho. Gracias!!!

[nenita]

Hola a todos:
Alguien sabe que significa eso de
HInt Resolve aux1 aux2??
yo lo he obviado pero pero me pregunto ahora si esta sentencia la hay que incluir en el fichero, si es así no tengo ni idea de para que sirve.

[SeñorAl]

Lo que hace Hint Resolve es que cuando hagas un auto, coq tambien pueda valerse de esas tacticas para resolver el objetivo. Deja la instruccion puesta
por si luego te interesa (en el peor caso no te hara falta, pero no te cuesta nada...)

[esramar]

La practica hay que hacerla toda o con un porcentaje determinado ya te dejan presentarte al examen¿?

Venga... quedan unos días y si te pones no es tan difícil

mi problema es que el Esquema no sale, de ninguna de las maneras, no se me ocurre LA hipotesis que me pueda ayudar, el resto esta hecho (tengo un par de problemillas con los aux, pero no creo que me molesten mucho) pero lo de
Esquema no sale... y no se si la practica te la cuenta como bien estando incompleta.

Edito: no puede haber nada con Admitted? porque yo tengo los ultimos tres teoremas con Admitted...

[susana]

mi problema es que el Esquema no sale, de ninguna de las maneras, no se me ocurre LA hipotesis que me pueda ayudar, el resto esta hecho (tengo un par de problemillas con los aux, pero no creo que me molesten mucho) pero lo de
Esquema no sale... y no se si la practica te la cuenta como bien estando incompleta.

Realmente LA hipótesis no es nada obvia, te escribo un MP con más detalles

no puede haber nada con Admitted? porque yo tengo los ultimos tres teoremas con Admitted...

No, no puede haber nada como Admitted. Admitted significa que lo das por supuesto, pero realmente no está demostrado. No es una táctica que te resuelva el objetivo. Para saber que algo está correctamente demostrado tiene que poner "Proof completed" y se acaba la demostración con Qed.

[InaDmO]

Estoy con el div2_le y me he quedado atascado. Bueno, pues usando Esquema y luego añadiendo con cut la hipotesis que propone Fonso (div2( S n) <= S n <-> (div2 (S n) < S n \/ div2 (S n) = S n)) llego a algo de lo que no tengo remota idea de por donde salir. He probado de todo.

n : nat
H : div2 n <= n
============================ (1/2)
(div2 (S n) < S n \/ div2 (S n) = S n -> div2 (S n) <= S n) ->
div2 (S (S n)) <= S (S n)

que tras los intros se convierte en:

n : nat
H : div2 n <= n
H0 : div2 (S n) < S n \/ div2 (S n) = S n -> div2 (S n) <= S n
============================ (1/2)
div2 (S (S n)) <= S (S n)

he probado de todo y no llego absolutamente a nada.

[NuSaRi6]

Hola!!!

Estoy atascado en evenodd!!!Llegado al punto que muestro abajo no sé seguir!!!!A ver si me podeis ayudar!!

Gracias!!!

1 subgoal

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

[esramar]

Estoy con el div2_le y me he quedado atascado. Bueno, pues usando Esquema y luego añadiendo con cut la hipotesis que propone Fonso (div2( S n) <= S n <-> (div2 (S n) < S n \/ div2 (S n) = S n)) llego a algo de lo que no tengo remota idea de por donde salir. He probado de todo.

n : nat
H : div2 n <= n
============================ (1/2)
(div2 (S n) < S n \/ div2 (S n) = S n -> div2 (S n) <= S n) ->
div2 (S (S n)) <= S (S n)

que tras los intros se convierte en:

n : nat
H : div2 n <= n
H0 : div2 (S n) < S n \/ div2 (S n) = S n -> div2 (S n) <= S n
============================ (1/2)
div2 (S (S n)) <= S (S n)

he probado de todo y no llego absolutamente a nada.

seguir por ese camino no se, pero creo que el div2_le es mas facil simplificando expresiones y demostrandolas con auto with arith.