Practico 3 Ejercicio 4

Practico 3 Ejercicio 4

de Santiago Guerra Boschiero -
Número de respuestas: 4

Buenas,

Estoy medio complicado con la formulación del teorema para este ejercicio, es decir que (id o id) x = id x. Me está dando error de tipos, y no se si estaré entendiendo mal los conceptos y definiendo mal las cosas además del teorema. Espero que no haya ningún problema con esto, pero adjunto mi definición del operador de composición, la identidad y lo que escribí para el teorema mencionado a ver si me pueden guiar un poco que me está costando.

Definition o: (A->B)->(B->C)->(A->C):=
   fun (f:A->B) (g:B->C) (x:A)=> g (f x).

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

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

Muchas gracias.

Saludos.

En respuesta a Santiago Guerra Boschiero

Re: Practico 3 Ejercicio 4

de Carlos Luna -

Hola Santiago.

Las variables dentro de una sección son arbitrarias pero fijas (no podés instanciarlas dentro de la sección). Recién cuando cerrás una sección las variables declaradas son abstraidas en las definiciones que las usan. Mirar los Check en:

Section Ejercicio3.

Variable A B C: Set.

Definition o : (A -> B) -> (B -> C) -> (A -> C) := fun f g x => g (f x).

Check o. (* o : (A -> B) -> (B -> C) -> A -> C *)

End Ejercicio3.

Check o.  (* o : forall A B C : Set, (A -> B) -> (B -> C) -> A -> C *)

Luego de cerrar la sección 3 notar que podrías instanciar "o" con instancias para A, B y C. Por ejemplo:

Section Ejercicio4.

Variable A: Set.

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

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

Otra opción es definir las funciones con las variables abstraidas (cuantificadas) directamente, dando la posibilidad a instanciarlas dentro de una misma sección. Por ejemplo:

Definition oo: forall A B C: Set, (A->B)->(B->C)->(A->C) :=

  fun (A:Set) (B:Set) (C:Set) f => fun g => (fun x => g (f x)).

Check oo.

Espero esto te ayude y si algo no quedó claro, volvé a escribir.

Saludos, Carlos

En respuesta a Carlos Luna

Re: Practico 3 Ejercicio 4

de Santiago Guerra Boschiero -
Con la formulación Theorem e4 : forall x : A, (o A A A id id) x = id x. me anduvo, muchas gracias. Me queda la duda de por qué es igual usar el operador o, o el oo (espero que se entienda el entrevero de letras o). Es decir, si yo en lugar de poner o en la definición del teorema, utilizo oo, me anda igual y tengo que instanciar A A A de igual forma. Qué aporta oo que no aporta o?
En respuesta a Santiago Guerra Boschiero

Re: Practico 3 Ejercicio 4

de Carlos Luna -

Hola

Las definciones son equivalentes. Usé oo para diferenciarla sintácticamente de o simplemente. El tipo de oo es el mismo tipo de o (fuera de la sección).

Saludos, Carlos