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

Subforo de asignaturas del curso 2008-09.

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

Notapor ishinay » Mar, 13 Ene 2009 16:50

Muchas gracias por la explicación y el esfuerzo, Susana :) Pero no logro entenderlo :( me explico: Me has puesto unos ejemplos de tipos inductivos y los principios de inducción que generan, supongo que con la esperanza de que en cierto modo encuentre una regla que explique el porqué de todo ello... pero mi limitada mente (cosa que reconozco) no da para tanto...
Mi duda es precisamente esa: ¿cuáles son esas reglas que generan los principios de inducción? Es decir, SIN HACERLO EN COQ, ¿cuál es el principio de inducción del siguiente tipo inductivo?:

Código: Seleccionar todo
Inductive mdt (A:Set) (B:Prop) ((C->D):Type):Type :=
    c1: mdt A B (C->D)
    | c2: forall H:Type, D->mdt D B H
    | c3: c1\/c2 -> c3/\c1

Si en el código anterior hay cosas mal expresadas (que no dudo que puedan estar), puedes modificarlo a tu gusto. La idea es que sea algo complejo y que no se vea a simple vista ;)

Una cuestión más: el término "recursividad" que usaste, realmente parece que todo tipo inductivo es recursivo, y lo único que incrementa su complejidad es que tenga parámetros.
Avatar de Usuario
ishinay
Cuervo Sangriento
 
Mensajes: 86
Registrado: Mar, 01 Abr 2008 23:58

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

Notapor ishinay » Mar, 13 Ene 2009 16:53

Ah! y gracias por la explicación de la utilización de "induction" y "elim" :) me ha quedado claro.
Avatar de Usuario
ishinay
Cuervo Sangriento
 
Mensajes: 86
Registrado: Mar, 01 Abr 2008 23:58

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

Notapor susana » Mar, 13 Ene 2009 17:29

ishinay escribió:
Código: Seleccionar todo
Inductive mdt (A:Set) (B:Prop) ((C->D):Type):Type :=
    c1: mdt A B (C->D)
    | c2: forall H:Type, D->mdt D B H
    | c3: c1\/c2 -> c3/\c1

Si en el código anterior hay cosas mal expresadas (que no dudo que puedan estar), puedes modificarlo a tu gusto. La idea es que sea algo complejo y que no se vea a simple vista ;)


Voy a usar otro ejemplo para intentar explicarme... tu mdt no me acaba de convencer ;)
Código: Seleccionar todo
Inductive arbol: Set :=
vacio: arbol| der: nat-> arbol ->arbol | izq: arbol ->arbol | nodo: nat->arbol.

Supongamos un árbol binario, donde las ramas derechas tienen etiquetas enteras, por ejemplo, y hay nodos vacíos o nodos con una etiqueta entera.

ishinay escribió:Una cuestión más: el término "recursividad" que usaste, realmente parece que todo tipo inductivo es recursivo, y lo único que incrementa su complejidad es que tenga parámetros.


Cuando me refiero a recursividad es que alguno de los parámetros del constructor sea del tipo que estamos definiendo. Por ejemplo, en DiaSemana no pasa nunca (por eso el principio inductivo es tan sencillo) y en los números naturales pasa para S:nat->nat, no para el O, por eso el P 0 es sencillo, en cambio el otro paso inductivo es más complejo (si P n -> P (S n) )

En este caso hay cinco constructores. Uno es más sencillo, porque no es recursivo ni tiene parámetros (vacio), dos recursivos y con parámetros y el último con un parámetro pero no recursivo.

Cómo será el principio inductivo?
Pues intentaremos sacarlo sin mirar en coq...
Para empezar queremos demostrar una propiedad relativa al tipo que estamos construyendo, así que será forall P:arbol->Prop.
El primer constructor es sencillo, no tiene recursividad, sólo tendremos que demostrar la propiedad para vacio, así que será P vacio.
El segundo constructor ya es más complicado, porque es recursivo. Así que en este caso debemos probar que si para cualquier n y cualquier árbol que se le pase al constructor, si se cumple la propiedad para este árbol entonces se debe cumplir para el nuevo árbol construido a partir de los parámetros con ese constructor. Es decir, para todo n:nat, a:arbol, si P a-> P (der n a).
Fíjate que es muy parecida a la recursividad de los naturales. En los naturales se tiene que S:nat->nat, por lo que para todo n:nat, si P n-> P (S n). En este caso se tiene que der: nat->arbol->arbol, así que es si para todo n:nat, para todo a:arbol, si P a-> P (der n a).
Para el otro constructor es parecido, pero no recibe nat, por lo que simplemente es para todo a:arbol, si P a -> P (izq a)
El último constructor sólo recibe un entero, no es recursivo, por lo que sólo se tendrá que comprobar que para todo n:nat, P (nodo n)


