Me gustaría ver, de ser posible, algún ejemplo de un predicado sobre lista.
Debemos implementar sorted o eq_list y la verdad me quedan dudas sobre el caso inductivo.
Y en particular en el sorted, donde le pongo que cumpla la condición R?
Gracias.
Practico 4 - Predicados inductivos sobre Listas
Número de respuestas: 4
En respuesta a German Adolfo Faller Farias
Re: Practico 4 - Predicados inductivos sobre Listas
ya vi otros mensajes en el foro y encontré algunos ejemplos, en particular
Inductive eq_list (A:Set): list A -> list A -> Prop :=
| eq_empty: eq_list A (nil A) (nilA)
| eq_cons: forall (e1 e2:A)(l1 l2:list A), eq e1 e2 -> eq_list A l1 l2 -> eq_list A (cons A e1 l1)(cons A e2 l2).
En respuesta a German Adolfo Faller Farias
Re: Practico 4 - Predicados inductivos sobre Listas
de Carlos Luna -
Hola.
Un ejemplo sobre listas (igualdad):
Inductive list (A : Set) : Set :=
nil : list A
| cons : A -> list A -> list A.
Inductive eq_list (A : Set) : list A -> list A -> Prop :=
eq_nil : eq_list A (nil A) (nil A)
| eq_cons : forall (e : A) (xs ys : list A),
eq_list A xs ys -> eq_list A (cons A e xs) (cons A e ys).
.En el caso de sorted, R es un parámetro de la relación:
Inductive sorted (A : Set) (R : A -> A -> Prop) : list A -> Prop :=
sorted_nil : sorted A R (nil A)
| ...
Saludos, Carlos
Hola.
Teniendo en cuenta este ejemplo, no entiendo a qué refiere la letra del práctico cuando dice "a partir de la igualdad del tipo A". Yo también lo pensé como lo que escribió German usando un predicado binario para elementos de A (aunque habría que tomarlo como parámetro en algún lado para que esté definido).
Saludos,
Gabriel
Teniendo en cuenta este ejemplo, no entiendo a qué refiere la letra del práctico cuando dice "a partir de la igualdad del tipo A". Yo también lo pensé como lo que escribió German usando un predicado binario para elementos de A (aunque habría que tomarlo como parámetro en algún lado para que esté definido).
Saludos,
Gabriel
Hola
Siguiendo este hilo, la igualdad entre elementos de un tipo A podría ser un parámetro de la relación inductiva sobre listas que lo usa (similar al ejemplo de sorted).
Sin usar la igualdad, una opción alternativa para definir una relación inductiva es usar el mismo elemento (variable) en cada instancia correspondiente a la definición, como se muesta en un mensaje de este hilo para la igualdad entre listas, por ejemplo.
Saludos Carlos
Siguiendo este hilo, la igualdad entre elementos de un tipo A podría ser un parámetro de la relación inductiva sobre listas que lo usa (similar al ejemplo de sorted).
Sin usar la igualdad, una opción alternativa para definir una relación inductiva es usar el mismo elemento (variable) en cada instancia correspondiente a la definición, como se muesta en un mensaje de este hilo para la igualdad entre listas, por ejemplo.
Saludos Carlos