# Is there an elegant way of proving an equality A=B by going in both directions?

I would like to prove an equality by splitting it into a proof in each direction.

Is there a more elegant style to start such a proof than this way::

lemma eq_by_both_directions:
shows "L = R"
apply (unfold iff_conv_conj_imp; rule conjI; rule impI)
proof (goal_cases)
case 1
assume ?L
show ?R by ...
next
case 2
assume ?R
then show ?L by ...
qed


Note: this is using the HOL theorem:

   HOL.iff_conv_conj_imp: (?P = ?Q) = ((?P ⟶ ?Q) ∧ (?Q ⟶ ?P))


The proof is also bad style because of the 'apply' commands before starting the Isar proof.

(Strangely, if those apply commands are inserted into the proof startup just before 'goal_cases', then only one case is generated rather than two, so the 'next case 2' becomes incorrect. But this might be an unrelated to my question).

So, is there a nicer way of starting up a bi-directional equality proof? Thanks!

• I can't comment on isar specifically, but in general, it is sometimes possible to prove logical equivalences by chaining together known equivalences using transitivity. But it depends on exactly how you are going to prove it. Feb 18 at 4:24
• Regarding tag usage, this is not a valid proof-review question because such a question should present a concrete theorem and its complete proof, not just a skeleton. Also, as Mike mentioned, the answer may vary depending on the theorem to prove (and how you'd prove it), so you may want to include such information in the question. Feb 18 at 5:24

I believe there is, provided that L and R are predicates, of course:

lemma eq_by_both_directions: "L ⟷ R"
proof(intro iffI, goal_cases)
case 1
then show ?case sorry
next
case 2
then show ?case sorry
qed


As a side note, there is no need to use goal_cases and, in fact, it may not be the most conventional format. If you wish to generate code (similar to the way it is generated by goal_cases) in a more conventional format automatically, you can import the tool HOL-ex.Sketch-and-Explore. Thus, for example, the invocation of

lemma eq_by_both_directions: "L ⟷ R"
sketch(intro iffI)
oops


generates the code akin to

lemma eq_by_both_directions: "L ⟷ R"
proof(intro iffI)
show R if L using that sorry
show L if R using that sorry
qed

• Thanks. proof (intro iffI) works perfectly and is much nicer! Feb 28 at 5:29