En conjunto se tiene, como se puede comprobar

Código: Seleccionar todo
arbol_ind
     : forall P : arbol -> Prop,
       P vacio ->
       (forall (n : nat) (a : arbol), P a -> P (der n a)) ->
       (forall a : arbol, P a -> P (izq a)) ->
       (forall n : nat, P (nodo n)) -> forall a : arbol, P a


Es cierto que a lo mejor los ejemplos que puse no eran muy aclaratorios para sacar un patrón, porque algunos tipos inductivos eran de tipo Set y otros eran de tipo Prop, que son claramente diferentes. Fíjate en todos los del tipo Set, por ejemplo, que son más intuitivos y siguen más claramente el patrón.

El patrón será:
- Si alguno de los parámetros es el mismo que el que se está definiendo, entonces se tendrá que demostrar que si P parametro -> P (constructor parametro)
- Si no es recursivo es más fácil, sólo habrá que demostrar P (constructor)
(donde en los dos casos puede haber más parámetros, pero lo importante son los recursivos)

La recursividad esa la puedes ver en nat (con S) y en este ejemplo. En los otros ejemplos que te puse no había más recursividades (fíjate por ejemplo que en ninguno de los constructores de and, or, ex... recibe un parámetro del mismo tipo que se está definiendo).


EDITO: edité el mensaje, porque me había confundido y aunque originalmente quería poner izq: nat->arbol->arbol, igual que el derecho, me había olvidado de pasarle el primer nat. Así que completé el ejemplo dejándolo así para que se pudiese ver toda la casuística ;)
susana
Ojo de Fuego
 
Mensajes: 361
Registrado: Jue, 27 Nov 2008 17:05

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

Notapor Fonso » Mié, 14 Ene 2009 21:06

Hola a todos,

Me ha surgido un problemilla demostrando evenodd. Después de hacer varios pasos, llego a este subobjetivo:

Código: Seleccionar todo
1 subgoal
n : nat
H : exists p : nat, n = S (S p)
______________________________(1/1)
exists p : nat, S n = S (S p)


Y aquí se acaba mi andadura. ¿Alguien tiene idea de por donde puedo tirar?
Fonso
Rakanishu
 
Mensajes: 12
Registrado: Lun, 12 Ene 2009 14:23

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

Notapor susana » Mié, 14 Ene 2009 21:50

Fonso escribió:Hola a todos,

Me ha surgido un problemilla demostrando evenodd. Después de hacer varios pasos, llego a este subobjetivo:

Código: Seleccionar todo
1 subgoal
n : nat
H : exists p : nat, n = S (S p)
______________________________(1/1)
exists p : nat, S n = S (S p)


Y aquí se acaba mi andadura. ¿Alguien tiene idea de por donde puedo tirar?


H es un término de un tipo inductivo, así que puedes eliminarlo. Si lo haces te dará el p que cumple esa propiedad. Por ejemplo, llamamos x al número tal que n = S (S x). Es decir, sabemos que n = x+2.

Para probar el objetivo tenemos que darle al sistema un valor de p que cumpla que n+1 = p + 2, es decir, tal que n = p +1. ¿Qué número cumple eso?
susana
Ojo de Fuego
 
Mensajes: 361
Registrado: Jue, 27 Nov 2008 17:05

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

Notapor ishinay » Mié, 14 Ene 2009 23:14

Fonso escribió:Hola a todos,
Me ha surgido un problemilla demostrando evenodd. Después de hacer varios pasos, llego a este subobjetivo:
Código: Seleccionar todo
1 subgoal
n : nat
H : exists p : nat, n = S (S p)
______________________________(1/1)
exists p : nat, S n = S (S p)


Y aquí se acaba mi andadura. ¿Alguien tiene idea de por donde puedo tirar?

Yo sobre esto tengo una duda y creo que interesante... tenemos un "exists p" en las hipótesis y otro "exist p" en el objetivo. Las 'p' son distintas ¿Me equivoco? (podría sustituírse por cualquier otro nombre y daría igual) de esta forma, la hipótesis te dice que existe (n-2) (existir de no ser menor que cero!)y lo que tienes que demostrar es que existe (n-1) ¿no?.
Escrito más claramente sería:
Código: Seleccionar todo
1 subgoal
n : nat
H : exists k : nat, n = S (S k)
______________________________(1/1)
exists p : nat, S n = S (S p)

¿Es correcto?
Avatar de Usuario
ishinay
Cuervo Sangriento
 
Mensajes: 86
Registrado: Mar, 01 Abr 2008 23:58

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

Notapor Fonso » Mié, 14 Ene 2009 23:15

susana escribió:H es un término de un tipo inductivo, así que puedes eliminarlo. Si lo haces te dará el p que cumple esa propiedad. Por ejemplo, llamamos x al número tal que n = S (S x). Es decir, sabemos que n = x+2.

