Reducing cases

Stream: new members

[Chris M]

I have come across a situation where a proposition X implies a disjunctive A\or B\or C. A, B, C are cases, but I can reduce case C to case B, i.e. lemma2: C\to B holds. I could write this as follows:

assume hX:X,
have h2: (A \or B) \or C, from lemma1 hX,
have h3: A \or B from or.elim h2 (assume h4:A \or B, h4) (assume h5:C, or.intro A (lemma2 h5))

However, this seems unnecessarily messy, and it seems I should be able to just "reduce C to B" in approximately one command, rather than having to consider the A and B cases as well. Is this possible?

[Chris Wong]

If you group the B and C together with or.assoc, then you can use or.imp_right to map that to B \or B then collapse it with or_self

[Chris Wong]

I think in general though we tend to use tactics like cc, which lessen the need to make manual manipulation easy

[Mario Carneiro]

There should be a theorem that says (q -> p) -> (p \/ q <-> p) that should be usable here

[Mario Carneiro]

example (a b c : Prop) (h : a ∨ b ∨ c) (h2 : c → b) : false :=
begin
  have := h.imp_right (or_iff_left_of_imp h2).1,
end

The advantage of this over using cc is that you don't have to assert the goal statement, it is a purely syntactic transformation so a,b,c can be any expressions and they will not be unduly affected by the tactic

[Mario Carneiro]

The fancy tactic version is

example (a b c : Prop) (h : a ∨ b ∨ c) (h2 : c → b) : false :=
begin
  have : a ∨ b := by tauto!,
end

[Mario Carneiro]

the other advantage of the first method is that the type of h2 is already determined by the context here so you can even do this in a way where h2 is a subgoal rather than a hypothesis:

example (a b c : Prop) (h : a ∨ b ∨ c) : false :=
begin
  have := h.imp_right (or_iff_left_of_imp (λ hb, _)).1,
  { -- this: a ∨ b |- false
    sorry },
  { -- hb: b |- c
    sorry },
end