## Stream: new members

### Topic: Turning a proof by cases into a linear proof

#### Aniruddh Agarwal (Jun 25 2020 at 17:12):

Consider the following proof:

def non_decreasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≤ f x₂

example (f : ℝ → ℝ) (h : non_decreasing f) (h' : ∀ x, f (f x) = x) : ∀ x, f x = x :=
begin
intro x,
specialize h' x,
unfold non_decreasing at h,
cases le_total (f x) x with,
{ specialize h (f x) x h_1,
rw h' at h,
exact le_antisymm h_1 h },
{ specialize h x (f x) h_1,
rw h' at h,
exact le_antisymm h h_1 }
end


The proof for each case is basically the same (with the only difference being the calls to le_antisymm, which are also the same modulo the symmetry of equality). Is there any way I can make the proof completely linear?

#### Yakov Pechersky (Jun 25 2020 at 17:51):

example (f : ℝ → ℝ) (h : non_decreasing f) (h' : ∀ x, f (f x) = x) : ∀ x, f x = x :=
begin
intro x,
specialize h' x,
cases le_total x (f x);
linarith [h _ _ h_1]
end


#### Yakov Pechersky (Jun 25 2020 at 17:52):

Still splits into cases, but both are just dealing with linear arithmetic, as you pointed out, and the terms can be inferred from the goal for the h hypothesis

Thanks!

#### Aniruddh Agarwal (Jun 25 2020 at 17:59):

This wasn't quite what I was hoping for, but I'm still very satisfied with the solution you provided

#### Yakov Pechersky (Jun 25 2020 at 18:02):

What were you hoping for?

#### Aniruddh Agarwal (Jun 25 2020 at 18:08):

I'm not sure honestly

#### Jalex Stark (Jun 25 2020 at 20:49):

you might have been looking for tactic#wlog

#### Aniruddh Agarwal (Jun 26 2020 at 00:28):

Jalex Stark said:

you might have been looking for tactic#wlog

Can you explain?

#### Jalex Stark (Jun 26 2020 at 00:30):

it is supposed to be similar to the mathematician's "without loss of generality", which means "if you give me a proof of one case, I'll show you how to turn it into a proof of the others"

#### Jalex Stark (Jun 26 2020 at 00:30):

i, uh, don't really know how to use it

#### Aniruddh Agarwal (Jun 26 2020 at 00:31):

I'll have to remind myself of what I was originally trying to do, but I'll take a look at this in a few minutes. wlog sounds like it could be very useful

#### Kevin Buzzard (Jun 26 2020 at 07:06):

It's not as powerful as mathematician's WLOG. I'm not sure it's up to this task.

Last updated: Dec 20 2023 at 11:08 UTC