## Stream: maths

### Topic: with_bot

#### orlando (May 07 2020 at 18:33):

Hello,
I'm reading a little the theory of degree in data.polynomial and there is a strange object :  with_bot \N :sweat_smile:

Do you have an idea to deal with bot ? For example !

import order
open with_bot
example  (a b : with_bot ℕ  ) : a ≤ b → a+1 ≤ b+1 := begin
intros,
end


#### Mario Carneiro (May 07 2020 at 18:43):

what is bot+1 supposed to be in this statement?

#### Mario Carneiro (May 07 2020 at 18:43):

That's true as long as you are talking about nats, and nats embed in with_bot nat

#### orlando (May 07 2020 at 19:02):

Hello Mario,

For me bot + 1 = bot  so i each case it ok !
But i don't understand who to deal in lean ? Is there is a file where this arithmetic property are state ?

#### Kevin Buzzard (May 07 2020 at 19:06):

Just do cases on a and b?

#### orlando (May 07 2020 at 19:20):

Yep i can cases ... but but but :sweat_smile:

example  (a b : with_bot ℕ  ) : a ≤ b → a+1 ≤ b+1 := begin
rcases  b, intros, rcases a, exact le_refl (none +1),
rw none_eq_bot  at *, rw some_eq_coe at *,rw  le_bot_iff at a_1,
rw a_1, refine le_refl _,
rcases a, rw none_eq_bot  at *, rw some_eq_coe at *,
intros, exact bot_le, rcases a, intros,
rw some_eq_coe at *, erw zero_add,
not finish


#### Johan Commelin (May 07 2020 at 19:21):

@orlando Note that there is also nat_degree.

#### Johan Commelin (May 07 2020 at 19:21):

They are the same, except for the zero polynomial

#### orlando (May 07 2020 at 19:24):

Yep Johan, but a try to use the theorem : in $\C$ all polynomial of 0 < degree  have roots ... and i have to deal i little with  degree :confused:

#### orlando (May 07 2020 at 19:44):

I little better

example  (a b : with_bot ℕ  ) : a ≤ b → a+1 ≤ b+1 := begin
intros,
rcases  b, intros, rcases a,
exact le_refl (none +1),
erw  le_bot_iff at a_1, rw a_1,
refine le_refl _,
rcases a,
exact bot_le,
apply some_le_some.mp a_1, exact le_refl 1,
end


#### Johan Commelin (May 07 2020 at 19:44):

@orlando There is a lemma degree_eq_nat_degree, which is probably useful

#### Johan Commelin (May 07 2020 at 19:45):

Of course it comes with the assumption that the polynomial is not zero

#### orlando (May 07 2020 at 19:54):

perhaps it help me ! I'm trying to make caracteristic polynomial of a matrix. And i have to proof that the degree of the polynomial is equal to the dimension of the matrix.

#### Reid Barton (May 07 2020 at 20:05):

where is this + even defined?

#### Kevin Buzzard (May 07 2020 at 20:06):

instance [add_semigroup α] : add_semigroup (with_bot α) := with_top.add_semigroup


#### Kevin Buzzard (May 07 2020 at 20:06):

