Contrapositive law without excluded middle?

Stream: new members

[Golol]

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]

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

[Kevin Buzzard]

Yes, you have to intro or lam until the goal is false.

[Kevin Buzzard]

and then put together what you have to make a proof of false from your contradictory assumptions.

[Golol]

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]

Section 3 of what?

[Golol]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Golol]

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

[Golol]

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]

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]

Tactic mode is a much better model for a mathematician

[Golol]

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

[Golol]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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