Zulip Chat Archive

Stream: maths

Topic: mul_pos


Johan Commelin (Feb 18 2021 at 10:07):

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 (Feb 18 2021 at 10:13):

#xy:

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

Kevin Buzzard (Feb 18 2021 at 10:13):

Yes it's true update: erm...

Johan Commelin (Feb 18 2021 at 10:13):

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 (Feb 18 2021 at 10:14):

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 (Feb 18 2021 at 10:15):

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

Johan Commelin (Feb 18 2021 at 10:16):

Right, I got that far as well...

Damiano Testa (Feb 18 2021 at 10:16):

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 (Feb 18 2021 at 10:17):

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

Kevin Buzzard (Feb 18 2021 at 10:22):

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

Kevin Buzzard (Feb 18 2021 at 10:23):

:-/

Damiano Testa (Feb 18 2021 at 10:24):

Should this go in the counterexamples folder? :smile:

Kevin Buzzard (Feb 18 2021 at 10:24):

Is it definitely a counterexample?

Kevin Buzzard (Feb 18 2021 at 10:25):

I need to prepare my class :-(

Damiano Testa (Feb 18 2021 at 10:26):

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 (Feb 18 2021 at 10:26):

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 (Feb 18 2021 at 10:27):

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 (Feb 18 2021 at 10:27):

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 (Feb 18 2021 at 10:29):

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 (Feb 18 2021 at 11:02):

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 (Feb 18 2021 at 11:03):

Thanks for the counterexample Kevin!

Kevin Buzzard (Feb 18 2021 at 11:04):

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

Kevin Buzzard (Feb 18 2021 at 11:05):

PR it to the counterexamples directory!

Johan Commelin (Feb 18 2021 at 11:10):

That directory doesn't exist yet, right?

Damiano Testa (Feb 18 2021 at 11:10):

it does in the branch counterexamples

Damiano Testa (Feb 18 2021 at 11:11):

but i never created a PR...

Damiano Testa (Feb 18 2021 at 11:11):

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

Damiano Testa (Feb 18 2021 at 11:12):

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

Kevin Buzzard (Feb 18 2021 at 11:13):

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 (Feb 18 2021 at 11:15):

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 (Feb 18 2021 at 11:18):

aah, good catch (-;

Damiano Testa (Feb 18 2021 at 11:33):

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

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

Damiano Testa (Feb 18 2021 at 14:58):

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 (Feb 18 2021 at 14:59):

Ooh, feel free to add it

Johan Commelin (Feb 18 2021 at 15:00):

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

Damiano Testa (Feb 18 2021 at 15:13):

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 (Feb 18 2021 at 19:02):

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


Last updated: Dec 20 2023 at 11:08 UTC