multiple disjunction elimination

Stream: general

[Bernd Losert]

If you have multiple hypotheses:

h : p ∨ q
h' : p' ∨ q'
h'' : p'' ∨ q''

how would I combine them into a disjunction of conjuncts (p ∧ p' ∧ p'') ∨ ...? And how do you eliminate such a large disjuction? I hope I won't have to resort to writing deeply nested code.

[Yaël Dillies]

One way to do it is to use the ; combinator:

obtain (h | h) := h; obtain (h' | h') := h'; obtain (h'' | h'') := h'',

[Huỳnh Trần Khanh]

another option is to use... the tauto tactic! for simple 1st order logic goals, tauto is great :smiley::+1:

[Bernd Losert]

Yaël Dillies said:

One way to do it is to use the ; combinator:

obtain (h | h) := h; obtain (h' | h') := h'; obtain (h'' | h'') := h'',

I don't understand that syntax. Is there a how-to or a tutorial explaining how to do this?

[Eric Wieser]

Another way is to use all_goals:

import tactic

lemma split_three_ors (p p' p'' q q' q'' : Prop) (h : p ∨ q) (h' : p' ∨ q') (h'' : p'' ∨ q'') :
  ((p ∧ p' ∧ p'' ∨ p ∧ p' ∧ q'') ∨
   (p ∧ q' ∧ p'' ∨ p ∧ q' ∧ q'')) ∨
  ((q ∧ p' ∧ p'' ∨ q ∧ p' ∧ q'') ∨
   (q ∧ q' ∧ p'' ∨ q ∧ q' ∧ q'')) :=
begin
  -- `tauto` probably works but is _very_ slow,
  obtain h | h := h; [left, right],
  all_goals { obtain h' | h' := h'; [left, right] },
  all_goals { obtain h'' | h'' := h''; [left, right], },
  all_goals { exact ⟨h, h', h''⟩}
end

[Huỳnh Trần Khanh]

Bernd Losert said:

Yaël Dillies said:

One way to do it is to use the ; combinator:

obtain (h | h) := h; obtain (h' | h') := h'; obtain (h'' | h'') := h'',

I don't understand that syntax. Is there a how-to or a tutorial explaining how to do this?

this is the ultimate guide on tactics https://leanprover-community.github.io/mathlib_docs/tactics.html. ; is a tactic combinator and you can read about tactic combinators here https://leanprover.github.io/theorem_proving_in_lean/tactics.html#tactic-combinators

[Eric Wieser]

The other thing to note is that | is part of the obtain syntax, which is the same as its meaning in rcases and rintro

[Bernd Losert]

Thanks guys. I'll grep mathlib to find examples that I can copy/paste.

[Mario Carneiro]

Also, obtain supports multiple destruction like so: obtain ⟨h | h, h' | h', h'' | h''⟩ := ⟨h, h', h''⟩. Thus:

lemma split_three_ors (p p' p'' q q' q'' : Prop) (h : p ∨ q) (h' : p' ∨ q') (h'' : p'' ∨ q'') :
  ((p ∧ p' ∧ p'' ∨ p ∧ p' ∧ q'') ∨
   (p ∧ q' ∧ p'' ∨ p ∧ q' ∧ q'')) ∨
  ((q ∧ p' ∧ p'' ∨ q ∧ p' ∧ q'') ∨
   (q ∧ q' ∧ p'' ∨ q ∧ q' ∧ q'')) :=
begin
  obtain ⟨h | h, h' | h', h'' | h''⟩ := ⟨h, h', h''⟩,
  all_goals { simp [h, h', h''] }
end

[Mario Carneiro]

Regarding tauto being slow: I am not sure why, this is a fairly trivial problem. itauto is quite fast on this problem

[Kyle Miller]

tauto doesn't seem to work for me with split_three_ors, but finish does work (somewhat slowly)

[Mario Carneiro]

(itauto also produces exactly the proof term you would write by hand, which I like to see)

[Eric Wieser]

Mario, does the ⟨h, h', h''⟩ there create an and term? Or is it special notation that obtain parses directly?

[Mario Carneiro]

@Eric Wieser It is special notation. (That notation would never parse normally, since the expected type is not known.) rcases is mutually recursive with a variation called rcases_many which handles many patterns at once (you need this to handle the list of subpatterns once you match a given n-ary pattern), and this is the surface level syntax to call rcases_many directly.

[Bhavik Mehta]

You can also do cases_matching* [_ ∨ _],