Stream: Beginner Questions

Topic: Shorthand to split an assumed conjunction

Charles Southerland (Feb 25 2024 at 01:57):

Is there some shorthand to split a conjunction into independent statements in an Isar proof?

The context: A pattern I often find myself repeating (particularly in slightly more intricate induction cases) is to assume a combined property with many /\ clauses for the purposes of exactly matching the proof requirement, but then immediately spilt the conjunction into independent statements. I am doing this to help make it clearer about exactly which part was required for a particular intermediate step when I come back to re-read my proof at a later date. I like the resulting level of verbosity in the test of my proof, but it seems unfortunate that this basically requires immediately repeating all that I already had to state in a single statement in order to meet the proof obligation. For what it's worth, another pattern like this also often comes up when I'm dealing with case analysis, though at least in those circumstances I am usually only explicitly pointing out properties from the state implied by the case being worked on. Perhaps it is very naive of me to try to make my proofs read as verbosely as those proofs I worked on in undergrad math, but at least so far this approach seems to have helped me diagnose subtle problems in my definitions more quickly.

Mathias Fleury (Feb 25 2024 at 06:50):

I think that I need an example here, because I do not see what youmean

lemma
  shows ‹P ∧ Q› (is ‹?P ∧ ?Q›)
proof -
  have ?P
    sorry
  moreover have ?Q
    sorry
  ultimately show ?thesis
    by auto
qed

lemma
  shows ‹P ∧ (R ⟶ Q)›
proof (intro allI conjI impI) ―‹I sometimes uses (intro allI conjI impI)›
  show P
    sorry
next (*actually optional as long as P has no assume*)
  assume R
  show Q
    sorry
qed

Mathias Fleury (Feb 25 2024 at 06:51):

Either I am misunderstanding what you mean, or is ?thesis / cases / and is not enough?

Charles Southerland (Mar 24 2024 at 10:14):

Sorry for the delayed response! I have several mediocre examples of this pattern on hand, but I was hoping to find a good, clean example in some of my previous code, but that has proven more difficult to find than I expected. I haven't yet eliminated the possibility that a good, clean example of this issue might be impossible, and that perhaps this pattern only comes up due to more fundamental issues with an approach. However, as I continue to work on these proofs, If I do find a good, clean example, I will share it here.

Last updated: Apr 28 2024 at 04:17 UTC