Zulip Chat Archive

Stream: new members

Topic: Reducing cases


view this post on Zulip Chris M (Jun 15 2020 at 04:24):

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?

view this post on Zulip Chris Wong (Jun 15 2020 at 05:08):

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

view this post on Zulip Chris Wong (Jun 15 2020 at 05:08):

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

view this post on Zulip Mario Carneiro (Jun 15 2020 at 05:10):

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

view this post on Zulip Mario Carneiro (Jun 15 2020 at 05:16):

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

view this post on Zulip Mario Carneiro (Jun 15 2020 at 05:18):

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

view this post on Zulip Mario Carneiro (Jun 15 2020 at 05:23):

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

Last updated: May 10 2021 at 00:31 UTC