non-boring but still simple example of a disjunctive goal?

Stream: new members

[rzeta0]

I'm developing simple almost-minimal examples of lean proofs as I myself learn lean as a beginner.

Currently I'm trying to think of a good example of a proof that has a disjunctive "or" goal.

Sadly the examples I can think of are mathematically very boring.

My request is for simple beginner-friendly suggestions for a disjunctive proof that is:

• not mathematically boring
• but not mathematically difficult or tortuous - I don't want to scare anyone away, nor distract them from the main learning point about the structure of a lean program for a disjunctive goal

What do I mean by "easy"? Something that a person who studied maths to age 16 can understand. So that excludes the fancy stuff about limits of weird functions eg $\lim_{n \to \infty}\sin^{2n}(x)$

---

My boring example is as follows. The maths level is about right. But the theorem is not interesting.

import Mathlib.Tactic

example {x : ℤ} (h : x = -1) : x^2 = 1 ∨ x^2 = -1 := by
  left
  calc
    x^2 = (-1)^2 := by rw [h]
    _ = 1 := by norm_num

[Dan Velleman]

How about this:

example (x : Real) (h : x ≤ x ^ 2) : x ≤ 0 ∨ 1 ≤ x

[rzeta0]

Dan Velleman said:

How about this:

example (x : Real) (h : x ≤ x ^ 2) : x ≤ 0 ∨ 1 ≤ x

This is certainly interesting and at about the right level of difficulty. But the lean proof itself might be too difficult. I myself can't think how I'd do it with the basic tactics beginners first learn.

[Dan Velleman]

Or this:

example (U : Type) (A B C : Set U) :
    A \ (B \ C) ⊆ (A \ B) ∪ C

(The initial goal is not a disjunction, but after a couple of steps it will be.)

[rzeta0]

Dan Velleman said:

Or this:

example (U : Type) (A B C : Set U) :
    A \ (B \ C) ⊆ (A \ B) ∪ C

(The initial goal is not a disjunction, but after a couple of steps it will be.)

We haven't done sets yet - only simple numbers in N, Z, Q or R. But thanks for suggesting, I do appreciate it.

[Dan Velleman]

rzeta0 said:

Dan Velleman said:

How about this:

example (x : Real) (h : x ≤ x ^ 2) : x ≤ 0 ∨ 1 ≤ x

This is certainly interesting and at about the right level of difficulty. But the lean proof itself might be too difficult. I myself can't think how I'd do it with the basic tactics beginners first learn.

Try starting with by_cases h2 : x ≤ 0.

[Dan Velleman]

rzeta0 said:

Dan Velleman said:

Or this:

example (U : Type) (A B C : Set U) :
    A \ (B \ C) ⊆ (A \ B) ∪ C

(The initial goal is not a disjunction, but after a couple of steps it will be.)

We haven't done sets yet - only simple numbers in N, Z, Q or R. But thanks for suggesting, I do appreciate it.

In my opinion, in Lean sets are easier than numbers, so beginners are better off starting with sets rather than numbers. (That's why I wrote the set theory game.)

[Vincent Beffara]

A simpler example than the previous one:

example (x : Real) (h : 1 ≤ x ^ 2) : x ≤ -1 ∨ 1 ≤ x := sorry

Note that your first example is not really representative because the choice of alternative is always left, independently of the value of x.

[rzeta0]

hi @Vincent Beffara thanks, your example looks like it could be the one I develop into an example.

I didn't understand (i'm a beginner) your point about only the left being true, independent of x.

It's ok for only one sub statement of a disjunction to be true for the full statement to be true?

And if x=2 then x^2=1 is not true - so there is a dependence on x?

Clearly I've misunderstood your comment.

[Edward van de Meent]

there is no case where x ^2 = -1 (since x is an integer rather than a complex number)

[rzeta0]

Hi Edward - yes, agreed.

But does that make a statement $P \lor Q$ false if the hypothesis always leads to $P$ being true?

That is, if $H \implies P$ then we still have a theorem $H \implies (P \lor Q)$ ?

I am new to mathematical logic so do correct me if I'm mistaken.

[Vincent Beffara]

It's definitely true, it is just not "non-boring" as an example