contrapose

Stream: lean4

[Aron]

Does contraposition not exist yet?

[Aron]

Actually, does contradiction exist yet??

[Sébastien Michelland]

It's built in the theory (the calculus of constructions). The definition of ¬P is P → False, where False is an absurd fact. Hence, ¬P is itself the statement of the contradiction theorem for P. If you have, let's say, h₁: ¬P and h₂: P then h₁ h₂ is of type False and can prove anything (many tactics do this automatically, but you can also use nomatch for that).

Contraposition works in a similar fashion:

theorem contraposition {P Q: Prop} (h: P → Q): ¬Q → ¬P :=
  fun not_Q P => not_Q (h P)

Once you unfold the definitions, you are left with P → Q, Q → False and P to prove False, which is straightforward.

[Aron]

Yes, but if I'm trying to prove by contraposition, how would I do that? There should be some command to add a hypothesis that is the negation of the current goal and to replace the current goal with False.

[Aron]

Sorry, I mean contradiction.

[Sébastien Michelland]

That would be docs4#Classical.byContradiction.

[Aron]

leanpkg doesn't seem to exist on my system?

error: toolchain 'leanprover/lean4:stable' does not have the binary `/Users/atobi16/.elan/toolchains/leanprover--lean4---stable/bin/leanpkg`

[Sébastien Michelland]

I'm not sure about the distribution, but since this is in Init you should have it automatically in any Lean4 script:

#check Classical.byContradiction
-- Classical.byContradiction : (¬?m.28684 → False) → ?m.28684

[Aron]

It's indeed there, but it still doesn't want to work in my proof.

#check Classical.byContradiction
def exunique (p : α → Prop) := ∃ (x : α), (p x ∧ ∀ y, p y → x = y)

syntax "∃!" term "," term: term
macro_rules
| `(∃! $t:term, $p:term) => `(exunique (fun $t => $p))

class incidence (point line: Type) (inc:point → line → Prop) :=
(one: ∀ P Q, P ≠ Q → ∃! l, inc P l ∧ inc Q l)
(two: ∀ l, ∃ P Q, P ≠ Q ∧ inc P l ∧ inc Q l)
(three: ∃ P Q R, P≠ Q∧ Q≠ R∧ P≠ R∧ ∀ l, ¬(inc P l ∧ inc Q l ∧ inc R l))

theorem t1
(point line:Type)
(inc:point → line → Prop)
[i: incidence point line inc]:
∀ l m,
l ≠ m
→ (∃ P, inc P l ∧ inc P m)
→ (∃! P, inc P l ∧ inc P m)
:= by
intro l m hlnm hex
cases hex with | intro P hPlm =>
rw [exunique]
exists P
apply And.intro
exact hPlm
cases hPlm with | intro hPl hPm =>
intro Q
intro hQlm; cases hQlm with | intro hQl hQm =>
Classical.byContradiction

trying.lean:31:1 <- last line
unknown tactic

[Julian Berman]

leanpkg doesn't seem to exist on my system?

Lean 4 uses lake rather than leanpkg. See e.g. https://leanprover.github.io/lean4/doc/quickstart.html#create-a-lean-project.

[Sébastien Michelland]

It's a theorem, you need to apply it. The full tactic would be apply Classical.byContradiction.

[Henrik Böving]

Aron said:

It's indeed there, but it still doesn't want to work in my proof.

#check Classical.byContradiction
def exunique (p : α → Prop) := ∃ (x : α), (p x ∧ ∀ y, p y → x = y)

syntax "∃!" term "," term: term
macro_rules
| `(∃! $t:term, $p:term) => `(exunique (fun $t => $p))

class incidence (point line: Type) (inc:point → line → Prop) :=
(one: ∀ P Q, P ≠ Q → ∃! l, inc P l ∧ inc Q l)
(two: ∀ l, ∃ P Q, P ≠ Q ∧ inc P l ∧ inc Q l)
(three: ∃ P Q R, P≠ Q∧ Q≠ R∧ P≠ R∧ ∀ l, ¬(inc P l ∧ inc Q l ∧ inc R l))

theorem t1
(point line:Type)
(inc:point → line → Prop)
[i: incidence point line inc]:
∀ l m,
l ≠ m
→ (∃ P, inc P l ∧ inc P m)
→ (∃! P, inc P l ∧ inc P m)
:= by
intro l m hlnm hex
cases hex with | intro P hPlm =>
rw [exunique]
exists P
apply And.intro
exact hPlm
cases hPlm with | intro hPl hPm =>
intro Q
intro hQlm; cases hQlm with | intro hQl hQm =>
Classical.byContradiction

trying.lean:31:1 <- last line
unknown tactic

are you familiar with proof writing in Lean 3 or 4 already, if not I'd recommend to read theorem proving in Lean 4 before starting with this.

[Aron]

I've read up. Still managing to stumble over myself.