Para probar el objetivo tenemos que darle al sistema un valor de p que cumpla que n+1 = p + 2, es decir, tal que n = p +1. ¿Qué número cumple eso?


Vale, había probado lo de eliminar H, pero después metí la gamba al darle el valor de p. Ya está resuelto; aún así, he tenido que dar bastantes vueltas después para acabar la demostración de algo bastante trivial. No sé como le quedará a los demás, pero me están saliendo demostraciones kilométricas. No puedo evitar pensar que son un poco chapuzas :lol: aunque supongo que si se llega al Proof Completed bien valen.

¡Gracias por la pista!
Fonso
Rakanishu
 
Mensajes: 12
Registrado: Lun, 12 Ene 2009 14:23

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

Notapor ishinay » Mié, 14 Ene 2009 23:28

Muchas gracias, Susana, por tu megaexplicación. Me ha quedado claro, pero reconozco que con Prop no acabo de ver las cosa... :P
En este caso:
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


¿Por qué no es algo del tipo...:
Código: Seleccionar todo
or_ind
      : forall P : or->Prop, (* Que conste que no tengo ni idea de cómo tratar propiedades de tipos inductivos con parámetros -el árbol no tenía-*)
        P or_introl ->
        P or_intror ->
        forall a:or, P a

Ya sé que te dolerán los ojos... sorry! xD
¿Los parámetros en "P or_introl" y "P or_intror"? Realmente me he basado en el "Inductive DiaSemana", ya que en el principio de inducción que da Coq mete un "A\/B" como parámetro para demostrar 'P' y tampoco sé de dónde sale :S
Gracias por las explicaciones, claro :)
Avatar de Usuario
ishinay
Cuervo Sangriento
 
Mensajes: 86
Registrado: Mar, 01 Abr 2008 23:58

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

Notapor Fonso » Jue, 15 Ene 2009 16:32

Hola otra vez,

A ver, estoy enfrascado en la demostración de div2_le y creo que más o menos se por donde puedo tirar, pero me encuentro con lo siguiente:

Código: Seleccionar todo
1 subgoal
n : nat
IHn : div2 n <= n
_____________________(1/1)
div2 (S n) <= S n

Lo que quiero hacer es separar esto en div2 (S n) < S n \/ div2 (S n) = S n, para demostrar cada cosa por separado. He probado a introducir hipotesis, pero la cosa se complica más y no estoy seguro de que vayan por ahí los tiros.

¿Hay alguna forma de que Coq descomponga la comparación objetivo en las dos que necesito? He leido en la referencia algo acerca de una táctica llamada Omega que se supone que resuelve las ecuaciones e inecuaciones o algo así, pero la verdad es que leer la documentación de Coq a veces hace más mal que bien.
Fonso
Rakanishu
 
Mensajes: 12
Registrado: Lun, 12 Ene 2009 14:23

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

Notapor susana » Jue, 15 Ene 2009 16:51

No entiendo a qué te refieres con que quieres demostrar "cada cosa por separado" en div2 (S n) < S n \/ div2 (S n) = S n, ya que no es posible demostrar las dos cosas por separado. No se puede cumplir que sea menor y que sea igual al mismo tiempo. Además para demostrar un or, te quedas con una parte, así que tendrías que demostrar que es menor o que es igual (con left o right)

De todas formas ojo! No sé si llegaste a ese subobjetivo usando la inducción normal, pero tiene toda la pinta. Como comenté anteriormente, todo lo que tenga que ver con div2 va a tener comportamientos diferentes con los pares y los impares, así que usar la inducción normal no es buena idea ;)
susana
Ojo de Fuego
 
Mensajes: 361
Registrado: Jue, 27 Nov 2008 17:05

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

Notapor Fonso » Jue, 15 Ene 2009 17:40

susana escribió:No entiendo a qué te refieres con que quieres demostrar "cada cosa por separado" en div2 (S n) < S n \/ div2 (S n) = S n, ya que no es posible demostrar las dos cosas por separado. No se puede cumplir que sea menor y que sea igual al mismo tiempo. Además para demostrar un or, te quedas con una parte, así que tendrías que demostrar que es menor o que es igual (con left o right)

De todas formas ojo! No sé si llegaste a ese subobjetivo usando la inducción normal, pero tiene toda la pinta. Como comenté anteriormente, todo lo que tenga que ver con div2 va a tener comportamientos diferentes con los pares y los impares, así que usar la inducción normal no es buena idea ;)


