Stream: Beginner Questions

Topic: Isar re-use facts and`next`


view this post on Zulip Robert Soeldner (Sep 30 2022 at 15:58):

I sometimes run into the problem, that a particular subgoal requires earlier proven subgoals. I always use next in between subgoals, but this prevents re-using the fact. Is there a common solution? I could imagine: drop next and use the fact (which I haven't seen in any other code, I think) or start the overall proof using proof - state the facts using have and re-use them later.

view this post on Zulip Wolfgang Jeltsch (Sep 30 2022 at 17:00):

Robert Soeldner said:

I sometimes run into the problem, that a particular subgoal requires earlier proven subgoals. I always use next in between subgoals, but this prevents re-using the fact. Is there a common solution? I could imagine: drop next and use the fact (which I haven't seen in any other code, I think) or start the overall proof using proof - state the facts using have and re-use them later.

I dropped the next in one particular case. In general, I don’t recommend it, because it leads to less structured proofs.


Last updated: Feb 27 2024 at 08:17 UTC