instance [add_semigroup α] : add_semigroup (with_top α) :=
{ add := λ o₁ o₂, o₁.bind (λ a, o₂.map (λ b, a + b)),
..@additive.add_semigroup _ $@with_zero.semigroup (multiplicative α) _ }  I blame Mario #### Kevin Buzzard (May 07 2020 at 20:07): I can't find some x + some y = some (x+y) #### Kevin Buzzard (May 07 2020 at 20:07): norm_cast won't do it #### Kevin Buzzard (May 07 2020 at 20:08): import data.polynomial open with_bot #check with_bot.add_semigroup example (a b : with_bot ℕ ) : a ≤ b → a+1 ≤ b+1 := begin intro hab, cases a with a; cases b with b, { refine le_refl _}, { rw none_eq_bot, rw bot_add, refine bot_le}, { exfalso, rw none_eq_bot at hab, rw le_bot_iff at hab, cases hab}, { rw some_le_some at hab, show (a : with_bot ℕ) + (1 : ℕ) ≤ b + (1 : ℕ), sorry }, end  Everything else is easy #### Reid Barton (May 07 2020 at 20:10): Kevin Buzzard said: instance [add_semigroup α] : add_semigroup (with_bot α) := with_top.add_semigroup  okay thanks, then the proof is add_le_add_right'. #### Kevin Buzzard (May 07 2020 at 20:10): @orlando because you don't format your code properly it's difficult for other people to read. You should use {} instead of having multiple goals open at once #### Reid Barton (May 07 2020 at 20:10): I don't know why apply can't apply this or why library_search can't find it though. #### Kevin Buzzard (May 07 2020 at 20:13): Orlando is doing induction on a but the issue isn't going to go away: the other goal is b a : ℕ ⊢ some (nat.succ a) ≤ some b → some (nat.succ a) + 1 ≤ some b + 1  It all hinges on some being a monoid hom. #### Reid Barton (May 07 2020 at 20:13): Reid Barton said: I don't know why apply can't apply this Aha, because le is cleverly implemented as a forall/function. #### Kevin Buzzard (May 07 2020 at 20:13): aah, coe_add isn't tagged with one of these norm_cast tags. #### Reid Barton (May 07 2020 at 20:14): Why are you mucking around with casts and stuff? #### Kevin Buzzard (May 07 2020 at 20:14): because I couldn't find the algebraic class which with_bot nat was #### Reid Barton (May 07 2020 at 20:15): It's annoying how hard it is to find instances. #### Kevin Buzzard (May 07 2020 at 20:15): but you're right, it's an ordered_add_comm_monoid. #### Kenny Lau (May 07 2020 at 20:15): import order open with_bot example (a b : with_bot ℕ) (H : a ≤ b) : a + 1 ≤ b +1 := begin cases a with a, { exact bot_le }, { rcases H a rfl with ⟨n, ⟨⟩, han⟩, rintros m ⟨⟩, exact ⟨n+1, rfl, nat.succ_le_succ han⟩ } end  #### Reid Barton (May 07 2020 at 20:16): my proof is shorter than kenny's :hole_in_one: #### Kenny Lau (May 07 2020 at 20:16): oh #### Kevin Buzzard (May 07 2020 at 20:17): with_bot.coe_le : ∀ {α : Type ?} [_inst_1 : partial_order α] {a b : α} {o : option α}, b ∈ o → (↑a ≤ o ↔ a ≤ b)  gaargh #### Kevin Buzzard (May 07 2020 at 20:17): that's not what coe_le is supposed to say #### Kenny Lau (May 07 2020 at 20:18): proposition to make \le inductive #### Reid Barton (May 07 2020 at 20:19): Hopefully it goes better than when I tried to do that to continuous... #### orlando (May 07 2020 at 20:22): @Reid Barton ...  add_le_add_right'  :+1: :+1: :+1: #### Kevin Buzzard (May 07 2020 at 20:22): The trick is to realise that it's an ordered_add_comm_monoid #### orlando (May 07 2020 at 20:23): Yep Kevin ! That give property ! That good ! #### Kevin Buzzard (May 07 2020 at 20:33): I see. So somehow the correct way to proceed would have been to say to Lean "hey Lean, give me the complete list of instances on with_bot nat because I can't remember the axioms for half of them and so don't actually know if it's an ordered semigroup or even if Lean has ordered semigroups" #### Reid Barton (May 07 2020 at 20:34): Well, ideally library_search would have simply worked but probably it ran into the apply bug #### Reid Barton (May 07 2020 at 20:34): But otherwise, yes that would be nice to have. #### orlando (May 07 2020 at 20:37):  libraty_search  and suggest  are nice tactic !!! #### Kevin Buzzard (May 07 2020 at 20:39): "and then tell me all the lemmas which apply to that object". I see. That's what library_searchis supposed to do? #### orlando (May 07 2020 at 20:42): In 10 years lean will work on his own, we will just have to watch him prove theorems :grinning_face_with_smiling_eyes: #### Mario Carneiro (May 07 2020 at 21:52): Kevin Buzzard said: I see. So somehow the correct way to proceed would have been to say to Lean "hey Lean, give me the complete list of instances on with_bot nat because I can't remember the axioms for half of them and so don't actually know if it's an ordered semigroup or even if Lean has ordered semigroups" namespace tactic meta def env_fold {α} (a : α) (f : declaration → α → tactic α) : tactic α := get_env >>= λ e s, e.fold ((return a : tactic _) s)$ λ d t,