Efectivamente, me he explicado fatal. A lo que me refería era a convertir el objetivo en un or, para poder demostrar una parte. Lo he demostrado utilizando primero induction e introduciendo después la hipotesis div2 (S n) <= S n <-> (div2 (S n) < S n \/ div2 (S n) = S n. He terminado la demostración, así que imagino que será válida; si se llega a Proof Completed es que está todo probado ¿no?
Fonso
Rakanishu
 
Mensajes: 12
Registrado: Lun, 12 Ene 2009 14:23

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

Notapor susana » Jue, 15 Ene 2009 18:30

Fonso escribió: si se llega a Proof Completed es que está todo probado ¿no?

Sí, desde luego

Fonso escribió:introduciendo después la hipotesis div2 (S n) <= S n <-> (div2 (S n) < S n \/ div2 (S n) = S n


EDITO:
No sé por qué me lié con el menor o igual, si tienes razón ;)
Pero no te hace falta demostrar la doble implicación, sólo es necesaria en este sentido <- para que puedas utilizarla en tu demostración
susana
Ojo de Fuego
 
Mensajes: 361
Registrado: Jue, 27 Nov 2008 17:05

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

Notapor Fonso » Jue, 15 Ene 2009 18:43

susana escribió:
Fonso escribió: si se llega a Proof Completed es que está todo probado ¿no?

Sí, desde luego

Fonso escribió:introduciendo después la hipotesis div2 (S n) <= S n <-> (div2 (S n) < S n \/ div2 (S n) = S n


EDITO:
No sé por qué me lié con el menor o igual, si tienes razón ;)
Pero no te hace falta demostrar la doble implicación, sólo es necesaria en este sentido <- para que puedas utilizarla en tu demostración


Jajaja, Ok. Cuando se me ocurrió estaba convencido de que estaba bien, pero después me hiciste dudar. Te he hecho caso y solo me he quedado con <- , queda más limpia la demostración. Bueno, ha dado guerra, pero ya está acabada la práctica. Espero que el examen sea algo más fácil que esto, sino no va a dar tiempo a acabarlo.

Un saludo.
Fonso
Rakanishu
 
Mensajes: 12
Registrado: Lun, 12 Ene 2009 14:23

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

Notapor susana » Jue, 15 Ene 2009 21:20

ishinay escribió:Me ha quedado claro, pero reconozco que con Prop no acabo de ver las cosa... :P
En este caso:
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


¿Por qué no es algo del tipo...:
Código: Seleccionar todo
or_ind
      : forall P : or->Prop, (* Que conste que no tengo ni idea de cómo tratar propiedades de tipos inductivos con parámetros -el árbol no tenía-*)
        P or_introl ->
        P or_intror ->
        forall a:or, P a

Ya sé que te dolerán los ojos... sorry! xD
¿Los parámetros en "P or_introl" y "P or_intror"? Realmente me he basado en el "Inductive DiaSemana", ya que en el principio de inducción que da Coq mete un "A\/B" como parámetro para demostrar 'P' y tampoco sé de dónde sale :S


El capítulo 14 del libro se centra precisamente en este tema, en cómo generar los principios de inducción. En una parte de este capítulo ya indica que los principios generados para los predicados de tipo Prop son diferentes a los del tipo Set. Los de tipo Prop son más sencillos, por la irrelevancia de la prueba. De esta manera sólo hay que suponer una P:Prop (ojo, no puede ser or->Prop, en todo caso sería or A B-> Prop, porque or es de tipo Prop->Prop->Prop, y si se tiene X->Prop, X sólo puede ser de tipo Set, Prop o Type). Si quieres profundizar en esto puedes mirar el libro, o incluso preguntarme personalmente, pero creo que sería liar mucho a la gente ponerse a explicar esto en detalle.

Pero lo que si es importante es el concepto de "irrelevancia de la prueba", no se si te sonará. A nosotros en el examen nos cayó un ejercicio que tenía que ver con esto...
Básicamente el ejercicio era intentar demostrar los siguientes lemas: (en papel! así que había que saber en cada momento qué táctica usar, y qué cambios en el contexto y objetivos se generaban):

Código: Seleccionar todo
- forall A:Set, forall P:A->Prop, {a:A|P a} -> exists a: A, P a
- forall A:Set, forall P:A->Prop, (exists a: A, P a) -> {a:A|P a}

Es un buen ejercicio que intentéis demostrarlos, o pensad por qué no se puede demostrar alguno de ellos...
susana
Ojo de Fuego
 
Mensajes: 361
Registrado: Jue, 27 Nov 2008 17:05

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

Notapor ishinay » Jue, 15 Ene 2009 21:55

Gracias, Susana! :)
A ver si llego a esa parte en el libro, que todavía estoy sobre la página 110... :P
Avatar de Usuario
ishinay
Cuervo Sangriento
 
Mensajes: 86
Registrado: Mar, 01 Abr 2008 23:58

AnteriorSiguiente

Volver a FIC Asignaturas 2008-09

¿Quién está conectado?

Usuarios navegando por este Foro: No hay usuarios registrados visitando el Foro y 0 invitados