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
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...
aunque supongo que si se llega al 