CFPTT: Practico 3 - Ej 4

Perdón por el código, espero no sea incorrecta su publicación.

En el Ej 3 def :

Definition o := fun (f: X->X) (g: X->X) (x:X) => g (f x) : X.

Luego en el Ej 4 def:

Definition id : A -> A := fun (x:A) => x : A.

AL intentar def el teorema:

Theorem e4 : forall x:A, id x = o (id (id x)).

The term "id (id x)" has type "A" while it is expected to have type "Set".

Probe con distintas parentisaciones, pero simpre me da problemas de tipo ( o (id id x) genera " The term "id" has type "A -> A" while it is expected to have type "A".)

No entiendo si es un tema de sintaxis o algún concepto que no estoy entendiendo, agradecería si me pudieran dirigir.

Re: Practico 3 - Ej 4

de Carlos Luna - miércoles, 9 de septiembre de 2015, 13:54

Hola.

Fijate por ejemplo el tipo del operador "o" que definiste, usando Check.

Ahí vas a observar que hay argumentos (de tipo Set) que no estás poniendo al escribir "o (id (id x))". Estás omitiendo estos argumentos.

Fijate también el tipo "id".

Si no sale, volvé a escribir.

Saludos, Carlos

Re: Practico 3 - Ej 4

de Daniel Eduardo Erguiz Cartelle - miércoles, 9 de septiembre de 2015, 18:15

Check (o). -> : forall X : Set, (X -> X) -> (X -> X) -> X -> X

Yo interpreto que a "o" le paso 3 elementos , los 2 primeros (X -> X) uno de tipo X y me va a devolver otro elemento de tipo X

Check (id). -> : A -> A , según entendí el polimorfismo parametrico tendria que aceptar a id .

Pero: Theorem e4 : forall x:A, id x = o (id -> id -> x ). me da The term "id" has type "A -> A" which should be Set, Prop or Type.

En resumidas cuentas no logro entender que argumentos me estan faltando.

Re: Practico 3 - Ej 4

de Carlos Luna - miércoles, 9 de septiembre de 2015, 19:36

Hola.

El primer parámetro de "o" tiene que ser entonces un Set (fijate que al hacer el Check lo primero es forall X:Set) y luego tenés los 3 argumentos que mencionás.

Los argumentos se pasan sin las flechas: (o A id id x).

Saludos, Carlos