8
$\begingroup$

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!

Improve this question
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Mike Shulman
    Commented Feb 18, 2022 at 4:24
  • 2
    $\begingroup$ 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. $\endgroup$
    – Bubbler
    Commented Feb 18, 2022 at 5:24

1 Answer 1

Reset to default
3
$\begingroup$

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
Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks. proof (intro iffI) works perfectly and is much nicer! $\endgroup$
    – Mark Utting
    Commented Feb 28, 2022 at 5:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.