Stream: Beginner Questions

Topic: how to write a function based on a lemma

view this post on Zulip ee (Feb 19 2024 at 14:41):

If I have a lemma that states "forall x. P x \/ Qx", and "Q x" has the form "\exists y. P y" how do I later use this to define a function that states "fun funName x = if ( P x) then 1 else (1 + funName y)" where the "y" comes from the existential quantifier in the lemma?

view this post on Zulip Yong Kiam (Feb 19 2024 at 15:46):

use the choice operator to choose y with SOME y. R y (R here is the name of the predicate under the exists)

Last updated: Apr 27 2024 at 20:14 UTC