## Stream: new members

### Topic: implication introduction

#### Alexandre Rademaker (Sep 02 2020 at 01:28):

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 (Sep 02 2020 at 01:29):

Hum, in tactic I solved with

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


#### Yakov Pechersky (Sep 02 2020 at 01:30):

Tactic mode given your first example:

intro pA,
exact h1


#### Alexandre Rademaker (Sep 02 2020 at 01:30):

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

#### Yakov Pechersky (Sep 02 2020 at 01:34):

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


#### Adam Topaz (Sep 02 2020 at 01:34):

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 (Sep 02 2020 at 01:36):

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

#### Yakov Pechersky (Sep 02 2020 at 01:37):

You can also

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


#### Yakov Pechersky (Sep 02 2020 at 01:38):

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

#### Alexandre Rademaker (Sep 02 2020 at 01:38):

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

Yes, it is

#### Alexandre Rademaker (Sep 02 2020 at 01:39):

yes, I found its definition! Thank you

#### Kyle Miller (Sep 02 2020 at 05:09):

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:

Last updated: May 14 2021 at 06:16 UTC