ideas to formalize non-standard analysis

Stream: new members

[Jiatong Yang]

I want to formalize some conclusions about non-standard analysis. What should I start with? Is there any ideas?
(difficulties:The superstructures do not fit well in type theory... Should the transfer principle just be formalized as a tactic?)

[Jireh Loreaux]

Are you sure that the superstructures can't be made to fit within type theory in a reasonable way? I feel like @Violeta Hernández may be able to provide some pointers about how to go about this. Also, note that we do have docs#hyperreal

[Eric Rodriguez]

I think Violeta is on an extended Lean hiatus, btw

[Adam Topaz]

What's an example of a statement that you want to formulate? We have docs#ultraproduct (well, somewhere ;))

[Junyan Xu]

I don't know a thing about how they're used in nonstandard analysis, but superstructure seem very similar to something that appears in the con-nf project, so you might get some inspiration regarding how to formalize it in type theory from there.

[Jiatong Yang]

But I don't want to formalize the logic, which will make hyperreals hard to use. I think Lean itself is some formal logic, we can just use metaprogramming when we need to transfer from and to the non-std models.

[Jiatong Yang]

For example, when the goal is "forall x ∈ *R, there exists y ∈ *N s.t. y > x". If a tactic transfer has been finished, I can just write transfer and then the goal becomes "forall x ∈ R, there exists y ∈ N s.t. y > x".

[Jiatong Yang]

Is there any advice?

[Jireh Loreaux]

I mean, a tactic has to supply Lean with the proof terms, so you first need to encode (some version of) the transfer principle in Lean. Then you can write a tactic that uses it.

[Jiatong Yang]

I have no idea how to express superstructures without formalizing logic.

[Jiatong Yang]

Jireh Loreaux said:

I mean, a tactic has to supply Lean with the proof terms, so you first need to encode (some version of) the transfer principle in Lean. Then you can write a tactic that uses it.

I understand that. For example, I need to prove some lemmas like *(a + b) = *a + *b and so on.

[Adam Topaz]

Pinging @Aaron Anderson since he formalized Łos's theorem.

[Yaël Dillies]

I don't see the problem with formalising superstructures. As Junyan said, what we do in Con(NF) is almost what you want already.

[Jiatong Yang]

But do we need to formalize functions as sets?

[Yaël Dillies]

Absolutely not

[Anatole Dedecker]

Jireh Loreaux said:

I mean, a tactic has to supply Lean with the proof terms, so you first need to encode (some version of) the transfer principle in Lean. Then you can write a tactic that uses it.

