Stream: Beginner Questions

Topic: stuck with proof

view this post on Zulip ee (Jan 31 2024 at 11:14):

The latest state of my proof is
"goal (1 subgoal):

  1. ∀x. ∃y. normalForm y ∧ (∃f. target f = y ∧ source f = x) ⟹
    ∀x. ∃y. (∃f. target f = y ∧ source f = x) ∧ normalForm y" which should be very simple to prove(I think) yet I'm not sure how to proceed. I checked the FOL and IFOL but couldn't really find anything that seemed helpful. Sorry if this is an extremely stupid question, I'm at the very early stages of learning Isabelle.

view this post on Zulip Mathias Fleury (Jan 31 2024 at 11:18):

I am going to assume that for reasons not in you post, you do not want to use blast / auto or any other tactic that according to try0 work

view this post on Zulip Mathias Fleury (Jan 31 2024 at 11:20):

So the problem is to:(i) use commutativity of conjunction and (ii) use assumption to prove the goal

view this post on Zulip Mathias Fleury (Jan 31 2024 at 11:20):

(i) can easily be done with apply (subst conj_commute)

view this post on Zulip Mathias Fleury (Jan 31 2024 at 11:20):

(ii) is simply by assumption

view this post on Zulip Mathias Fleury (Jan 31 2024 at 11:21):

But: I suggest starting with not bothering on these annoying details and be happy that auto is able to do it for you

view this post on Zulip ee (Jan 31 2024 at 11:25):

Thank you!

Last updated: Apr 28 2024 at 01:11 UTC