Hola.
Tengo una duda en
K = def [x][y]x
No me queda claro como usar y.
Yo lo tome como un parametro que no se usa.
Definition K : forall A B: Set, A->A:= fun (A: Set)(B: Set)(x: A)=> x.
Pero en la parte 2 de este ejercicio me di cuenta que esta mal por que me tira un error de tipo la igualdad
S K K = I.
Por eso creo que el problema es como defino K.
Saludos.
Hola.
K no está bien definido. Debería ser:
Definition K : forall A B:Set, A -> B -> A :=
fun (A B:Set) (x:A) (y:B) => x.
Para formalizar el lemma SKK=I (e52) va a ser necesario poner los tipos adecuados. Esto es, determinar los tipos ?i en:
Lemma e52 : forall ... : Set, (S ?1 ?2 ?3 (K ?4 ?5) (K ?6 ?7)) = I ?8.
NOTA: les recomiendo renombrar el operador S (por ejemplo S') para evitar conflictos con S:nat->nat, que se usa después.
Saludos, Carlos
Hola.
No tenés que pensar en S en función de un posible uso posterior, sino según su definición.
Definition S' : forall A B C:Set, (A->B->C) -> (A->B) -> A -> C :=
fun (A B C:Set) (f:A->B->C) (g:A->B) (x:A) =>
(f x) (g x).
Saludos, Carlos
Hola Carlos,
No entiendo en tu definición cómo podrías hacer SKK si en realidad terminarías teniendo:
(A->B->C) -> (A->B) -> A -> C = (A->B->C) -> (A->B) -> (A -> C)
Si SKK = I, entonces está bien que al final quede una función de un parámetro (porque así es I), pero no veo cómo se hace encajar el segundo K en SKK, cuando K es del tipo A->B->A, mientras que tu segundo parámetro sería esperable que fuera (A->B), segun esa definicion.
Disculpá si es muy boba la pregunta.
Creo que este error viene de la mano con lo que yo digo:
S' ?1 ?2 ?3 (K ?4 ?5) (K ?6 ?7) = I ?8.
The term "K ?6 ?7" has type "... -> ... -> ..."
while it is expected to have type ".. -> ..".
En mi mail puse:
Lemma e52 : forall ... : Set, (S ?1 ?2 ?3 (K ?4 ?5) (K ?6 ?7)) = I ?8.
Una ayuda: ?2 y ?5 tienen que ser un tipo (el mismo tipo) de la forma: Ti -> Tj.
Saludos, Carlos
