Robert Soeldner (Sep 30 2022 at 15:58): 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.
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
nextin between subgoals, but this prevents re-using the fact. Is there a common solution? I could imagine: dropnextand use the fact (which I haven't seen in any other code, I think) or start the overall proof usingproof -state the facts usinghaveand 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: Apr 25 2024 at 20:15 UTC