Hola, me surge la duda de cómo es que funciona exactamente la táctica elim cuando tenemos un implica. ¿En qué casos se puede aplicar? Hay un par de ejercicios que los resolví con esto, pero no entiendo el mecanismo.
Saludos,
Jairo.
Hola.
No se vio en el curso el elim de una ->. No siempre se puede aplicar, por lo que no es una buena idea usarlo. Por ejemplo:
Variable A B: Prop.
Lemma L1: (A->B) -> A -> B.
intros.
elim H. <----- ES UN ERROR
Lemma L1: (A->B) -> A -> B.
intros.
apply H. <----- ESTÁ BIEN
Saludos, Carlos
Igual ese no era el uso que le estaba dando, cuando se puede utilizo apply. El tema era en otros casos por ejemplo para elminar "(A -> False) -> False".
Lo que hacía era me ponía como goal "(A -> False)".
Pero ahora que miré nuevamente, pude evitar usar esta táctica y en su lugar utilicé cut.
Saludos,
Jairo.