# Zulip Chat Archive

## Stream: new members

### Topic: Contrapositive law without excluded middle?

#### Golol (May 10 2020 at 15:30):

Hi, I am trying to solve the following exercise:

example : (p → q) → (¬q → ¬p) := sorry

I have a working proof using em, but the exercise is listed as working without classical.

I don't see a way of getting to \not q without arguing that p being true would lead to absurd (needs em to make an or-elim).

Is ther a way to do this without em?

#### Kenny Lau (May 10 2020 at 15:32):

hint: (not p) is defined to be (p -> false)

#### Kevin Buzzard (May 10 2020 at 15:33):

Yes, you have to `intro`

or `lam`

until the goal is `false`

.

#### Kevin Buzzard (May 10 2020 at 15:34):

and then put together what you have to make a proof of `false`

from your contradictory assumptions.

#### Golol (May 10 2020 at 15:41):

aah thanks, perfect!

Not wanting to open a new thread, there was something else I wondered about.

The tutorial in section 3 (Propositional logic) does such a nice job of showing you how beautifully you can dobasically everything with "->", but then hits you with things like add.elim, or.intro etc. which seem clunky at first and a bit "artificial" (but they probably make more sense later).

I thinkthat basically:

variables p q r: Prop

#constant and.intro : p->q->p and q

#constant and.elim_left : p and q -> p

#constant or.intro_left: p->p or q

#constant or.elim (p or q) -> (p->r) -> (q -> r) -> r

etc.

should achieve exactly the same, at least in this specific section about Propositional logic?

#### Kevin Buzzard (May 10 2020 at 15:42):

Section 3 of what?

#### Golol (May 10 2020 at 15:43):

https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html#exercises

#### Kevin Buzzard (May 10 2020 at 15:43):

These things are essentially constants anyway, they are basically defined when you create the types

#### Kevin Buzzard (May 10 2020 at 15:44):

For a tactic-based take on it, try Proposition World in the natural number game.

#### Golol (May 10 2020 at 15:46):

Im only at quantifiers, idk tactics yet :D. But I think this stuff is super cool.

#### Golol (May 10 2020 at 15:47):

I wanna learn this, get up to date with the state of the art of analysis/pde in the database and get going

#### Kevin Buzzard (May 10 2020 at 15:48):

If you start with the natural number game then you go straight into tactics and you don't have to learn all this #constant and and.elim stuff. I agree that they're artificial, they're not the way a mathematician thinks about how to manipulate these things.

#### Kevin Buzzard (May 10 2020 at 15:48):

Tactic mode is a much better model for a mathematician

#### Golol (May 10 2020 at 15:50):

Then Ill do that. After I read the inductive types chapter though. Thanks!

#### Golol (May 10 2020 at 15:52):

(Im still living in the undergrad fantasy world where you should linearily understand all preceding mathematics to be allowed to use something)

#### Kevin Buzzard (May 10 2020 at 15:57):

The natural number game is basically an argument that Theorem Proving In Lean is written in the wrong order for mathematicians.

#### Kevin Buzzard (May 10 2020 at 15:58):

Our forthcoming book Mathematics in Lean will be developing the theory in an order more appropriate for mathematicians, and there will certainly be tactics before `and.intro`

.

#### Mario Carneiro (May 10 2020 at 17:03):

Golol said:

(Im still living in the undergrad fantasy world where you should linearily understand all preceding mathematics to be allowed to use something)

The nice thing about formalized mathematics is that this is actually a viable strategy

Last updated: May 14 2021 at 02:15 UTC