building reals with quasi-morphisms

Stream: new members

[yannis monbru]

Hello, i am a french student in mathematics and for fun (and in order to practice) i am trying to build the real numbers with the quasi-morphisme construction.

[Scott Morrison]

See docs#finset.max and docs#finset.max'.

[Scott Morrison]

Can you post a #mwe showing what you're trying to do to import, and explain the file layout?

[yannis monbru]

thank you for the link

I just created a second file in the directory "src" and wrote " import [name of my first file]" wich didn't work and i see that lean is not aware of what i wrote on the other file

the begining of the file is that:
/-
import data.int.basic
import tactic.linarith

def q_morph (f:ℤ→ ℤ) := ∃ (M :ℤ) , ∀ n m, (- M≤ f n + f m - f (n+m))∧(f n + f m - f (n+m)≤ M)

def QM: set _ :={f:ℤ→ℤ | q_morph f }

def egal (f:ℤ → ℤ ) (g:ℤ→ℤ):= q_morph (f - g) -/

and then there are lemmas to prove that things behave like we would expect

[Patrick Massot]

For the quotient question, you can start with

import tactic

structure quasi_mph :=
(to_fun : ℤ → ℤ)
(bound : ℤ)
(map_mul' : ∀ x y, abs(to_fun (x*y) - to_fun x - to_fun y) ≤ bound)

namespace quasi_mph

instance : has_coe_to_fun quasi_mph := ⟨_, λ q, q.to_fun⟩

-- Let's restate the `map_mul' axiom in term of the coercion to function

lemma map_mul (q : quasi_mph) (x y : ℤ) : abs (q (x*y) - q x - q y) ≤ q.bound :=
q.map_mul' x y

instance : setoid quasi_mph :=
{ r := sorry,
  iseqv := ⟨sorry, sorry, sorry⟩ }

end quasi_mph

def euxodus_real := quotient quasi_mph.setoid

variable q : quasi_mph

#check (⟦q⟧ : euxodus_real)

[Patrick Massot]

You also need to read #backticks

[Scott Morrison]

Do you have a leanpkg.toml? Did you open a file in VSCode, or the whole folder?

[Scott Morrison]

(You need one, and you need to open the folder containing src.)

[Patrick Massot]

About the file layout, we need to know what is the src folder you're talking about

[Patrick Massot]

Did you create a project using leanproject new?

[Patrick Massot]

yannis.gif

[Patrick Massot]

Do not mind the leanproject bug that says it's looking for yannis olean instead of mathlib oleans

[yannis monbru]

i thought i did like that, but after redoing it like on your video, it now works. So i don't understand what hapened but the issue is now gone...

thank you very much

[Patrick Massot]

Also make sure to read https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients if you haven't read it yet.

[Yaël Dillies]

Also note that this construction has already been done if you need inspiration, although I can't find it anymore :confused:

[yannis monbru]

i saw on wikipedia that it has been done by the projet IsarMathLib, but is it in Lean?

[Yaël Dillies]

I remember so... but I might be mistaken. Can anyone else infirm/confirm?

[Alex J. Best]

There was https://github.com/Lix0120/eudoxus which seems pretty similar, though I don't know if they are exactly the same?

[Yaël Dillies]

That's what I was thinking about! This is exactly the same.

[yannis monbru]

hello, i have a question about lifting maps to with two agruments to the quotient

is there a way to lift to arguments at the same time or do we need to lift in one argument and then in the other?

[Alex J. Best]

Is https://leanprover-community.github.io/mathlib_docs/data/quot.html#quot.lift%E2%82%82 what you want?

[yannis monbru]

yes it is exactly that thank you

[yannis monbru]

Hello, is there a way to extract from a term "\exists M,....." a value of M in the same way that we exctrat a proof of A from a proof of "A and B".

I am trying to define a new term of a structure and i need to give to lean a value of M and a proof that this M satisfy some conditions, but the actual value of M is dificult to know so i can't give it just by writing it's value.

On the other hand i tryed to define my term between 'begin' and 'end' in order to be able to use rcase (\exists M,...) but it seems not to work.

thank you for your help

[Eric Wieser]

On the other hand i tryed to define my term between 'begin' and 'end' in order to be able to use rcase (\exists M,...) but it seems not to work.

can you show your code?

[Riccardo Brasca]

Do you mean obtain ⟨x, hx⟩ := h, where h : ∃ x,...?

[yannis monbru]

def c_qm (f:quasi_mph) (g:quasi_mph): quasi_mph:=
begin
  rcases stab_c f g with ⟨M,hM⟩,

end

and the interpretor says nduction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop

[Yaël Dillies]

You almost got #backticks right :smile: Put them on their own line.

[Yaël Dillies]

That's because you can't get data out of an existential to define data (without the axiom of choice). You can only get data of an existential to prove a proposition.

[Yaël Dillies]

(Those are backticks: `` Those are not '')

[Yaël Dillies]

If you're French, the backticks are actually loose accents graves. You can find them on the key for 7.

[Yaël Dillies]

Ah! You found them.

[yannis monbru]

thank you for the tips

is there a way to cheat, knowing that the value have an expression completly constructive?

[Yaël Dillies]

The solution here is to either use docs#classical.some and docs#classical.some_spec, or not hiding your data inside an existential in the first place.

[Yaël Dillies]

Yeah so in your case you want to define a function.

[yannis monbru]

ok i will try to find an explicit value, than you

[yannis monbru]

hello, i have a lot of calculation involving involving integer + and - (like x-y= x- z+ -y+z) to prove to lean and the tacting ring (or ring_nf) seems to have problem with this kind of example, is there another tactic better suited for that job ?

thank you

[Anupam Nayak]

linarith

[Anupam Nayak]

https://leanprover-community.github.io/mathlib_docs/tactic/linarith/frontend.html

[Patrick Massot]

Do you really mean integer here? Do you have an example?

[Patrick Massot]

ring has no trouble doing example (x y z : ℤ) : x - y = x - z + -y + z := by ring (that would be a huge bug noticed a long time ago)

[yannis monbru]

no it is somme elements that have the type int but they are of the form f ( g(n)+g(m)) for example
i have an example but i am not shure it is realy readable

[Patrick Massot]

#mwe

[Patrick Massot]

We can't help you without a mwe

[yannis monbru]

calc |f (g (n + m)) - f (g n + g m)| = |(f((g(n + m)) - f (g (n + m)-(g n+g m))- f (g n + g m))+(f (g (n + m)-g n-g m))|: by {ring,}

to better read it it is of the form |x-y|=|x-z-y+z|

[Kevin Buzzard]

This is not a #mwe -- what is the definition of |? Maybe ring can't see inside it. You could apply congr_fun first maybe? What are the domain and codomain of f, g etc? If you give us code which we can just cut and paste and which works (the point of a mwe) we can help.

[Kevin Buzzard]

Otherwise we have to start guessing, and this wastes people's time

[Kevin Buzzard]

import tactic

-- some guessing
example (f : ℤ → ℤ) (a b c : ℤ) : f (a + b) + f c = f c + f (b + a) :=
begin
  ring_nf,
  ring,
end

[yannis monbru]

sorry about that,

import tactic
variables f:ℤ→ ℤ
variables g:ℤ→ℤ


lemma ineg:∀ n m, |f (g (n + m))-f (g n +g m)|<= 42:=
begin
  intros n m,
    calc |f (g (n + m)) - f (g n + g m)| = |f ((g (n + m)) - f (g (n + m)-(g n+g m))- f (g n + g m))+(f (g (n + m)-g n-g m))|: by {

      ring_nf,
    }
    ...≤ 42: by sorry,

end

[Yaël Dillies]

This doesn't solve your question but the correct thing to use here is docs#abs_sub_le.

[yannis monbru]

thank you for that

[Patrick Massot]

This code is not correct

[Patrick Massot]

It has errors having nothing to do with ring

[Patrick Massot]

Presumably parentheses are messed up

[yannis monbru]

yes i wrongly ad a ( by making the example it is corected now

[Patrick Massot]

I'm pretty sure this is still not what you intended to write

[Patrick Massot]

Try additing the generalize lines to your code

lemma ineg:∀ n m, |f (g (n + m))-f (g n +g m)|<= 42:=
begin
  intros n m,
    calc |f (g (n + m)) - f (g n + g m)| = |f ((g (n + m)) - f (g (n + m)-(g n+g m))- f (g n + g m))+(f (g (n + m)-g n-g m))|: by {
     generalize : g(n+m) = x,
     generalize : g n = y,
     generalize : g m = z,

      ring_nf,
    }
    ...≤ 42: by sorry,

end

[yannis monbru]

yes indeed , i will think again on my example an see if did a mistake by wrinting my code (realy sorry if it is the case)

[Patrick Massot]

Still, ring can't guess what to do inside function applications. I'm not sure you can do much better than

lemma ineg:∀ n m, |f (g (n + m))-f (g n +g m)|<= 42:=
begin
  intros n m,
  calc |f (g (n + m)) - f (g n + g m)| = |f (g (n + m)) - f (g (n + m)-(g n+g m))-
                                          f (g n + g m)+(f (g (n + m)-g n-g m))| : by {
    rw show ∀ x y z : ℤ, x - (y + z) = x - y - z, by { intros, ring },
    congr,
    ring,
  }
  ...≤ 42: sorry,
end

[Patrick Massot]

Do you know you can use the widgets to inspect the structure of a complicated term and make sure that it associates correctly?

[Patrick Massot]

Simply make sur the info view is wide (otherwise there are bugs) and put your mouse over subexpressions, paying attention to highlighting

[yannis monbru]

in fact the problem was that i had an other calculation inside a function and thought it was not a problem so i removed it in the example , and doing that i completly mixed up the '(' and now ring is okay

i will handle the inside as in your example

thank you very much

[yannis monbru]

hello, I am trying to lift a predicate "is positive" : r->Prop to a quotient of r but i think that in order to use the constructor like quot.lift i need an equivalence relation on Prop to express the fact that two elements of r that are equivalents are positive at the same time but i don't know what it could be.
but maybe there is a direct construction for this type of lifting, could you give me a solution

thank you for your help

[Reid Barton]

In order to get a predicate on the quotient you need to know that if x and y are related then the propositions is_positive x and is_positive y are equal--but because of docs#propext that's the same as saying that they are equivalent (related by iff).

[yannis monbru]

ok thank you very much

[yannis monbru]

Hello, i have a formalisation of a commutavive ring , (in fact i have fonctions add:R->R->R, ....., and proof of the axioms of a comutative ring) and i have some statement to prove that need calculations with the ring structure. Is there a way to handle these calculations with some features of ring ?

thank you for your help

[Alex J. Best]

There are tactics for calculations in rings such as tactic#ring and tactic#noncomm_ring, do those help?

[Patrick Massot]

This question is too vague, we can't help you. You should try to provide #mwe or a link to a Lean project hosted on GitHub if building a mwe is too complicated.

[yannis monbru]

yes i found the answer by reading this, i need to say to lean that i have a ring and not stay with a list of statement.
thank you very much