I guess the point is that the transfer principle is in some sense a "meta theorem" (because you need to express the fact that the formula you're transfering is of first order), and we could absolutely have a tactic that does it in each concrete cases without being able to prove the general theorem. I actually tried to do exactly that one year and a half ago, and it seemed doable (you can see what I did here), but I just got bored and came back from my mandatory nonstandard hype time :)

[Aaron Anderson]

A nonstandard extension can be thought of as an elementary extension, which we have in mathlib: docs#first_order.language.elementary_embedding

[Aaron Anderson]

The trick is to choose your language carefully - you want a language where there's a symbol for every single n-ary function and relation on your Type (presumably R).

[Aaron Anderson]

The pain will be in showing that the things you want to transfer are first-order, as first-order formulas are weird-looking in our current implementation.

[Jiatong Yang]

Anatole Dedecker said:

Jireh Loreaux said:

I mean, a tactic has to supply Lean with the proof terms, so you first need to encode (some version of) the transfer principle in Lean. Then you can write a tactic that uses it.

I guess the point is that the transfer principle is in some sense a "meta theorem" (because you need to express the fact that the formula you're transfering is of first order), and we could absolutely have a tactic that does it in each concrete cases without being able to prove the general theorem. I actually tried to do exactly that one year and a half ago, and it seemed doable (you can see what I did here), but I just got bored and came back from my mandatory nonstandard hype time :)

Your code is inspiring! :tada:

[Jiatong Yang]

Anatole Dedecker said:

Jireh Loreaux said:

I mean, a tactic has to supply Lean with the proof terms, so you first need to encode (some version of) the transfer principle in Lean. Then you can write a tactic that uses it.

I guess the point is that the transfer principle is in some sense a "meta theorem" (because you need to express the fact that the formula you're transfering is of first order), and we could absolutely have a tactic that does it in each concrete cases without being able to prove the general theorem. I actually tried to do exactly that one year and a half ago, and it seemed doable (you can see what I did here), but I just got bored and came back from my mandatory nonstandard hype time :)

Why does linarith not work on hyperreals?

[Jiatong Yang]

The problem is that ↑𝓗.germ ℝ is not the same as ℝ* though they are def equal.

[Kevin Buzzard]

Feel free to not quote large posts again and again, they're just above where everyone is reading on both the browser and mobile apps, and not hard to find. This isn't email, it's a conversation

[Kevin Buzzard]

If you're working with hyperreals then you might find several things don't work because hyperreals haven't been given much love in mathlib. Maybe isolate some simple things which you'd like to work and which don't, post them as #mwe s, and maybe someone can get them working

[Jiatong Yang]

import data.real.hyperreal analysis.normed.group.basic tactic
open filter function
namespace filter.germ

section examples
local notation `𝓗` := hyperfilter ℕ

noncomputable def omega' {α : Type*} [ordered_semiring α] :
  (𝓗 : filter ℕ).germ α := ↑(coe : ℕ → α)

local notation `ω` := omega'

open_locale topological_space
open hyperreal

lemma abs_eq_map_abs : (abs : ℝ* → ℝ*) = germ.map abs :=
begin
   ext x,
   rw [abs_eq_max_neg, max_def],
   refine x.induction_on (λ f, _),
   refl
end

lemma goal (u : ℕ → ℝ) (l : ℝ) (h : tendsto u at_top (𝓝 l)) : is_st (germ.map u ω) l :=
begin
  rw metric.tendsto_at_top at h,
  intros ε hε,
  rcases h ε hε with ⟨N, hN⟩,
  simp_rw [dist_eq_norm, real.norm_eq_abs] at hN,
  have : (∀ n : ℕ, n ≥ N → abs (u n - l) < ε) ↔
    (∀ n : (𝓗 : filter ℕ).germ ℕ, n ≥ ↑N → germ.map abs (germ.map u n - ↑l) < ↑ε),
  sorry,
  rw this at hN,
  clear this,
  specialize hN ω (begin
    change (↑N ≤ ω),
    simp [le_def],
    apply mem_hyperfilter_of_finite_compl,
    simp,
    have : {x | N ≤ x}ᶜ = {x | x < N}, by { ext, simp },
    rw this,
    exact set.finite_lt_nat N,
  end),
  rw ← abs_eq_map_abs at hN,
  rw abs_lt at hN,
  cases hN with hN₁ hN₂,
  split,
  change ↑l - ↑ε < germ.map u ω, linarith,
  change germ.map u ω < ↑l + ↑ε, linarith,
end

end examples
end filter.germ

Now I've solved the problem. This is one part of @Anatole Dedecker 's code and I've just filled in two sorrys. (now the sorry part can be solved by transfer, but it needs more files, so I just write sorry to quote the code). The changes in the final lines seem very stupid :joy:...

[Mario Carneiro]

Jiatong Yang said:

Why does linarith not work on hyperreals?

That sounds like a bit of scope creep... Are the hyperreals actually amenable to linarith?

[Anatole Dedecker]

Mario Carneiro said:

Jiatong Yang said:

Why does linarith not work on hyperreals?

That sounds like a bit of scope creep... Are the hyperreals actually amenable to linarith?

We do have docs#filter.germ.linear_ordered_comm_ring, if that answers the question

[Anatole Dedecker]

Jiatong Yang said:

[...]
Now I've solved the problem. This is one part of Anatole Dedecker 's code and I've just filled in two sorrys. (now the sorry part can be solved by transfer, but it needs more files, so I just write sorry to quote the code). The changes in the final lines seem very stupid :joy:...

Nice! Now I feel bad for leaving my code in such a bad state, I didn't think anyone would want to use it :sweat_smile: I don't have a lot of time to work on that, but at least I'll try to add comments to pass it to you properly. Also, note that transfer is the first and only tactic I ever wrote in Lean3, so it's probably terribly unoptimal

[Jiatong Yang]

Thanks a lot! I have written no tactics before, so I need to learn tactic writing first :grinning: