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

[susana]

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.

Ya te contesté por email

[InaDmO]

hum... yo lo que hago es aplicar antes de nada (antes de hacer intro, que creo q tenia problemas) el Esquema y luego a base de unfolds, lefts/roights y reflexivitis pues por lo menos los dos primeros subgoals se resuleven

[InaDmO]

el div_ent_2 y el esquema me los he saltado y estoy ahora con los aux, con un problema igual al que tenia jhota ¿como salgo de aqui:?

x: nat
y: nat
H: 2 * S y = S(S x))
------------------------------
2 * y = x

trasteando solo llego a absurdos como 2*y=0, 2*y=1....

[susana]

hum... yo lo que hago es aplicar antes de nada (antes de hacer intro, que creo q tenia problemas) el Esquema y luego a base de unfolds, lefts/roights y reflexivitis pues por lo menos los dos primeros subgoals se resuleven

Sí, efectivamente ese era el problema.
Si haces intro ya no te "coincide" el lema que tienes que resolver con el final del tipo de Esquema, así que hay problemas si se hace apply Esquema.
La solución es hacer apply Esquema al principio de todo o utilizar elim x using Esquema en caso de hacer intros. Con esta última táctica se dice que se aplique el principio de inducción sobre x, pero en vez de aplicar el usual (nat_ind, ya que x:nat) se indica que se use Esquema en su lugar.

[ishinay]

Sí, efectivamente ese era el problema.
Si haces intro ya no te "coincide" el lema que tienes que resolver con el final del tipo de Esquema, así que hay problemas si se hace apply Esquema.
La solución es hacer apply Esquema al principio de todo o utilizar elim x using Esquema en caso de hacer intros. Con esta última táctica se dice que se aplique el principio de inducción sobre x, pero en vez de aplicar el usual (nat_ind, ya que x:nat) se indica que se use Esquema en su lugar.

Concretamente, ¿cómo es eso de aplicar el principio de inducción? ¿Qué hipótesis tienes y de qué manera se transforman? (por así decirlo) y ¿por qué? es que yo con "induction" no me entero de nada, ni por qué aparecen unas hipótesis dadas ni por qué desaparecen otras cosas ni por qué otras veces es como si fuera un simple "elim".

[susana]

el div_ent_2 y el esquema me los he saltado y estoy ahora con los aux, con un problema igual al que tenia jhota ¿como salgo de aqui:?

x: nat
y: nat
H: 2 * S y = S(S x))
------------------------------
2 * y = x

trasteando solo llego a absurdos como 2*y=0, 2*y=1....

Básicamente lo que tienes es que es cierto que (S(S (2*y))) = S ( S x) (H escrito de otra forma). Y necesitas demostrar 2 * y = x. Parece bastante obvio no? Es decir, la idea es poder demostrar que si S ( n ) = S ( m ) -> n = m, (dos veces seguidas, ya que lo que tenemos en la hipótesis es el siguiente del siguiente).

Lo que quiero decir es que intentéis analizar qué es lo que tenéis como cierto y qué es lo que tenéis que demostrar. Podéis hacer lemas auxiliares sencillitos que os ayuden a hacer la demostración, incluso puede que ya esté hecha y exista un lema que os lo resuelva... (podéis ver la documentación en internet).

[ishinay]

el div_ent_2 y el esquema me los he saltado y estoy ahora con los aux, con un problema igual al que tenia jhota ¿como salgo de aqui:?

x: nat
y: nat
H: 2 * S y = S(S x))
------------------------------
2 * y = x

trasteando solo llego a absurdos como 2*y=0, 2*y=1....

Básicamente lo que tienes es que es cierto que (S(S (2*y))) = S ( S x) (H escrito de otra forma). Y necesitas demostrar 2 * y = x. Parece bastante obvio no? Es decir, la idea es poder demostrar que si S ( n ) = S ( m ) -> n = m, (dos veces seguidas, ya que lo que tenemos en la hipótesis es el siguiente del siguiente).

Lo que quiero decir es que intentéis analizar qué es lo que tenéis como cierto y qué es lo que tenéis que demostrar. Podéis hacer lemas auxiliares sencillitos que os ayuden a hacer la demostración, incluso puede que ya esté hecha y exista un lema que os lo resuelva... (podéis ver la documentación en internet).

¡Anda! ¡Al fín una explicación en la que vislumbro algo realmente claro! Gracias! Esto sí que es realmente aclaratorio y se puede ver cómo enfocar tantos doses y tantos asteriscos. Ahora que sé este "truquito" empezaré a fijarme más en esas cosas, que antes no me daba cuenta.

[susana]

Sí, efectivamente ese era el problema.
Si haces intro ya no te "coincide" el lema que tienes que resolver con el final del tipo de Esquema, así que hay problemas si se hace apply Esquema.
La solución es hacer apply Esquema al principio de todo o utilizar elim x using Esquema en caso de hacer intros. Con esta última táctica se dice que se aplique el principio de inducción sobre x, pero en vez de aplicar el usual (nat_ind, ya que x:nat) se indica que se use Esquema en su lugar.

