Zulip Chat Archive

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?

Yakov Pechersky (Sep 02 2020 at 01:39):

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: Dec 20 2023 at 11:08 UTC