Feedback (Heine Borel in progress)

Stream: new members

[Guillermo Barajas Ayuso]

Hi, I have uploaded some code in the link https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/Topology/Heine-Borel%20(incomplete) , I'll leave it here in case you want to give me some feedback. Thank you for your time! :-)

[Kevin Buzzard]

theorem for_all_not_all {α : Type u} (P Q R: α → Prop):
(∀ x (H : R x), ¬ (P x ∧ Q x)) ↔  ∀ x (H : R x), P x → ¬ Q x :=
⟨λ Hnand x Hx, not_and.mp $ Hnand x Hx, λ Hton x Hx, not_and.mpr $ Hton x Hx⟩

Mathlib would prefer that kind of style to your tactic proof. I always suspect that such results are either in mathlib already or easily deducible. Looking at the proof I feel like it's one of those ones which could be shortened with some magic use of function.comp like in https://xenaproject.wordpress.com/2018/05/19/function-composition/ .

Oh wait --

theorem for_all_not_all {α : Type u} (P Q R: α → Prop):
(∀ x (H : R x), ¬ (P x ∧ Q x)) ↔  ∀ x (H : R x), P x → ¬ Q x := by simp [not_and]

[Kevin Buzzard]

The simp proof -- the proof takes 50% longer to process but the parser takes far less time parsing :-) End result is that both versions run in about the same time.

[Kevin Buzzard]

I have an error at line 431 by the way, and there are 6 sorrys. Do you need help filling them in?

[Kevin Buzzard]

Re the argument on line 431: there is already nat.lt_pow_self.

theorem le_pow (n : ℕ) : (n : ℝ) ≤ (2 : ℝ) ^ n :=
begin
  show (n : ℝ) ≤ ((2 : ℕ) : ℝ) ^ n,
  rw ←nat.cast_pow,
  rw nat.cast_le,
  exact le_of_lt (nat.lt_pow_self (dec_trivial) n),
end

[Kevin Buzzard]

notation ⟦a,b] := closed_interval a b