Concretamente, ¿cómo es eso de aplicar el principio de inducción? ¿Qué hipótesis tienes y de qué manera se transforman? (por así decirlo) y ¿por qué? es que yo con "induction" no me entero de nada, ni por qué aparecen unas hipótesis dadas ni por qué desaparecen otras cosas ni por qué otras veces es como si fuera un simple "elim".

Una respuesta rápida (que me voy a comer, después si quieres la amplío )
Elim aplica el principio de inducción del tipo sobre el que lo aplicas. Es decir, si haces elim x, siendo x:nat, usa nat_ind. Si haces elim H, siendo H:A\/B aplica or_ind. Si haces un check de estos tipos entenderás por qué aparecen los subobjetivos que aparecen. Es como hacer un apply: la parte final de la implicación se unifica con tu objetivo y se generan tantos subobjetivos nuevos como partes izquierdas tenga la implicación del principio de inducción.
Por ejemplo, para nat_ind. Imagínate que tienes que demostrar que todo número natural es mayor que 0.

Código: Seleccionar todo

Goal(forall n:nat, n>=0)

Después de hacer el intro, si haces un elim n (o apply nat_ind, que será lo mismo) te generará dos subobjetivos. Veamos el porqué.

Código: Seleccionar todo

nat_ind
     : forall P : nat -> Prop,
       P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

por lo tanto, al unificar la parte final de nat_ind con nuestro objetivo

forall n:nat, P n
forall n:nat, n>=0

vemos que P n es n>=0, por lo que ahora se generarán dos subobjetivos, uno para la primera parte de la implicación P 0 y otra para la segunda (forall n : nat, P n -> P (S n)) (P ya está unificado, así que para forall P : nat -> Prop no se tiene que generar nada).

Por eso aparecen los dos subobjetivos:
- 0 >= 0 , que es P 0 (recordemos que P n es n>=0, por lo que P 0 es 0>=0)
- forall n : nat, n >= 0 -> S n >= 0, que es (forall n : nat, P n -> P (S n)) con P sustituido.

Cuando se hace elim x using Esquema lo que se hace es utilizar otro principio de inducción.

Como

Código: Seleccionar todo

Esquema: forall P : nat -> Prop,
       P 0 ->
       P 1 -> (forall n : nat, P n -> P (S (S n))) -> forall n : nat, P n

Entonces se generan 3 subobjetivos:
- 0 >= 0 , que es P 0
- 1 >= 0 , que es P 1
- forall n : nat, n >= 0 -> S (S n) >= 0, que es (forall n : nat, P n -> P (S (S n)))


Cuando se hace induction, lo que se hace es aplicar el principio de inducción igual que elim, pero a mayores hace los intros necesarios y sustituye en las hipótesis todo lo necesario (por ejemplo, si en hubiese una hipótesis que tuviese n, para el primer subobjetivo la sustituiría por 0).

[jotha]

He conseguido demostrar el lema aux1, y para hacerlo he necesitado las dos cosillas q dice susana, y lo he implementado con dos lemas mas.

Lemma aux11 : forall y:nat, 2*S y = S(S(2*y)).

Lemma aux12: forall n m:nat, S ( n ) = S ( m ) -> n = m.

Las demostraciones son muy faciles, y con ellos en 3 lineas esta listo el aux1.

[InaDmO]

el div_ent_2 y el esquema me los he saltado y estoy ahora con los aux, con un problema igual al que tenia jhota ¿como salgo de aqui:?

x: nat
y: nat
H: 2 * S y = S(S x))
------------------------------
2 * y = x

trasteando solo llego a absurdos como 2*y=0, 2*y=1....

Básicamente lo que tienes es que es cierto que (S(S (2*y))) = S ( S x) (H escrito de otra forma). Y necesitas demostrar 2 * y = x. Parece bastante obvio no? Es decir, la idea es poder demostrar que si S ( n ) = S ( m ) -> n = m, (dos veces seguidas, ya que lo que tenemos en la hipótesis es el siguiente del siguiente).

Lo que quiero decir es que intentéis analizar qué es lo que tenéis como cierto y qué es lo que tenéis que demostrar. Podéis hacer lemas auxiliares sencillitos que os ayuden a hacer la demostración, incluso puede que ya esté hecha y exista un lema que os lo resuelva... (podéis ver la documentación en internet).

Hasta esa suposicion habia llegado, pero no se como transformar mi objetivo para que sea como la hipotesis, pq si hago replaces luego tengo que demostrar cosas como S(S x) = x, lo cual no es cierto. Me estoy volviendo loco..

[ishinay]

Hasta esa suposicion habia llegado, pero no se como transformar mi objetivo para que sea como la hipotesis, pq si hago replaces luego tengo que demostrar cosas como S(S x) = x, lo cual no es cierto. Me estoy volviendo loco..

Recuerda esto:

Básicamente lo que tienes es que es cierto que (S(S (2*y))) = S ( S x) (H escrito de otra forma). Y necesitas demostrar 2 * y = x. Parece bastante obvio no? Es decir, la idea es poder demostrar que si S ( n ) = S ( m ) -> n = m, (dos veces seguidas, ya que lo que tenemos en la hipótesis es el siguiente del siguiente).

