mul_pos

Stream: maths

[Johan Commelin]

import algebra.linear_ordered_comm_group_with_zero

open_locale classical

lemma mul_pos'''' {M : Type*} [linear_ordered_comm_monoid_with_zero M]
  (a b : M) (ha : 0 < a) (hb : 0 < b) :
  0 < a * b :=
begin
  admit,
end

Is this true?

[Johan Commelin]

#xy:

example {ι : Type*} (s : finset ι) (f : ι → ℕ) (h : ∀ i, 0 < f i) :
  0 < ∏ i in s, f i :=
begin
  sorry
end

[Kevin Buzzard]

Yes it's true update: erm...

[Johan Commelin]

I know I can prove the second example by passing to int or pnat, but that feels like a hack around a hole in the library.

[Johan Commelin]

I don't understant the contortion linear_ordered_comm_monoid_with_zero well enough to know whether my set of examples covers its behaviour...

[Kevin Buzzard]

I've got it down to a,b!=0 implies ab!=0 and this is surely true for any linearly ordered structure

[Johan Commelin]

Right, I got that far as well...

[Damiano Testa]

I am not sure that there is a proof in Lean that a linear order has no non-trivial zero divisors... seems like a job for the new notion of regular! :stuck_out_tongue_wink:

[Rémy Degenne]

I see no reference to a linear order in the instances of docs#no_zero_divisors

[Kevin Buzzard]

So how about {0,eps,1} with eps^2=0 and all other multiplications the obvious ones?

[Kevin Buzzard]

:-/

[Damiano Testa]

Should this go in the counterexamples folder? :smile:

[Kevin Buzzard]

Is it definitely a counterexample?

[Kevin Buzzard]

I need to prepare my class :-(

[Damiano Testa]

I am not sure: of course, the weird thing is eps^2 not being positive, but I do not know if this is precluded by the axioms of linear...

[Kevin Buzzard]

It sounds right though. I've even seen this example before. The valuation on Z_p takes values in [0,1], and now if you want to quotient and get some kind of valuation on Z/p^nZ then you need to quotient the target too, and get {0} union (1/p^n,1], and this comes up in tilting and is precisely the reason I wanted to switch from linear_ordered_comm_group_with_zero as the target of a valuation to linear_ordered_comm_monoid_with_zero.

[Kevin Buzzard]

Update on this: I think I did all the groundwork for making that change (e.g. I made the class!) but I never did the switch for the target of a valuation IIRC.

[Rémy Degenne]

going through the fields of linear_ordered_comm_monoid_with_zero one by one, it looks like it fits. I did not code anything to verify though.

[Kevin Buzzard]

If it doesn't fit then I need to completely re-evaluate the "change group to monoid" idea for valuations, because my understanding of what is going on is wrong. I was completely wrong when I claimed 0<a -> 0<b -> 0<ab was true, I even knew this counterexample.

[Johan Commelin]

import algebra.ordered_monoid

@[derive [decidable_eq]]
inductive foo
| zero
| eps
| one

namespace foo

instance : has_zero foo := ⟨zero⟩
instance : has_one foo := ⟨one⟩
notation `ε` := eps

def aux1 : foo → ℕ
| 0 := 0
| ε := 1
| 1 := 2

meta def boom : tactic unit :=
`[repeat {rintro ⟨⟩}; dec_trivial]

lemma aux1_inj : function.injective aux1 :=
by boom

instance : linear_order foo :=
linear_order.lift aux1 $ aux1_inj

def mul : foo → foo → foo
| 0 _ := 0
| ε 1 := ε
| ε _ := 0
| 1 x := x

instance : comm_monoid foo :=
{ mul := mul,
  one := 1,
  one_mul := by boom,
  mul_one := by boom,
  mul_comm := by boom,
  mul_assoc := by boom }

instance : linear_ordered_comm_monoid_with_zero foo :=
{ zero := 0,
  zero_mul := by boom,
  mul_zero := by boom,
  mul_le_mul_left := by { rintro ⟨⟩ ⟨⟩ h ⟨⟩; revert h; dec_trivial },
  lt_of_mul_lt_mul_left := by { rintro ⟨⟩ ⟨⟩ ⟨⟩; dec_trivial },
  zero_le_one := dec_trivial,
  .. foo.linear_order,
  .. foo.comm_monoid }

end foo

[Johan Commelin]

Thanks for the counterexample Kevin!

[Kevin Buzzard]

Good to know that my global understanding was correct and my local error was just that!

[Kevin Buzzard]

PR it to the counterexamples directory!

[Johan Commelin]

That directory doesn't exist yet, right?

[Damiano Testa]

it does in the branch counterexamples

[Damiano Testa]

but i never created a PR...

[Damiano Testa]

because I am not sure that what I wrote there would actually be acceptable for mathlib, even in the counterexamples directory!

[Damiano Testa]

https://github.com/leanprover-community/mathlib/tree/counterexamples

[Kevin Buzzard]

I dream of a linter which, for any ordered pair of distinct prop-valued classes, checks that either there's an instance showing that one implies the other, or a counterexample showing that it doesn't :-)

[Damiano Testa]

You can golf your multiplication as follows:

def mul1 : foo → foo → foo
| 1 x := x
| x 1 := x
| _ _ := 0

lemma muleq : mul = mul1 :=
begin
  ext1 a, ext1 b,
  cases a;cases b;
  boom,
end

(This is simply me trying to learn how to use the equation compiler.)

[Johan Commelin]

aah, good catch (-;

[Damiano Testa]

Kevin, your linter seems great! I hope that it will exist one day!

The counterexamples folder is a home-remedy for it...

[Damiano Testa]

Johan, given that you wrote down a fully formalized proof of the example, it will be very little work to add it to counterexamples: there is a non-existent review process for that branch!

If you want, I can push it, but feel free to do so yourself, if you prefer!

[Johan Commelin]

Ooh, feel free to add it

[Johan Commelin]

We should have a journal "Counterexamples of Mathematics" with a nonexistent review process. Sounds like an awesome place to publish :rofl:

[Damiano Testa]

Ahaha

In the meanwhile, the CI is working on it: I guess this counts as one of the most thorough refereeing processes, after actually getting into mathlib!

[Damiano Testa]

Johan, the referee report is back: your proof is correct!