implication introduction

Stream: new members

[Alexandre Rademaker]

In ND, the implication can be introduced with zero hypotheses being canceled, right? How to make this operation in Lean? In tactic mode, I am in the current stage:

A B : Prop,
h : ¬(A → B),
h1 : B
⊢ A → B

[Alexandre Rademaker]

Hum, in tactic I solved with

example (h : ¬ (A → B)) : ¬ B :=
begin
 intro h1,
 apply h,
 intro h2, exact h1,
end

[Yakov Pechersky]

Tactic mode given your first example:

intro pA,
exact h1

[Alexandre Rademaker]

yes, I am now trying to make it in term mode...

[Yakov Pechersky]

example (A B : Prop) (h : ¬ (A → B)) : ¬ B :=
λ (pB : B), h (λ (pA : A), pB)

[Adam Topaz]

Keep in mind that \not P is the same as P -> false. So in term mode you can start with \lam hb, ... and you'll see that the goal is false. You only have one thing in context which can be used, which is h, etc.

[Alexandre Rademaker]

Thank you, the trick part was λ (pA : A), pB

[Yakov Pechersky]

You can also

example (h : ¬ (A → B)) : ¬ B :=
begin
  show_term { intro h1,
  apply h,
  intro h2,
  exact h1 }
end

[Yakov Pechersky]

For simple tactic steps like these, the show_term will give something decipherable.

[Alexandre Rademaker]

show_term is not working for me... maybe it is from mathlib?

[Yakov Pechersky]

Yes, it is

[Alexandre Rademaker]

yes, I found its definition! Thank you

[Kyle Miller]

Just as an amusement, another term mode proof that uses SKI combinators:

example {A B : Prop} : ¬ (A → B) → ¬ B := S (S (K S) K) (K K)

though I had to change their definitions in core.lean to use Sort rather than Type. It's obviously better because it's pointless I mean point-free. :smile: