More elegant way?

Stream: new members

[Walter Moreira]

What could be a more elegant way to solve this? It looks like too many steps:

import data.real.basic

example : 1 = ((1 + real.sqrt 5) / 2 - (1 - real.sqrt 5) / 2) / real.sqrt 5 :=
begin
ring,
refine (inv_mul_cancel _).symm,
intro,
linarith [(real.sqrt_eq_zero (by linarith)).mp a],
end

[Jalex Stark]

you're missing import tactic to make this a #mwe

[Jalex Stark]

import data.real.basic
import tactic

example : 1 = ((1 + real.sqrt 5) / 2 - (1 - real.sqrt 5) / 2) / real.sqrt 5 :=
begin
  ring,
  refine (inv_mul_cancel _).symm, norm_num,
end

[Jalex Stark]

norm_num is the first thing i hit up when i want to prove something is not 0

[Walter Moreira]

Oh so sorry! How does it work for me?

[Jalex Stark]

uh, I assume you're running this codeblock inside of a file that already imported tactic?

[Jalex Stark]

oh, nevermind, I just had one of those "lean spits out a temporary error before it finishes compiling". I guess data.real.basic imports tactic?

[Johan Commelin]

Yup, certainly

[Walter Moreira]

No, it's just it's own file [Screen-Shot-2020-06-04-at-10.51.51-AM.png]
(https://leanprover.zulipchat.com/user_uploads/3121/gsrQOXPpBtrhTLj9BVx3OMdt/Screen-Shot-2020-06-04-at-10.51.51-AM.png)

[Walter Moreira]

@Jalex Stark Ah cool. Thanks for the norm_num hint.

[Jalex Stark]

it's working for me now, too. the problem was on my end.

[Jalex Stark]

you can just use rw instead of refine

import data.real.basic

example : 1 = ((1 + real.sqrt 5) / 2 - (1 - real.sqrt 5) / 2) / real.sqrt 5 :=
begin
  ring, rw inv_mul_cancel, norm_num,
end

[Jalex Stark]

rw is usually how iff statements are meant to be used

[Walter Moreira]

Very nice!

[Patrick Massot]

I see norm_num still has a lot to improve...

[Jalex Stark]

? do you want norm_num to be able to do everything ring can?

[Patrick Massot]

norm_num should close this goal without any help.

[Johan Commelin]

We can improve norm_num be writing the right simp lemmas

[Johan Commelin]

This might be related to Yury's recent question of making the field_simp simpset a subset of the normal simpset.

[Jalex Stark]

at some point it needs to know that it's supposed to prove a denominator is not equal to 0

[Jalex Stark]

field_simp doesn't do any denominator-clearing unless you pass it a proof that something is not 0

[Jalex Stark]

I think simp only [inv_mul_cancel]doesn't do anything here

[Johan Commelin]

That's true. Still... since there are no variables here, I think that in principle norm_num ought to be able to tackle this alone.

[Patrick Massot]

Yes, my point is that there is no variable.

[Jalex Stark]

I guess the first target is

example : (1:ℝ) = 2/2 := by norm_num

[Jalex Stark]

oh, norm_num does handle that, I should have tried it first...

[Jalex Stark]

but not

example : (1:ℝ) = (real.sqrt 5)/(real.sqrt 5):= sorry

[Jalex Stark]

should I raise an issue?

[Patrick Massot]

We can ask @Mario Carneiro first.

[Mario Carneiro]

What do you think norm_num is? It can't just evaluate arbitrary real number expressions. (That's undecidable, remember?)

[Johan Commelin]

But this one isn't arbitrary!

[Johan Commelin]

More seriously... can we add some special tags or lemmas that will teach norm_num to evaluate this

[Mario Carneiro]

Even though norm_num nominally works on real number expressions, that's only if they in fact describe rationals

[Alex J. Best]

Algebraic numbers are decidable right? (I actually don't know but they feel decidable!)

[Johan Commelin]

Galois theory says yes

[Mario Carneiro]

Algebraic numbers are decidable, yes. The algorithm is very complicated and I've never done it although I've looked at the proof

[Johan Commelin]

I guess you don't actually need galois theory for that

[Mario Carneiro]

something to do with permanents

[Alex J. Best]

You probably need some float approximation too?

[Mario Carneiro]

no

[Johan Commelin]

That might give a speed up, maybe?

[Alex J. Best]

Hmm interesting, I figured the operations would all be with the minimal polynomials, but then you need some approximation to distinguish roots occasionally

[Mario Carneiro]

Evaluating algebraic numbers is a component in CAD

[Alex J. Best]

http://fredrikj.net/calcium/index.html

[Mario Carneiro]

and that needs some approximation too

[Mario Carneiro]

You can express approximation problems as alg_1 < alg_2

[Alex J. Best]

His qqbar implementation uses some root finding, which is what put the idea in my head, its cool that its not needed!

[Mario Carneiro]

There are multiple ways to express algebraic numbers. A minimal polynomial is not enough because polynomials have several roots. You can number and order them but this still basically requires you to locate all the roots. One popular method is to put a box around the root you want that excludes all the others

[Mario Carneiro]

another trick (for real algebraics) is to use the sequence of signs of all the derivatives of the minimal polynomial at the target number. Perhaps surprisingly this determines which root uniquely

[Johan Commelin]

But square roots are easier, right

[Johan Commelin]

Human beings have no problem calculating with roots and powers

[Mario Carneiro]

They are acting more like simp though

[Johan Commelin]

So maybe quadratic_closure rat is tractible?

[Mario Carneiro]

I don't think this is an appropriate goal for norm_num

[Johan Commelin]

Yup... so we need some simp lemmas

[Mario Carneiro]

I know people love their kitchen sink tactics, but I really think I should take a stand and say that this is out of scope for norm_num. norm_num assumes that all evaluable expressions have a normal form that is a rational numeral. Here that is not the case

[Mario Carneiro]

It is really best if the tactic knows in advance what the normal form is. Currently we are using separate tactics for separate normal forms for separate decision procedures, e.g. ring vs abel vs norm_num

[Johan Commelin]

Ok, that's fine. Then we just need a new tactic.

[Kevin Buzzard]

How does field_simp fare?

[Mario Carneiro]

It should be possible to prove this with ring++

[Mario Carneiro]

field_simp should work if you pass it a sqrt positivity lemma and use norm_num as discharger

[Walter Moreira]

As a continuation of this question, I'm able to prove in one line that phi^2 - phi - 1 = 0, and deduce from there that phi^2 = phi + 1.

But when I try to prove directly that phi^2 = phi + 1 (last example) I cannot find a simple chain of rws to prove it. Am I missing some more powerful technique for this?

import data.real.basic

noncomputable theory

def phi : ℝ := ((1 + real.sqrt 5) / 2)

lemma phi_sol : phi^2 - phi - 1 = 0 :=
begin
unfold phi, ring, rw real.sqr_sqrt; norm_num,
end

example : phi^2 = phi + 1 :=
begin
rw [←sub_eq_zero, sub_add_eq_sub_sub, phi_sol],
end

example : phi^2 = phi + 1 :=
begin
unfold phi,
sorry
end

[Patrick Massot]

I think this is again a trivial case of the missing Grobner basis tactic.

[Patrick Massot]

Here you can apply eq_of_sub_eq_zero then rw and ring