Teniendo:

Código: Seleccionar todo

x: nat
y: nat
H: 2 * S y = S(S x))
------------------------------
2 * y = x

Si previamente has demostrado:

Código: Seleccionar todo

Lemma aux11 : forall y:nat, 2*S y = S(S(2*y)). ### SIGNIFICA: 2*(y+1) = (2*y)+2
Lemma aux12: forall n m:nat, S ( n ) = S ( m ) -> n = m. ### SIGNIFICA: Si (n+1)=(m+1) entonces n=m.

Al hacer "rewrite aux11 in H", obtienes lo primero que dice Susana: H: (S(S (2*y))) = S ( S x)
Si haces 2 veces "apply aux12" como dice Susana, obtienes el objetivo que dice Susana: primero (S (2*y)) = (S x) y después (S(S (2*y))) = S ( S x)
Y ahora ya es trivial

[InaDmO]

si si... lo hice asi y sin problema.

Por cierto, para resolver el Esquema es muy muy facil si sabeis que hipotesis añadir. Una vez hecho parece de niños pequeños.

[susana]

Por cierto, para resolver el Esquema es muy muy facil si sabeis que hipotesis añadir. Una vez hecho parece de niños pequeños.

Cierto, lo que no es tan obvio es la hipótesis a añadir

He conseguido demostrar el lema aux1, y para hacerlo he necesitado las dos cosillas q dice susana, y lo he implementado con dos lemas mas.

Lemma aux11 : forall y:nat, 2*S y = S(S(2*y)).

Lemma aux12: forall n m:nat, S ( n ) = S ( m ) -> n = m.

Las demostraciones son muy faciles, y con ellos en 3 lineas esta listo el aux1.

Así está perfecto. Si no queréis usar el lema aux11 que os propone jotha, podéis recordar lo que os comenté del replace [lo que hay] with [por lo que quieres cambiar] in [hipótesis donde se va a cambiar] by [táctica para resolver la igualdad que propones para hacer el replace]

[ishinay]

¿Cómo hace Coq para generar los principos de inducción apartir de una difinición inductiva? (y no me refiero al ejemplo de nat, sino al cualquier cosa).

[susana]

¿Cómo hace Coq para generar los principos de inducción apartir de una difinición inductiva? (y no me refiero al ejemplo de nat, sino al cualquier cosa).

A partir de los constructores.

Veamos una serie de ejemplos:

Código: Seleccionar todo

Inductive DiaSemana : Set :=
    Lunes : DiaSemana
  | Martes : DiaSemana
  | Miercoles : DiaSemana
  | Jueves : DiaSemana
  | Viernes : DiaSemana
DiaSemana_ind
     : forall P : DiaSemana -> Prop,
       P Lunes ->
       P Martes ->
       P Miercoles -> P Jueves -> P Viernes -> forall d : DiaSemana, P d

Si definimos un tipo inductivo DiaSemana con constructores básicos todos, el principio de inducción generado es muy fácil:
Para demostrar que una proposición P:DiaSemana->Prop se cumple para todo d: DiaSemana, hay que demostrar que se cumple para el Lunes, para el Martes... (obvio, no? Se demuestra que se cumple para todos los días de la semana si lo demuestras para todos los días de la semana)

La "dificultad" viene cuando alguno de los constructores tiene recursividad.

Código: Seleccionar todo

Inductive nat : Set :=  O : nat | S : nat -> nat
nat_ind
     : forall P : nat -> Prop,
       P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

Para nat se tienen dos constructores: O y S(n) por así decirlo, por lo que se tienen dos hipótesis en el principio de inducción:
- Para el constructor 0 se tiene que demostrar P 0
- Para el constructor S(n) se tiene que demostrar que si P n -> P (S n)

Código: Seleccionar todo

Inductive or (A : Prop) (B : Prop) : Prop :=
    or_introl : A -> A \/ B | or_intror : B -> A \/ B
or_ind
     : forall A B P : Prop, (A -> P) -> (B -> P) -> A \/ B -> P

Para or se tienen dos constructores: or_introl(a) y or_intror(b) por lo que se tienen dos hipótesis en el principio de inducción:
- Para el constructor or_introl(a) se tiene que demostrar que si A->P (algo así como que P(a))
- Para el constructor or_intror(b) se tiene que demostrar que si B->P (algo así como que P(b))

Código: Seleccionar todo

Inductive and (A : Prop) (B : Prop) : Prop :=  conj : A -> B -> A /\ B
and_ind
     : forall A B P : Prop, (A -> B -> P) -> A /\ B -> P

Para and se tiene un constructor: conj(a,b) por lo que se tiene una hipótesis en el principio de inducción:
- Para el constructor conj(a,b) se tiene que demostrar que si A->B->P (algo así como que P(a,b))

Código: Seleccionar todo

Inductive False : Prop := 
False_ind
     : forall P : Prop, False -> P

Para False no se tiene ningún constructor, por lo tanto no se tienen ninguna hipótesis de inducción.