How to reduce implication goal to not of lhs

Stream: new members

[Jakub Nowak]

What is the easiest way to reduce goal of the form p → q to ¬p?

Here I achieved what I need by implementing impl_elim:

def impl_elim (nhp : ¬p) : p → q := by exact fun a ↦ False.elim (nhp a)

example {p q : Prop} : p → q := by
  -- Doesn't work???
  -- apply?
  apply impl_elim

Btw, I think there is some problem with apply? for implications. I'm not sure but my guess it's probably because apply? tries to intro.

[Kyle Miller]

Usually if your goal is an implication you'll have introd. A pure-tactic way to deal with this is intro h; exfalso; revert h.

[Robin Arnez]

impl_elim is too generic for apply? because it could match everything: for it 1 < 2 could be a candidate for this with the remaining goals ¬?p, ?p and ?p : Prop. This is obviously not good because it would mean we get irrelevant results for every goal. Thus, it just ignores them.