A canonically ordered commutative semiring with two different elements a and b such that a ≠ b and 2 * a = 2 * b. Thus, multiplication by a fixed non-zero element of a canonically ordered semiring need not be injective. In particular, multiplying by a strictly positive element need not be strictly monotone.

Recall that a canonically ordered commutative semiring is a commutative semiring with a partial ordering that is "canonical" in the sense that the inequality a ≤ b holds if and only if there is a c such that a + c = b. There are several compatibility conditions among addition/multiplication and the order relation. The point of the counterexample is to show that monotonicity of multiplication cannot be strengthened to strict monotonicity.

Reference: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/canonically_ordered.20pathology

theorem Counterexample.mem_zmod_2 (a : ZMod 2) : Or (Eq a 0) (Eq a 1)

theorem Counterexample.add_self_zmod_2 (a : ZMod 2) : Eq (HAdd.hAdd a a) 0

def Counterexample.Nxzmod2.preN2 : PartialOrder (Prod Nat (ZMod 2))

The preorder relation on ℕ × ℤ/2ℤ where we only compare the first coordinate, except that we leave incomparable each pair of elements with the same first component. For instance, ∀ α, β ∈ ℤ/2ℤ, the inequality (1,α) ≤ (2,β) holds, whereas, ∀ n ∈ ℤ, the elements (n,0) and (n,1) are incomparable.

Equations

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

def Counterexample.Nxzmod2.csrN2 : CommSemiring (Prod Nat (ZMod 2))

Equations

• Eq Counterexample.Nxzmod2.csrN2 inferInstance

def Counterexample.Nxzmod2.csrN21 : AddCancelCommMonoid (Prod Nat (ZMod 2))

Equations

• Eq Counterexample.Nxzmod2.csrN21 { toAddCommMonoid := NonUnitalNonAssocSemiring.toAddCommMonoid, add_left_cancel := Counterexample.Nxzmod2.csrN21._proof_5 }

theorem Counterexample.Nxzmod2.lt_def {a b : Prod Nat (ZMod 2)} : Iff (LT.lt a b) (LT.lt a.fst b.fst)

A strict inequality forces the first components to be different.

theorem Counterexample.Nxzmod2.add_left_cancel (a b c : Prod Nat (ZMod 2)) : Eq (HAdd.hAdd a b) (HAdd.hAdd a c) → Eq b c

theorem Counterexample.Nxzmod2.add_le_add_left (a b : Prod Nat (ZMod 2)) : LE.le a b → ∀ (c : Prod Nat (ZMod 2)), LE.le (HAdd.hAdd c a) (HAdd.hAdd c b)

theorem Counterexample.Nxzmod2.le_of_add_le_add_left (a b c : Prod Nat (ZMod 2)) : LE.le (HAdd.hAdd a b) (HAdd.hAdd a c) → LE.le b c

theorem Counterexample.Nxzmod2.instZeroLEOneClassProdNatZModOfNat_counterexamples : ZeroLEOneClass (Prod Nat (ZMod 2))

theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_left (a b c : Prod Nat (ZMod 2)) : LT.lt a b → LT.lt 0 c → LT.lt (HMul.hMul c a) (HMul.hMul c b)

theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_right (a b c : Prod Nat (ZMod 2)) : LT.lt a b → LT.lt 0 c → LT.lt (HMul.hMul a c) (HMul.hMul b c)

def Counterexample.Nxzmod2.socsN2 : StrictOrderedCommSemiring (Prod Nat (ZMod 2))

Equations

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

def Counterexample.ExL.L : Type

Initially, L was defined as the subsemiring closure of (1,0).

Equations

• Eq Counterexample.ExL.L (Subtype fun (l : Prod Nat (ZMod 2)) => Ne l { fst := 0, snd := 1 })

theorem Counterexample.ExL.add_L {a b : Prod Nat (ZMod 2)} (ha : Ne a { fst := 0, snd := 1 }) (hb : Ne b { fst := 0, snd := 1 }) : Ne (HAdd.hAdd a b) { fst := 0, snd := 1 }

theorem Counterexample.ExL.mul_L {a b : Prod Nat (ZMod 2)} (ha : Ne a { fst := 0, snd := 1 }) (hb : Ne b { fst := 0, snd := 1 }) : Ne (HMul.hMul a b) { fst := 0, snd := 1 }

def Counterexample.ExL.lSubsemiring : Subsemiring (Prod Nat (ZMod 2))

The subsemiring corresponding to the elements of L, used to transfer instances.

Equations

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

def Counterexample.ExL.instOrderedCommSemiringL : OrderedCommSemiring L

Equations

• Eq Counterexample.ExL.instOrderedCommSemiringL Counterexample.ExL.lSubsemiring.toOrderedCommSemiring

def Counterexample.ExL.inhabited : Inhabited L

Equations

• Eq Counterexample.ExL.inhabited { default := 1 }

theorem Counterexample.ExL.bot_le (a : L) : LE.le 0 a

def Counterexample.ExL.orderBot : OrderBot L

Equations

• Eq Counterexample.ExL.orderBot { bot := 0, bot_le := Counterexample.ExL.bot_le }

theorem Counterexample.ExL.exists_add_of_le (a b : L) : LE.le a b → Exists fun (c : L) => Eq b (HAdd.hAdd a c)

theorem Counterexample.ExL.le_self_add (a b : L) : LE.le a (HAdd.hAdd a b)

theorem Counterexample.ExL.eq_zero_or_eq_zero_of_mul_eq_zero (a b : L) : Eq (HMul.hMul a b) 0 → Or (Eq a 0) (Eq b 0)

def Counterexample.ExL.instOrderedCommSemiringL_1 : OrderedCommSemiring L

Equations

• Eq Counterexample.ExL.instOrderedCommSemiringL_1 inferInstance

theorem Counterexample.ExL.instCanonicallyOrderedAddL : CanonicallyOrderedAdd L

theorem Counterexample.ExL.instNoZeroDivisorsL : NoZeroDivisors L