meta def get_all_classes : tactic (list name) :=
list.reverse <$> env_fold [] (λ d l, mcond (is_class (expr.const d.to_name (level.param <$> d.univ_params)))
(return (d.to_name :: l)) (return l))

meta def list_instances (e : expr) : tactic (list expr) :=
get_all_classes >>= list.mfoldr (λ n l,
(do e' ← mk_app n [e],
mk_instance e' >> return (e' :: l)) <|>
return l) [] .

open interactive interactive.types
meta def interactive.list_instances (e : parse texpr) : tactic unit :=
to_expr e >>= list_instances >>= list.mmap' trace

run_cmd list_instances (ℕ) >>= trace

example : true := by {list_instances ℕ, trivial}

end tactic


#### Mario Carneiro (May 07 2020 at 21:52):

add_semigroup ℕ
has_sub ℕ
inhabited ℕ
has_well_founded ℕ
semigroup ℕ
has_lt ℕ
has_to_tactic_format ℕ
has_to_format ℕ
has_one ℕ
monoid ℕ
preorder ℕ
has_zero ℕ
has_mod ℕ
comm_semigroup ℕ
zero_ne_one_class ℕ
has_sizeof ℕ
reflected ℕ
has_le ℕ
has_repr ℕ
comm_monoid ℕ
nonempty ℕ
linear_order ℕ
distrib ℕ
has_to_string ℕ
ordered_semiring ℕ
decidable_linear_order ℕ
mul_zero_class ℕ
has_dvd ℕ
semiring ℕ
has_mul ℕ
has_div ℕ
decidable_linear_ordered_semiring ℕ
linear_ordered_semiring ℕ
comm_semiring ℕ
partial_order ℕ


#### Mario Carneiro (May 07 2020 at 21:55):

example : true := by {list_instances (with_bot ℕ), trivial}
-- inhabited (with_bot ℕ)
-- semilattice_sup_bot (with_bot ℕ)
-- has_well_founded (with_bot ℕ)
-- has_lt (with_bot ℕ)
-- has_to_tactic_format (with_bot ℕ)
-- lattice (with_bot ℕ)
-- has_sup (with_bot ℕ)
-- has_to_format (with_bot ℕ)
-- has_one (with_bot ℕ)
-- distrib_lattice (with_bot ℕ)
-- preorder (with_bot ℕ)
-- has_zero (with_bot ℕ)
-- has_bot (with_bot ℕ)
-- has_sizeof (with_bot ℕ)
-- semilattice_inf (with_bot ℕ)
-- reflected (with_bot ℕ)
-- has_le (with_bot ℕ)
-- nonempty (with_bot ℕ)
-- linear_order (with_bot ℕ)
-- decidable_linear_order (with_bot ℕ)
-- semilattice_inf_bot (with_bot ℕ)
-- semilattice_sup (with_bot ℕ)
-- has_inf (with_bot ℕ)
-- order_bot (with_bot ℕ)
-- partial_order (with_bot ℕ)


#### Kevin Buzzard (May 07 2020 at 22:54):

Oh this was the thing that was called ordered_comm_monoid which confused the perfectoid project? How come there's no ordered_monoid?

#### Johan Commelin (May 08 2020 at 03:48):

@Kevin Buzzard In mathlib/core what used to be called an ordered_monoid is now called ordered_add_monoid. Once norm_num is out of core, we can refactor everything and also have (multiplicative) ordered_monoids.
Of course we could have them now, but not with all the nice to_additive machinery. That's why the norm_num PR is important.

#### Johan Commelin (May 08 2020 at 03:51):

Reid Barton said:

It's annoying how hard it is to find instances.

