Zulip Chat Archive

Stream: new members

Topic: implication introduction


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 01:30):

Tactic mode given your first example:

intro pA,
exact h1

view this post on Zulip Alexandre Rademaker (Sep 02 2020 at 01:30):

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

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 01:34):

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

view this post on Zulip 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.

view this post on Zulip Alexandre Rademaker (Sep 02 2020 at 01:36):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 01:38):

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

view this post on Zulip Alexandre Rademaker (Sep 02 2020 at 01:38):

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

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 01:39):

Yes, it is

view this post on Zulip Alexandre Rademaker (Sep 02 2020 at 01:39):

yes, I found its definition! Thank you

view this post on Zulip 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