with_bot

Stream: maths

[orlando]

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]

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

[Mario Carneiro]

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

[orlando]

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]

Just do cases on a and b?

[orlando]

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]

@orlando Note that there is also nat_degree.

[Johan Commelin]

They are the same, except for the zero polynomial

[orlando]

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]

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.mpr, apply add_le_add,
    apply some_le_some.mp a_1, exact le_refl 1,
end

[Johan Commelin]

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

[Johan Commelin]

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

[orlando]

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]

where is this + even defined?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

I can't find some x + some y = some (x+y)

[Kevin Buzzard]

norm_cast won't do it

[Kevin Buzzard]

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]

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]

@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]

I don't know why apply can't apply this or why library_search can't find it though.

[Kevin Buzzard]

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]

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]

aah, coe_add isn't tagged with one of these norm_cast tags.

[Reid Barton]

Why are you mucking around with casts and stuff?

[Kevin Buzzard]

because I couldn't find the algebraic class which with_bot nat was

[Reid Barton]

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

[Kevin Buzzard]

but you're right, it's an ordered_add_comm_monoid.

[Kenny Lau]

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]

my proof is shorter than kenny's :hole_in_one:

[Kenny Lau]

oh

[Kevin Buzzard]

with_bot.coe_le : ∀ {α : Type ?} [_inst_1 : partial_order α] {a b : α} {o : option α}, b ∈ o → (↑a ≤ o ↔ a ≤ b)

gaargh

[Kevin Buzzard]

that's not what coe_le is supposed to say

[Kenny Lau]

proposition to make \le inductive

[Reid Barton]

Hopefully it goes better than when I tried to do that to continuous...

[orlando]

@Reid Barton ... add_le_add_right' :+1: :+1: :+1:

[Kevin Buzzard]

The trick is to realise that it's an ordered_add_comm_monoid

[orlando]

Yep Kevin ! That give property ! That good !

[Kevin Buzzard]

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]

Well, ideally library_search would have simply worked but probably it ran into the apply bug

[Reid Barton]

But otherwise, yes that would be nice to have.

[orlando]

libraty_search and suggest are nice tactic !!!

[Kevin Buzzard]

"and then tell me all the lemmas which apply to that object". I see. That's what library_searchis supposed to do?

[orlando]

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]

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,
  interaction_monad.result.cases_on t (f d) result.exception

#print interaction_monad.monad

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]

add_semigroup ℕ
has_sub ℕ
inhabited ℕ
add_monoid ℕ
has_well_founded ℕ
semigroup ℕ
has_lt ℕ
has_to_tactic_format ℕ
decidable_linear_ordered_cancel_add_comm_monoid ℕ
has_to_format ℕ
has_one ℕ
monoid ℕ
preorder ℕ
add_comm_monoid ℕ
add_comm_semigroup ℕ
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 ℕ
add_right_cancel_semigroup ℕ
ordered_semiring ℕ
decidable_linear_order ℕ
has_add ℕ
mul_zero_class ℕ
has_dvd ℕ
semiring ℕ
has_mul ℕ
has_div ℕ
add_left_cancel_semigroup ℕ
decidable_linear_ordered_semiring ℕ
linear_ordered_semiring ℕ
ordered_cancel_add_comm_monoid ℕ
comm_semiring ℕ
partial_order ℕ

[Mario Carneiro]

example : true := by {list_instances (with_bot ℕ), trivial}
-- add_semigroup (with_bot ℕ)
-- inhabited (with_bot ℕ)
-- semilattice_sup_bot (with_bot ℕ)
-- add_monoid (with_bot ℕ)
-- has_well_founded (with_bot ℕ)
-- has_lt (with_bot ℕ)
-- has_to_tactic_format (with_bot ℕ)
-- lattice (with_bot ℕ)
-- has_sup (with_bot ℕ)
-- ordered_add_comm_monoid (with_bot ℕ)
-- has_to_format (with_bot ℕ)
-- has_one (with_bot ℕ)
-- distrib_lattice (with_bot ℕ)
-- preorder (with_bot ℕ)
-- add_comm_monoid (with_bot ℕ)
-- add_comm_semigroup (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 ℕ)
-- has_add (with_bot ℕ)
-- semilattice_sup (with_bot ℕ)
-- has_inf (with_bot ℕ)
-- order_bot (with_bot ℕ)
-- partial_order (with_bot ℕ)

[Kevin Buzzard]

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]

@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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

@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  *,
      exact leading_coeff_C _,
    },
    {
        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,
    },
    rw finset.sum_const,  rw add_monoid.smul_one,
                                            ---- here i have to use nat.cast = with_bot coe  HERE
      refine cast_with_bot  _ ,
end

[Kevin Buzzard]

Maybe sometimes it is unavoidable?

[Kevin Buzzard]

Maybe there is a missing simp lemma though?

[Kevin Buzzard]

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]

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]

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

[orlando]

hint give me a commandunfold_coes :grinning_face_with_smiling_eyes:

[Mario Carneiro]

there should be a theorem that says they are the same

[Kevin Buzzard]

But should the user be required to know its name?

[Mario Carneiro]

first the theorem, then the fancy

[Kevin Buzzard]

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

[Mario Carneiro]

are we sure the theorem even exists?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[orlando]

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

[Mario Carneiro]

does that even typecheck?

[Kevin Buzzard]

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]

what are the types

[Kevin Buzzard]

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

[Mario Carneiro]

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

[orlando]

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]

just over nat though?

[Mario Carneiro]

#2636

[Mario Carneiro]

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

[orlando]

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

[Johan Commelin]

Congratulations!

[Johan Commelin]

So now we know that eigenvalues exist (-;

[Johan Commelin]

What is the determinant of a 0x0 matrix?

[Johan Commelin]

I guess it's 1

[Kenny Lau]

Johan Commelin said:

So now we know that eigenvalues exist (-;

we don't know that C is alg. closed

[Johan Commelin]

We do

[Johan Commelin]

Chris did that ages ago

[Kenny Lau]

Johan Commelin said:

I guess it's 1

yes

[Kenny Lau]

Johan Commelin said:

Chris did that ages ago

wait what

[Johan Commelin]

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

[orlando]

@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]

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

[Johan Commelin]

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

[Johan Commelin]

If so, we quickly need to add that typeclass

[orlando]

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

[orlando]

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

[Kenny Lau]

what was the proof?

[Johan Commelin]

Of what?

[Johan Commelin]

@orlando Are you planning to PR this?

[Kenny Lau]

of FTA

[Johan Commelin]

@Chris Hughes :up:

[Bhavik Mehta]

Congratulations!!

[orlando]

@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]

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]

yeah you linked to https://ncatlab.org/nlab/show/fundamental+theorem+of+algebra#classical_fta_via_advanced_calculus

[Kenny Lau]

aha, you proof the open mapping theorem specifically for polynomials

[Kenny Lau]

which does not require complex analysis

[Kenny Lau]

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

[Johan Commelin]

@orlando I strongly encourage you to PR this

[Johan Commelin]

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

[Mario Carneiro]

Shouldn't that be theorem je_ne_sais_pas?

[Johan Commelin]

Je ne sais pas...

[orlando]

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

[Patrick Massot]

Johan Commelin said:

So now we know that eigenvalues exist (-;

Isn't it sad to use determinants for that?

[Patrick Massot]

Congratulations to Orlando anway!

[Patrick Massot]

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]

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]

@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]

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