Glitch?

Stream: maths

[Colin Jones ⚛️]

Attempting to solve this goal.

import Mathlib

open Set Filter

variable (a b x : ℝ)

example : Tendsto (fun x:ℝ => x / (x^3 - 1)) (nhdsWithin 1 (Set.Iio 1)) atBot := by
  rw [← tendsto_neg_atTop_iff]
  have h : (fun x:ℝ => -(x / (x^3 - 1))) = (fun x:ℝ => x*(-x^3 + 1)⁻¹) := by
    apply funext
    intro x
    rw [mul_comm, ← div_eq_inv_mul, show (-x^3 + 1) = - (x^3 - 1) by ring, div_neg]
  have h' : 0 < (1:ℝ) := by positivity
  rw [h]
  apply Filter.Tendsto.mul_atTop h'
  clear h h'
  · refine tendsto_nhdsWithin_of_tendsto_nhds ?hf.h
    exact fun ⦃U⦄ a => a
  · have h' : (fun x:ℝ => (-x^3 + 1)) = (fun x => ((-x + 1)*(x^2 + x + 1))) := by
      apply funext
      intro x
      ring
    refine Filter.Tendsto.inv_tendsto_zero ?_
    rw [h', show (0:ℝ) = (-1+1)*(1*1 + 1 + 1) by ring]
    rw [nhdsWithin]
    apply Filter.Tendsto.inf
    · apply Filter.Tendsto.mul
      · apply Filter.Tendsto.add
        · exact tendsto_neg 1
        · exact tendsto_const_nhds
      · apply Filter.Tendsto.add
        · apply Filter.Tendsto.add
          · simp_rw [sq]
            apply Filter.Tendsto.mul
            <;> exact fun ⦃U⦄ a => a
          · exact fun ⦃U⦄ a => a
        · exact tendsto_const_nhds
    · refine tendsto_principal_principal.mpr ?h₂.a
      intro x hx
      simp [Set.mem_Ioi] at *
      have h1 : 0 < (-x + 1) := by linarith
      have h2 : 0 < (x^2 + x + 1) := by
        rw [show (x^2 + x + 1) = x*(x + 1) + 1 by ring]
        by_cases hx : -1/2 ≤ x
        · have h21' : 0 < x + 1 := by linarith
          have h21'' : x + 1 < 2 := by linarith
          rw [← neg_lt_iff_pos_add]
          calc
            -1 ≤ (-1/2) * 2 := by ring

At the very end it gives me a strange, unintended statement in the infoview saying - 1 \le -2, but (-1/2)*2 should evaluate to -1. Why does this happen?

[Colin Jones ⚛️]

Using the tactic "norm_num" instead of the last "ring" gives a goal of False as well.

[Colin Jones ⚛️]

I believe it originates from how Lean handles stuff. If I put the following command into Lean:
#eval (2)*(-1/2)
I obtain the -2 in the infoview. Can someone explain why?

[Colin Jones ⚛️]

Oh wait nevermind. I figured it out. It's because Lean is evaluating (-1/2) as -1 because the 1 and 2 are int types.

[Notification Bot]

Colin Jones ⚛️ has marked this topic as resolved.

[Notification Bot]

David Loeffler has marked this topic as unresolved.

[David Loeffler]

Yes, this is a really annoying foot-gun, that division of number literals such as -1 / 2 is interpreted as Nat or Int division by default (I've been bitten by that a good few times). I wonder if there's a way of switching this off?

By the way, in your example you can get to the final goal rather more quickly as follows:

    · refine tendsto_principal_principal.mpr ?h₂.a
      intro x hx
      simp [Set.mem_Ioi] at *
      apply mul_pos
      · linarith -- [proves 0 < -x + 1]
      · nlinarith -- [proves 0 < x ^ 2 + x + 1]

It's a pity that the automated inequality tactics aren't quite strong enough to prove 0 < (-x + 1) * (x ^ 2 + x + 1) in one go.

[Ralf Stephan]

In Sage, one gets used to writing QQ(1)/2. What would be the equivalent in Lean?

[Mario Carneiro]

(1/2 : ℚ)

[Mario Carneiro]

note that the type ascription should go on the outside because type inference mainly proceeds from outside in, unlike in Sage

[Eric Wieser]

because type inference mainly proceeds from outside in

Isn't this untrue in Lean 4 thanks to thinks like binop% and HDiv? Generally this is true, but for arithmetic operators the rule is reversed

[Eric Wieser]

Which is often confusing, because Finset.sum is not considered an arithmetic operator, so the casting rules are not the same as they are for +

[Mario Carneiro]

it's complicated

[Mario Carneiro]

but for the most basic case I would say that it is outside-in even for arithmetic operators:

#check fun x y : Nat => (x + y : Int)
-- fun x y => ↑x + ↑y : Nat → Nat → Int

[Kyle Miller]

Yeah, to first approximation it's outside-in, and it's wrong to say that "the rule is reversed".

Basic operation: it locates the entire tree of arithmetic expressions (the ones that participate in the binop%/unop%/rightact%/etc protocol), elaborates each leaf without an expected type, computes a type that everything can coerce to (the "maximal type"), then drops coercions at the leaves wherever they're needed. Just like for the Lean 3 "outside-in" description, coercions are at the leaves, but unlike pure "outside-in", (1) leaves can influence the type of the entire expression and (2) coercions can't be dropped inside the leaves, since elaboration is already completed.

If it weren't expensive, the way it could work instead is, rather than inserting coercions at leaves, is to re-elaborate each leaf with the computed maximal type. That would let the types propagate coercions deeper into subexpressions, like Finset.sum.

[Kyle Miller]

Maybe there's a more explicitly bidirectional elaboration algorithm for elaboration in general, where stage 1 calculates expected types (during which the binop%/etc. protocol figures out a maximal type to the best of its ability) and during stage 2 it elaborates with these computed expected types.

[Kevin Buzzard]

Kyle's explanation is hard for me to follow because I don't know what binop% is (is this something I should ever be typing as a user? Because I don't think I ever typed it). The lean 3 algorithm was very easy to understand and also very predictable. Now I can never predict, I just write some code and then inspect how it was elaborated.

[Kyle Miller]

@Kevin Buzzard That's definitely not meant to be an explanation for a general audience, but rather one for someone who's looked at definitions of +/-/etc. in the Init module and hasn't read the elaboration code for binop%, etc.

Here's a quickly written introductory explanation (could be better, but hopefully it helps):

Arithmetic operations (like +, -, *, ^, etc.) are specially handled during elaboration. Entire arithmetic expressions are handled at once. Working with an example, x + (y + 2) * f z is an arithmetic expression with leaf expressions x, y, 2, and f z. Recall that the elaboration process make use of an optional expected type (this expected type is only a hint, not a requirement). First, each leaf expression is elaborated without an expected type. Second, it figures out the maximal type for the whole arithmetic expression by combining its expected type along with the resulting types of each leaf expression -- it combines pairs of types by seeing which of the two can be coerced into the other. Third, it commits to this maximal type by inserting coercions at each leaf node when necessary.

The purpose of this algorithm is that arithmetic operations are heterogeneous (they do not require both arguments to have the same type, and furthermore the result can have a type that's different from the arguments), and that means elaboration gets stuck in many common cases without hints (these inserted coercions). For example, x + n would fail with x : Real and n : Nat since it would look for a HAdd Real Nat _ instance. Instead, the algorithm hints that it should use (n : Nat) : Real, and it finds the homogeneous HAdd Real Real Real instance.

[Kyle Miller]

You can also look at the source, which has module docs and at RFC lean4#2854, which has a partial explanation of this elaborator.

[Kyle Miller]

But the key is that Lean 4 has HAdd rather than just Add, and that causes some issues, since it no longer can propagate the expected type toward the arguments.

On the other hand, now there are certain Lean 3 issues that this new one doesn't have, in particular both n + z and z + n succeed in elaboration with n : Nat and z : Int. In Lean 3, the first would fail and the second would succeed, but now both succeed.

[Michael Stoll]

It still makes a difference performance-wise:

import Mathlib

set_option trace.Meta.synthInstance true

variable (a : ℕ) (b : ℤ)

count_heartbeats in -- 387
#check a + b

count_heartbeats in -- 44
#check b + a

As you can see from the trace, Lean spends some time in figuring out that there is no coercion from ℤ to ℕ in the first case...