Buenas tardes, estaba haciendo el 4.3 del práctico, y la única manera que estoy encontrando de solucionarlo es llegar a esta situación:
2 goals
A, B, C : Prop
h1 : A -> B -> C
h2 : A /\ B
______________________________________(1/2)
A
______________________________________(2/2)
B
Y aplicar la táctica "destruct" sobre h2, obteniendo ambas hipótesis A y B, y luego simplemente hacer los assumption .
La pregunta es si por un lado, es aceptado el uso de "destruct" en las entregas de los ejercicios, dado que no aparece en las diapositivas.
La segunda pregunta sería, cómo podría solucionarse de otra manera porque de existir no la estoy encontrando.
En particular sospecho que en esta situación anterior
1 goal
A, B, C : Prop
h1 : A -> B -> C
______________________________________(1/1)
A /\ B -> C
Podría hacerse otra cosa que no sea un intro. Gracias
Hola Camilo.
Si, destruct está habilitada. AL usarla podés luego usar apply sobre h1 y verás que se generan dos obligaciones de prueba triviales.
Otra opción es usar (de lo visto en la clase): elim h2. Luego de hacer intros estás en la situación descrita arriba.
Saludos, Carlos