With the new widget stuff by @Edward Ayers this will hopefully be a lot easier soon. It's really ironic that the goal window has all this information (in principle), but is only showing us a really nice pp version. And if you ask for the raw stuff, that's what you get. A brutal flood of :poop: (-;

Anyway, in the mean time: what about a command #find_instance that just like #simp uses variables that have been declared in the context, so that you can do things like

#find_instance : add_comm_monoid (with_bot nat)

variables (X Y : Type) [fintype X] [fintype Y]

#find_instance : fintype (X → Y)


etc...

#### orlando (May 08 2020 at 23:05):

Hello, just to understand the mecanism of coersion. Is there is a quick way to do that ?

lemma cast_bot'   (a  : ℕ ) :  nat.cast (a) = ( a: with_bot ℕ ) :=   ???


#### Chris Hughes (May 08 2020 at 23:24):

If you had used the notation for nat.cast I think simp would solve it. Otherwise, I think it would have to be done by induction on a if it isn't in the library.

#### Chris Hughes (May 08 2020 at 23:26):

There's two coercion from nat to with_bot nat, and you should usually just use the higher priority with_bot coercion. Most of the necessary lemmas are in the with_bot namespace.

#### orlando (May 09 2020 at 00:04):

Ok for the two coersion, so the definition is  with_bot not nat.cast  ! Thx !

#### Kevin Buzzard (May 09 2020 at 07:16):

I think the trick is to find out which one is used in the library and then to always use that one, and to always use it in the exact syntactic form which is in the library, because if you don't then simp will not work

#### orlando (May 09 2020 at 07:37):

@Kevin Buzzard : In theory, i understand ! But i practice i have some difficulty for example at the last proof i can't finish the proof without a conversion  int.cast vs bot_cast .

The tactic state before  cast_with_bot  is

1 goal
R : Type u,
_inst_1 : nonzero_comm_ring R,
A : Type v,
_inst_2 : fintype A,
_inst_3 : decidable_eq A,
s : finset A,
φ : A → polynomial R,
hyp : ∀ (ℓ : A), degree (φ ℓ) = 1,
hyp_lc : ∀ (ℓ : A), monic (φ ℓ),
⊢ ↑(card s) = ↑(card s)   ----- AHHAHAHAHAHAHAHAH  :upside_down:

import data.polynomial
open finset polynomial with_bot
universes u v
variables
{R : Type u}[nonzero_comm_ring R]
{A : Type v} [fintype A][decidable_eq A]
lemma prod_monic (s : finset A)(φ : A → polynomial R)  (hyp : ∀ a : A, monic (φ a)) :
monic (finset.prod s  (λ x : A, φ x))  :=
begin
apply (finset.induction_on s), {
erw prod_empty at  *,
},
{
intros ℓ  s hyp' hyp_rec,
rw finset.prod_insert (by assumption),
exact monic_mul (hyp ℓ)  hyp_rec,
},
end
lemma degree_prod_monic (s : finset A)(φ : A → polynomial R)
(hyp_lc : ∀ ℓ : A, monic (φ ℓ )) :
degree (finset.prod s  (λ x : A, φ x)) =  finset.sum s ( λ x : A, degree (φ x)) :=
begin
apply (finset.induction_on s), {
rw prod_empty,
exact degree_C (one_ne_zero),
},
{
intros ℓ  s hyp' hyp_rec,
rw finset.prod_insert (by assumption),
rw finset.sum_insert (by assumption),
rw ← hyp_rec,
apply degree_mul_eq',
conv_lhs {
rw  monic.def.mp (hyp_lc ℓ), rw one_mul,
rw  monic.def.mp (prod_monic s φ hyp_lc),
},
exact one_ne_zero,
},
end

theorem cast_with_bot   (a  : ℕ ) :  nat.cast (a) = (a: with_bot ℕ ) := begin
apply (nat.rec_on a),  {
exact rfl,
},
intros ℓ  hyp_rec,
change _ = ↑ℓ + ↑1,
erw ← hyp_rec, exact rfl,
end
lemma coeff_prod_nat'  (s : finset A)(φ : A → polynomial R)(hyp : ∀ ℓ : A, degree(φ ℓ ) = 1 )
(hyp_lc : ∀ ℓ : A, monic(φ ℓ) ) :   -- monic !
degree (finset.prod s  (λ x : A, φ x)) =  card s :=
begin
rw degree_prod_monic s φ  hyp_lc,
conv_lhs{
apply_congr, skip,
rw hyp x,
},
---- here i have to use nat.cast = with_bot coe  HERE
refine cast_with_bot  _ ,
end


#### Kevin Buzzard (May 09 2020 at 07:40):

Maybe sometimes it is unavoidable?

#### Kevin Buzzard (May 09 2020 at 07:41):

Maybe there is a missing simp lemma though?

#### Kevin Buzzard (May 09 2020 at 07:42):

I am not an expert in simp but maybe one should expect norm_cast to solve this. Unfortunately I just regard norm_cast as magic

#### orlando (May 09 2020 at 07:43):

i try all the  simp hint library_search and suggest  before understanding that the first coersion is nat.cast and the second bot_cast 

#### Kevin Buzzard (May 09 2020 at 07:43):

So I don't know whether norm_cast should be taught to solve this or whether it is not its job

#### orlando (May 09 2020 at 07:43):

 hint  give me a commandunfold_coes  :grinning_face_with_smiling_eyes:

#### Mario Carneiro (May 09 2020 at 07:43):

there should be a theorem that says they are the same

#### Kevin Buzzard (May 09 2020 at 07:44):

But should the user be required to know its name?

#### Mario Carneiro (May 09 2020 at 07:44):

first the theorem, then the fancy

#### Kevin Buzzard (May 09 2020 at 07:44):

Because I am always confused about whether it's cast or coe, and which namespace it's in

#### Mario Carneiro (May 09 2020 at 07:44):

are we sure the theorem even exists?

#### Mario Carneiro (May 09 2020 at 07:45):

because if it doesn't I won't expect the tactics to find the proof

#### Kevin Buzzard (May 09 2020 at 07:45):

I don't know enough about simp to know how to even state the lemma

#### Mario Carneiro (May 09 2020 at 07:46):

I don't know exactly what the lemma is here, something about with_bot?

#### orlando (May 09 2020 at 07:46):

i don't see  nat.coe = bot_coe  theorem in mathlib

#### Mario Carneiro (May 09 2020 at 07:47):

does that even typecheck?

#### Kevin Buzzard (May 09 2020 at 07:47):

This is all part of the CS machinery which I don't have much of an understanding of. I am not even 100% sure that norm_cast should do it, but I guess that would be my instinct

#### Mario Carneiro (May 09 2020 at 07:47):

what are the types

#### Kevin Buzzard (May 09 2020 at 07:47):

And I wouldn't know how to make it do it if it didn't

#### Mario Carneiro (May 09 2020 at 07:47):

there is a mathematical part of this to be dealt with before the tactics can take over

#### orlando (May 09 2020 at 07:48):

This is ok

theorem cast_with_bot   (a  : ℕ ) :  nat.cast (a) = (a: with_bot ℕ ) := begin
apply (nat.rec_on a),  {
exact rfl,
},
intros ℓ  hyp_rec,
change _ = ↑ℓ + ↑1,
erw ← hyp_rec, exact rfl,
end


#### Mario Carneiro (May 09 2020 at 07:48):

just over nat though?

#2636

#### Mario Carneiro (May 09 2020 at 08:18):

It's apparently not eligible for any kind of *_cast tactic, but it can be a simp lemma

#### orlando (May 09 2020 at 18:07):

Youppi : i finish the first part of caracteristic polynomial :grinning_face_with_smiling_eyes:

 theorem  (hyp : 0 < fintype.card A  ):  ∀ M : matrix A A ℂ ,  ∃ t : ℂ, det ( M + t •(1 : matrix A A ℂ )) = 0


Congratulations!

#### Johan Commelin (May 09 2020 at 18:08):

So now we know that eigenvalues exist (-;

#### Johan Commelin (May 09 2020 at 18:09):

What is the determinant of a 0x0 matrix?

I guess it's 1

#### Kenny Lau (May 09 2020 at 18:10):

Johan Commelin said:

So now we know that eigenvalues exist (-;

we don't know that C is alg. closed

We do

#### Johan Commelin (May 09 2020 at 18:10):

Chris did that ages ago

#### Kenny Lau (May 09 2020 at 18:10):

Johan Commelin said:

I guess it's 1

yes

#### Kenny Lau (May 09 2020 at 18:11):

Johan Commelin said:

Chris did that ages ago

wait what

#### Johan Commelin (May 09 2020 at 18:11):

We don't have algebraic closures, but we do know what an algebraically closed field is

#### orlando (May 09 2020 at 18:11):

@Johan Commelin hum : it's a sum over the permutation of empty set ... so a sum with one term ! so it's one i think !

#### Johan Commelin (May 09 2020 at 18:11):

Maybe we don't have a type class [algebraically_closed K], but we have FTA

#### Johan Commelin (May 09 2020 at 18:12):

@orlando Does your proof work for arbitrary alg closed fields?

#### Johan Commelin (May 09 2020 at 18:12):

If so, we quickly need to add that typeclass

#### orlando (May 09 2020 at 18:13):

The theorem FTA i s in the file : The theorem is in the file  analysis.complex.polynomial 

#### orlando (May 09 2020 at 18:14):

Yes a think it's ok for all algebraicly closed field

#### Kenny Lau (May 09 2020 at 18:14):

what was the proof?

Of what?

#### Johan Commelin (May 09 2020 at 18:14):

@orlando Are you planning to PR this?

of FTA

#### Johan Commelin (May 09 2020 at 18:15):

@Chris Hughes :up:

#### Bhavik Mehta (May 09 2020 at 18:16):

Congratulations!!

#### orlando (May 09 2020 at 18:17):

@Johan Commelin : i have to simplify ! It's very complicated with the sum and the product of the determinant.

Thx @Bhavik Mehta :grinning:

#### Chris Hughes (May 09 2020 at 18:17):

I think there's even a link to the proof I used in the file. I did it well over a year ago.

#### Kenny Lau (May 09 2020 at 18:17):

aha, you proof the open mapping theorem specifically for polynomials

#### Kenny Lau (May 09 2020 at 18:18):

which does not require complex analysis

#### Kenny Lau (May 09 2020 at 18:18):

therefore the minimum (which exists by O analysis) must be 0

#### Johan Commelin (May 09 2020 at 18:22):

@orlando I strongly encourage you to PR this

#### Johan Commelin (May 09 2020 at 18:25):

theorem jenesaispas, nice (-;
It will need some cleaning up and unfrenchyfying :rofl:

#### Mario Carneiro (May 09 2020 at 18:34):

Shouldn't that be theorem je_ne_sais_pas`?

#### Johan Commelin (May 09 2020 at 18:35):

Je ne sais pas...

#### orlando (May 09 2020 at 18:39):

I have no idea of name at the end :joy:

#### Patrick Massot (May 09 2020 at 20:28):

Johan Commelin said:

So now we know that eigenvalues exist (-;

Isn't it sad to use determinants for that?

#### Patrick Massot (May 09 2020 at 20:29):

Congratulations to Orlando anway!

#### Patrick Massot (May 09 2020 at 20:30):

Now you can start a very important part of your initiation to Lean. Turning this mess into a merged mathlib PR will teach you at least as much Lean as what you learned up to now.

#### Bhavik Mehta (May 09 2020 at 20:45):

Patrick Massot said:

Now you can start a very important part of your initiation to Lean. Turning this mess into a merged mathlib PR will teach you at least as much Lean as what you learned up to now.

I couldn't agree with this more!

#### orlando (May 09 2020 at 21:13):

@Patrick Massot : There is a long way to go to understand lean and mathlib. I have been using lean for two months and even if I have made progress, I am not really comfortable with it! Always a feeling of not understanding how it works. But that fun and i have time :grinning_face_with_smiling_eyes:

#### Kevin Buzzard (May 09 2020 at 22:06):

My first PR was the complex numbers and it got changed a huge amount before it was accepted. It's a very interesting experience!

Last updated: May 06 2021 at 17:38 UTC