An example of a LinearOrderedCommMonoidWithZero in which the product of two positive elements vanishes.

This is the monoid with 3 elements 0, ε, 1 where ε ^ 2 = 0 and everything else is forced. The order is 0 < ε < 1. Since ε ^ 2 = 0, the product of strictly positive elements can vanish.

Relevant Zulip chat: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/mul_pos

inductive Counterexample.Foo : Type

The three element monoid.

• zero: Counterexample.Foo
• eps: Counterexample.Foo
• one: Counterexample.Foo

instance Counterexample.instDecidableEqFoo : DecidableEq Counterexample.Foo

Equations

• Counterexample.instDecidableEqFoo x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Counterexample.Foo.inhabited : Inhabited Counterexample.Foo

Equations

• Counterexample.Foo.inhabited = { default := Counterexample.Foo.zero }

instance Counterexample.Foo.instZero : Zero Counterexample.Foo

Equations

• Counterexample.Foo.instZero = { zero := Counterexample.Foo.zero }

instance Counterexample.Foo.instOne : One Counterexample.Foo

Equations

• Counterexample.Foo.instOne = { one := Counterexample.Foo.one }

def Counterexample.Foo.aux1 : Counterexample.Foo → ℕ

The order on Foo is the one induced by the natural order on the image of aux1.

Equations

• x.aux1 = match x with | Counterexample.Foo.zero => 0 | Counterexample.Foo.eps => 1 | Counterexample.Foo.one => 2

def Counterexample.Foo.boom : Lean.ParserDescr

A tactic to prove facts by cases.

Equations

• Counterexample.Foo.boom = Lean.ParserDescr.node `Counterexample.Foo.boom 1024 (Lean.ParserDescr.nonReservedSymbol "boom" false)

theorem Counterexample.Foo.aux1_inj : Function.Injective Counterexample.Foo.aux1

instance Counterexample.Foo.linearOrder : LinearOrder Counterexample.Foo

Equations

• Counterexample.Foo.linearOrder = LinearOrder.lift' Counterexample.Foo.aux1 Counterexample.Foo.aux1_inj

def Counterexample.Foo.mul : Counterexample.Foo → Counterexample.Foo → Counterexample.Foo

Multiplication on Foo: the only external input is that ε ^ 2 = 0.

Equations

• x✝.mul x = match x✝, x with | Counterexample.Foo.one, x => x | x, Counterexample.Foo.one => x | x, x_1 => 0

instance Counterexample.Foo.commMonoid : CommMonoid Counterexample.Foo

Equations

• Counterexample.Foo.commMonoid = CommMonoid.mk Counterexample.Foo.commMonoid.proof_6

instance Counterexample.Foo.instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero Counterexample.Foo

Equations

• One or more equations did not get rendered due to their size.

theorem Counterexample.Foo.not_mul_pos : ¬∀ {M : Type} [inst : LinearOrderedCommMonoidWithZero M] (a b : M), 0 < a → 0 < b → 0 < a * b