Stream: Beginner Questions

Topic: ✔ Failing to solve existential goal but metis can

Manuel Eberl (Jul 26 2022 at 14:08):

You're going to need the axiom of choice for this. metis is good at this. I think it performs skolemisation as a pre-processing step, and the skolemized version of the thing you already proved is exactly the goal, so metis doesn't even have to do anything anymore.

If you really don't want to use metis, you have to apply the axiom of choice yourself, e.g. like this:

  apply -
  apply (rule choice allI)+
  apply blast
  done

Jan van Brügge (Jul 26 2022 at 14:14):

Thank you, that did the trick:

apply (rule choice allI)+
apply (insert 1)
apply assumption
done

Notification Bot (Jul 26 2022 at 14:14):

Jan van Brügge has marked this topic as resolved.

Last updated: Apr 25 2024 at 20:15 UTC