Nos podrían guiar un poco para arrancar?
Gracias.
Tenemos un par de dudas con respecto a este ejercicio. No entendemos bien que es lo que se pide, ni de que forma hay que probarlo.
Hola.
Lo que se pide inicialmente es dar términos de los tipos indicados. Por ejemplo:
Variable A B C : Set.
(*1*)
Definition Ej1_1_a_1 (f : A -> A -> A) (x : A) := f x x.
Definition Ej1_1_a_2 (f : A -> A -> A) (x : A) := x.
(* 2 *)
Usando Check se pueden ver que ambos términos tienen el mismo tipo (son dos habitantes del mismo tipo):
Check Ej1_1_a_1.
Check Ej1_1_a_2.
(*3*)
La parte 3 para el ejemplo de arriba sería:
Lemma Ej1_3_a_1 : (A -> A -> A) -> A -> A.
Proof.
tauto.
Qed.
Lemma Ej1_3_a_2 : (A -> A -> A) -> A -> A.
Proof.
intros H H0; exact (H H0 H0).
Qed.
Saludos, Carlos