natural number hell

Stream: general

[Patrick Massot]

I want to use big.map once I have the map

[Patrick Massot]

I should push something so that you can see the context

[Mario Carneiro]

and then the f will be applied to the functions P and F... then what?

[Patrick Massot]

https://github.com/PatrickMassot/bigop/blob/master/src/bigop.lean#L343

[Mario Carneiro]

wait, so you want the function f to be i |-> a+b-i?

[Mario Carneiro]

then why are you mapping with something else in the lemma?

[Patrick Massot]

The problem is reverse_range' is about your range', with start and length, and my goal is to have the maths range', with start and end

[Mario Carneiro]

Think of the problem in reverse. You want the theorem to say a+b-i at the end, so you want f to be \lam i, a+b-i when you apply big.map; the reverse theorem just adds a list.reverse on the set. So you should be proving reverse (range' a b) = map (λ i, a+b-i) (range' a b)

[Mario Carneiro]

that is, without any algebraic rearrangement this is exactly what you need to fill the gap in the proof. Right?

[Patrick Massot]

Maybe I did so many detours I forgot the goal on the road

[Patrick Massot]

It seems I still need a + (b + 1 - a) - i = a + b - i (still assuming i ∈ range' a (b + 1 - a))

[Mario Carneiro]

that's easy though, it is one of the add_sub theorems

[Patrick Massot]

I think we already saw that one

[Mario Carneiro]

nat.add_sub_cancel', which requires a <= b + 1

[Mario Carneiro]

Note that your assumption is sufficient to prove this, but only in a circuitous fashion, do you have any more direct evidence that a <= b+1?

[Patrick Massot]

wait

[Mario Carneiro]

wait

[Mario Carneiro]

your theorem is nonsense

[Patrick Massot]

your theorem is nonsense

[Patrick Massot]

reverse (range' a b) = map (λ i, a+b-i) (range' a b) is not true

[Patrick Massot]

I changed all statements so many times...

[Mario Carneiro]

I'm rather confused by the dual use of range' btw, could you give it another name? range'' maybe?

[Patrick Massot]

You mean in the name of reverse_range'?

[Mario Carneiro]

I mean range' a b = [a, ..., b] vs range' a b = [a, ..., a+b]

[Mario Carneiro]

pretty sure both functions are being called range'

[Patrick Massot]

I don't redefine range'

[Mario Carneiro]

What is your definition?

[Patrick Massot]

I use your range'

[Mario Carneiro]

oh I see

[Patrick Massot]

But always in range' a (b+1-a)

[Mario Carneiro]

In that case I need to state the theorem above with your bounds

[Mario Carneiro]

reverse (range' a (b+1-a)) = map (λ i, a+b-i) (range' a (b+1-a))

[Patrick Massot]

yes, this is correct

[Patrick Massot]

(not that I can prove it, but I can check it on examples)

[Patrick Massot]

But I wanted to deduce it from a version involving only range' a b in LHS

[Patrick Massot]

hence the "arithmetic" trouble

[Patrick Massot]

But indeed this is the statement which makes big.range_anti_mph trivial to prove from the previous results

[Mario Carneiro]

Well, there are a lot of free endpoints in the reverse theorem, maybe you need to generalize it?

[Patrick Massot]

what reverse theorem?

[Mario Carneiro]

I'm thinking:

reverse (range' a (n + 1)) = map (λ i, c-i) (range' b (n + 1))

subject to an equation relating a,b,c

[Mario Carneiro]

Actually I think we need another generalization of range' that varies the step too

[Mario Carneiro]

that would make this easy

[Patrick Massot]

I need to go to my office, but the situation improved a lot: https://github.com/PatrickMassot/bigop/blob/master/src/bigop.lean#L335-L341 Thank you very much

[Patrick Massot]

I hope I'll be able to prove that last missing lemma later if you don't have time to do it properly

[Mario Carneiro]

I did it properly. Here are the lemmas I added:

theorem map_add_range' (a) : ∀ s n : ℕ, map ((+) a) (range' s n) = range' (a + s) n
| s 0     := rfl
| s (n+1) := congr_arg (cons _) (map_add_range' (s+1) n)

theorem range_succ_eq_map (n : ℕ) : range (n + 1) = 0 :: map succ (range n) :=
by rw [range_eq_range', range_eq_range', range',
       add_comm, ← map_add_range'];
   congr; exact funext one_add

theorem reverse_range' : ∀ s n : ℕ,
  reverse (range' s n) = map (λ i, s + n - 1 - i) (range n)
| s 0     := rfl
| s (n+1) := by rw [range'_concat, reverse_append, range_succ_eq_map];
  simpa [show s + (n + 1) - 1 = s + n, from rfl, (∘),
    λ a i, show a - 1 - i = a - succ i,
    by rw [nat.sub_sub, add_comm]; refl]
  using reverse_range' s n

[Patrick Massot]

Thank you Mario! I already had the first one at https://github.com/PatrickMassot/bigop/blob/master/src/bigop.lean#L126

[Patrick Massot]

Maybe I should learn to do induction using pattern matching

[Patrick Massot]

I read too quickly, I thought you proved the lemma I needed

[Patrick Massot]

But your RHS doesn't even contains range'

[Patrick Massot]

Proving the lemma I stated from what you proved seems to be as much work as a direct proof, no?

[Mario Carneiro]

You still have some algebra before you get to the exact version you need, but you can put reverse_range', range_eq_range', map_add_range' and map_map together and then do some algebra

[Mario Carneiro]

theorem range'_eq_map_range (s n : ℕ) : range' s n = map ((+) s) (range n) :=
by rw [range_eq_range', map_add_range']; refl

example (a b : ℕ) : reverse (range' a (b+1-a)) = map (λ i, a+b-i) (range' a (b+1-a)) :=
begin
  rw [reverse_range', range'_eq_map_range, map_map],
  apply map_congr, intros i H,
  simp at *,
  rw [nat.add_sub_add_left, nat.add_sub_cancel'], {refl},
  refine (le_total _ _).resolve_left (λ h, _),
  rw sub_eq_zero_of_le h at H,
  exact not_lt_zero _ H
end

[Patrick Massot]

Thank you very much Mario! I'm still not convinced this is simpler than a direct attack on this lemma, but I very much relieved to have it.

[Patrick Massot]

What is this resolve_left thing?

[Patrick Massot]

The state at the point where you write this, a b i : ℕ, H : i < b + 1 - a ⊢ b + 1 ≥ a is typically something that could have led me to harm my computer.

[Patrick Massot]

I also note that you used simp at * in the middle of a proof. Isn't this frowned upon according to mathlib's docs?

[Mario Carneiro]

That's actually a really subtle thing, it wouldn't work if it was i <= b+1-a

[Patrick Massot]

What do you mean it wouldn't work? The statement would still be true, right?

[Mario Carneiro]

no

[Patrick Massot]

This is crazy

[Mario Carneiro]

if i is zero then b+1 could be less than a

[Patrick Massot]

Did I mentioned I hate this substraction?

[Mario Carneiro]

the argument is basically that when you subtract small minus large you get 0, so since i is less than the subtraction it isn't zero so it is in the proper domain

[Mario Carneiro]

You could also have taken a <= b+1 as an assumption to the theorem if you like

[Patrick Massot]

I still don't know what resolve_left stands for

[Mario Carneiro]

or.resolve_left

[Kenny Lau]

@Patrick Massot The type of le_total _ _ is or _ _

[Kenny Lau]

So (le_total _ _).resolve_left means or.resolve_left (le_total _ _)

[Patrick Massot]

Thanks

[Patrick Massot]

to both of you

[Patrick Massot]

So the strategy here is some variation on a case disjunction, right?

[Patrick Massot]

Is it possible to use by_cases instead? (I only try to understand, I don't really want to use by_cases)

[Kenny Lau]

by_cases uses p or not p instead of any arbitrary p or q

[Patrick Massot]

It's true that le_total is almost but not quite like this

[Kenny Lau]

however I don't see the difference between or.resolve_left (le_total _ _) and le_of_not_le

[Patrick Massot]

I still don't understand why the goal after this refine is false

[Kenny Lau]

refine (le_total _ _).resolve_left (λ h, _)

[Kenny Lau]

the expected type of (λ h, _) is not (le _ _)

[Kenny Lau]

so h has type le _ _

[Kenny Lau]

so _ has type false

[Patrick Massot]

Indeed the mysterious line has the same effect as apply le_of_not_le, by_contradiction h,

[Kenny Lau]

try refine le_of_not_le (λ h, _)

[Mario Carneiro]

le_of_not_le would also have worked

[Kenny Lau]

@Mario Carneiro entao eu ganho?

[Mario Carneiro]

vc ganhou

[Kenny Lau]

:D

[Patrick Massot]

The proof of le_of_not_le is exactly this or.resolve_left le_total

[Patrick Massot]

But indeed Kenny's solution will probably be easier to remember for me

[Patrick Massot]

So, what should we do with all those lemmas we discussed in the last few days. Do you want me to prepare a PR? Are you doing it yourself?

[Mario Carneiro]

I've got a pot brewing, you can hold onto them locally until then

[Patrick Massot]

No problem

[Patrick Massot]

I extracted everything from my bigop file. It's now all in https://github.com/PatrickMassot/bigop/blob/master/src/pending_lemmas.lean if you want to make sure you have everything that was discussed here

[Patrick Massot]

It's bedtime now. Thank you very much again!

[Patrick Massot]

I have three substractions now :fearful: H : N ≥ 1, hyp : 0 ≤ i ∧ i < N ⊢ N - (N - 1 - i) = i + 1

[Patrick Massot]

Isn't it a way to first prove that we would get the same result in Z, because each substraction comes with its relevant inequality, and then ring?

[Mario Carneiro]

yes, of course

[Mario Carneiro]

just use int.cast_sub

[Patrick Massot]

how does that work?

[Mario Carneiro]

that is, use int.cast_inj to convert the natural number equality to a Z equality, and then use int.cast_add, int.cast_sub etc lemmas to move the arrows down to the bottom

[Patrick Massot]

Looking at the statement is pretty puzzling

[Mario Carneiro]

simp will do the latter part

[Chris Hughes]

example {i N : ℕ} (H : N ≥ 1) (hyp : 0 ≤ i ∧ i < N) : N - (N - 1 - i) = i + 1 :=
have 1 + i ≤ N, by rw add_comm; exact hyp.2,
by rw [nat.sub_sub, nat.sub_sub_self this, add_comm]

[Kenny Lau]

and the winner is...

[Mario Carneiro]

^ or just prove it directly

[Patrick Massot]

Thanks Chris, but I'm really tired of those direct proofs

[Patrick Massot]

I want a systematic method

[Mario Carneiro]

example {i N : ℕ} (H : N ≥ 1) (hyp : 0 ≤ i ∧ i < N) : N - (N - 1 - i) = i + 1 :=
by rw [nat.sub_sub, add_comm, nat.sub_sub_self hyp.2]

[Kenny Lau]

and the winner is...

[Chris Hughes]

Is it poor form to use exact hyp.2 instead of exact nat.succ_le_of_lt hyp.2?

[Mario Carneiro]

meh

[Kenny Lau]

maybe you should replace exact hyp.2 with cc

[Kenny Lau]

I mean, it isn't like you can't prove H from hyp...

[Mario Carneiro]

in general you should minimize your implicit definitional unfolding, but some things are too foundational to change at this point and I assume it will stay that way

[Patrick Massot]

I don't know how to use int.cast_inj

[Mario Carneiro]

oops, I mean int.coe_nat_inj'

[Mario Carneiro]

example {i N : ℕ} (H : N ≥ 1) (hyp : 0 ≤ i ∧ i < N) : N - (N - 1 - i) = i + 1 :=
by rw [← int.coe_nat_inj', int.coe_nat_sub, int.coe_nat_sub, int.coe_nat_sub]

produces a bunch of side conditions about less equal stuff

[Mario Carneiro]

actually it's a bit messy since the side conditions themselves involve natural number subtraction, so you need to rewrite them too or else prove them directly

[Mario Carneiro]

If you want to take this route I would suggest not writing natural number subtraction at all when you can help it, so that you don't need to deal with nested subtractions and the like

[Mario Carneiro]

that is, just use integer subtraction and convert back to natural numbers at the end with int.to_nat if necessary

[Patrick Massot]

"not writing natural number subtraction at all" is my greatest Lean dream

[Mario Carneiro]

A simple way to actually do that is to replace m - n everywhere with int.to_nat (m - n) (where the subtraction there is actually integer subtraction now)

[Patrick Massot]

I need to go, I'll try tonight. Thanks you!

[Mario Carneiro]

That way the funky zero saturation operator is explicit

[Kevin Buzzard]

I want a systematic method

How about this: replace every occurrence of X <= Y with Y = X + c and replace every occurrence of X < Y with Y = X + c + 1, and then just use add_sub_cancel or whatever it's called -- a + b - b = a. It would not surprise me if this algorithm worked every time.

[Kevin Buzzard]

Example: you know i < N and you want to prove N - (N - 1 - i) = i + 1, well, write N = i + 1 + j and -- oh -- you also need X - (Y + Z) = X- Y - Z -- you get N - (j + 1 + i - (1 + i)) which is N - j which is i + 1 + j - j which is i + 1

[Kevin Buzzard]

I am assuming that your mathematician's goals never actually rely on the fact that a - b = 0 if b>a

[Kevin Buzzard]

This should reduce everything to nat.sub_sub (if memory serves -- is it called that?) and add_sub_cancel or whatever it's called (not in front of Lean right now).

[Kevin Buzzard]

oh and associativity and commutativity of course

[Kevin Buzzard]

Make them simp lemmas and see if simp can do it after you make the substitutions

[Kevin Buzzard]

(if they're not simp lemmas already)

[Kevin Buzzard]

Might not be the optimal approach but it looks pretty systematic to me

[Chris Hughes]

replace every occurrence of X <= Y with `Y = X + c

This bit sounds hard to do with simp, since it involves casing on exists.

[Kevin Buzzard]

you just introduce another variable

[Kevin Buzzard]

you do all that before you start the simp