This is a hilarious idea. Does it work? Re-using notation which is already used is a dangerous game, but given that as far as I know in Lean every use of ] in notation comes with an [ too, so avoiding the [ in this case gives you better leeway.

[Kevin Buzzard]

theorem le_ε_to_le (Hle_ε : ∀ ε > 0, a ≤ b + ε) : a ≤ b := sorry These things are really annoying if they're not there already. @Kenny Lau how is one supposed to prove stuff like this?

[Kevin Buzzard]

theorem le_ε_to_le (Hle_ε : ∀ ε > 0, a ≤ b + ε) : a ≤ b :=
le_of_not_gt $ λ H, begin
  have H2 := Hle_ε ((a - b) / 2) _,
    revert H2, -- because it makes the rewriting easier
    rw [←(mul_le_mul_right (show (2 : ℝ) > 0, by norm_num)),add_mul,
    div_mul_cancel _ (show (2 : ℝ) ≠ 0, by norm_num),
   (show b * 2 + (a - b) = a + b, by ring),
    mul_two,add_le_add_iff_left],
    exact not_le_of_gt H,
  apply div_pos _ (show (0 : ℝ) < 2, by norm_num),
  exact sub_pos_of_lt H
end

This time last year there was no norm_num and no ring -- imagine how hard it was doing M1F example sheets!

[Kenny Lau]

theorem le_ε_to_le {α : Type*} [linear_ordered_field α] {a b : α}
  (Hle_ε : ∀ ε > 0, a ≤ b + ε) : a ≤ b :=
le_of_not_lt $ λ H, not_lt_of_le (Hle_ε ((a-b)/2) (half_pos $ sub_pos_of_lt H)) $
calc  b+(a-b)/2
    < b+(a-b) : add_lt_add_left (half_lt_self (sub_pos_of_lt H)) _
... = a : add_sub_cancel'_right b a

[Kevin Buzzard]

theorem between_shorter (H1 : b ≤ c) (H2 : c ≤ a) (H3 : b ≤ d) (H4 : d ≤ a) :
abs (c - d) ≤ abs (a - b) :=
begin
  rw abs_of_nonneg (sub_nonneg_of_le $ le_trans H1 H2),
  rw abs_le, split,
    rw neg_sub,
    exact _root_.sub_le_sub H1 H4,
    exact _root_.sub_le_sub H2 H3,
end

This one wasn't too bad -- proof felt natural.

[Kenny Lau]

theorem between_shorter {α : Type*} [decidable_linear_ordered_comm_group α] {a b c d : α}
  (H1 : b ≤ c) (H2 : c ≤ a) (H3 : b ≤ d) (H4 : d ≤ a) :
  abs (c - d) ≤ abs (a - b) :=
calc  abs (c - d)
    ≤ a - b : abs_sub_le_iff.2 ⟨sub_le_sub H2 H3, sub_le_sub H4 H1⟩
... = abs (a - b) : (abs_of_nonneg $ sub_nonneg_of_le $ le_trans H1 H2).symm

[Kevin Buzzard]

lemma half_le_self (H : 0 ≤ a) : a / 2 ≤ a := begin
  rw div_le_iff (show (2 : ℝ) > 0, by norm_num),
  rw mul_two,
  rwa le_add_iff_nonneg_left,
end

[Kenny Lau]

lemma half_le_self {α : Type*} [linear_ordered_field α] {a : α}
  (H : 0 ≤ a) : a / 2 ≤ a :=
div_le_of_le_mul two_pos $ (two_mul a).symm ▸ le_add_of_nonneg_left H

[Kevin Buzzard]

Should there be training or exercises or something for people who need stuff like this?

[Rob Lewis]

import tactic.linarith

lemma half_le_self {α : Type*} [linear_ordered_field α] {a : α}
  (H : 0 ≤ a) : a / 2 ≤ a :=
by linarith

theorem between_shorter {α : Type*} [decidable_linear_ordered_comm_ring α] {a b c d : α}
  (H1 : b ≤ c) (H2 : c ≤ a) (H3 : b ≤ d) (H4 : d ≤ a) :
  abs (c - d) ≤ abs (a - b) :=
by unfold abs max; split_ifs; linarith

[Kevin Buzzard]

...or maybe even a tactic!

[Scott Morrison]

Next we make a wrapper for linarith that unfolds stuff that is secretly arithmetic. :-)

[Kevin Buzzard]

    < b+(a-b) : [blah]
... = a : add_sub_cancel'_right b a

Kenny -- you misspelt "by ring".

Why should mathematican end users have to know that the triviality b + (a - b) = a is called add_sub_cancel'_right? Surely we should just be able to write something which generates this proof for us, and then internally replaces what we wrote with this add_sub_cancel' nonsense? I'm assuming that using ring to do this is not recommended because it might take about 10 times as long. It's all well and good people writing clever tactics which solve all goals of this nature, but then we end up in this situation where people are encouraged not to use them and instead get an encyclopedic knowledge of all this add_sub_cancel'_right nonsense, or learn how to look it up. I guess what I'm asking for is a tactic which does by ring but only takes a long time the first time -- like Scott's tidy trick. Can this be done in other cases somehow?

[Kevin Buzzard]

@Guillermo Barajas Ayuso -- linarith is a brand new tactic which Rob wrote. You might find it useful in other situations.

[Kenny Lau]

@Rob Lewis re between_shorter, my version works for objects without multiplication

[Rob Lewis]

Can this be done in other cases somehow?

It can in principle. But things like ring often don't try to produce short or pretty output, because it's way harder to write something that does that and works generally. And the output will probably still look messy on anything more complicated than that basic example.

[Rob Lewis]

I wouldn't expect ring to be unreasonably slow for examples like that, either.

[Scott Morrison]

Hi @Rob Lewis, in the interest in making linarith even easier to use, what would you think of having it automatically try exfalso if the goal doesn't look like linear arithmetic?

[Scott Morrison]

It's of course possible to achieve this by: linarith <|> (exfalso >> linarith), but I worry that this is inefficient.

[Scott Morrison]

(Actually maybe it isn't --- if the goal is something else, linarith I guess fails before doing any work already...)

[Rob Lewis]

That's completely reasonable. I actually thought it did that already, but apparently I added a check for a false goal.

[Rob Lewis]

If there are no inequality hypotheses, it'll fail immediately. If there are hypotheses it can work with, it will try, but failure is a lot quicker than success.

[Rob Lewis]

I'll add a config option for trying to prove arbitrary goals by exfalso.

[Keeley Hoek]

This sort of follows-up what Kevin was saying before: it seems to me that it'd be really great if Lean had a facility for tactics to opt-in to cache what they did on invocation, not just in the interactive lean session (memoizing there), but statically in a file in the repository.

[Keeley Hoek]

The (my?) dream is that mathlib (or just mathematics) could be filled with tactic proofs which call shiny-new maybe-expensive tactics which do all of your dirty-work for you in one line (e.g by super_ring), without any detrimental performance impact; if you change the first line of a file, the expensive tactic proofs in the file below instantly recompile; and if you change the statement of a lemma the cached proof will just silently fail to typecheck and the tactic proof will be re-run. mathlib can be distributed with these cache-files, or they could just be built the first time mathlib is built, and everyone is happy.

[Keeley Hoek]

Instead it seems like in many places people have to steer clear of the "big guns", or at least only use them to get a term/tactic-mode proof which they will replace them with. To me, this seems just like a manual way of doing the same sort of static caching, but the tools which helped generate your easy proof (e.g. ring → add_sub_cancel'_right) are lost forever (and don't auto-fix your proof when you e.g. tinker with your lemma).

[Patrick Massot]

    < b+(a-b) : [blah]
... = a : add_sub_cancel'_right b a

Kenny -- you misspelt "by ring".

Or "by abel"

[Kevin Buzzard]

Or even by simp. Grr. What is the point of this abel tactic? I still haven't found an example which simp can't do.

[Patrick Massot]

Hopefully abel is a step towards the module tactic which should be more useful