Documentation

Counterexamples.CanonicallyOrderedCommSemiringTwoMul

A CanonicallyOrderedCommSemiring 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 CanonicallyOrderedCommSemiring 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

def Counterexample.FromBhavik.K :

Bhavik Mehta's example. There are only the initial definitions, but no proofs. The Type K is a canonically ordered commutative semiring with the property that 2 * (1/2) ≤ 2 * 1, even though it is not true that 1/2 ≤ 1, since 1/2 and 1 are not comparable.

Instances For

instance Counterexample.FromBhavik.instCoeKRat :

Coe Counterexample.FromBhavik.K ℚ

instance Counterexample.FromBhavik.inhabitedK :

Inhabited Counterexample.FromBhavik.K

instance Counterexample.FromBhavik.instPreorderK :

Preorder Counterexample.FromBhavik.K

theorem Counterexample.mem_zmod_2 (a : ZMod 2) :

a = 0 ∨ a = 1

theorem Counterexample.add_self_zmod_2 (a : ZMod 2) :

a + a = 0

instance Counterexample.Nxzmod2.preN2 :

PartialOrder (ℕ × 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.

instance Counterexample.Nxzmod2.csrN2 :

CommSemiring (ℕ × ZMod 2)

instance Counterexample.Nxzmod2.csrN21 :

AddCancelCommMonoid (ℕ × ZMod 2)

@[simp]

theorem Counterexample.Nxzmod2.lt_def {a : ℕ × ZMod 2} {b : ℕ × ZMod 2} :

a < b ↔ a.fst < b.fst

A strict inequality forces the first components to be different.

theorem Counterexample.Nxzmod2.add_left_cancel (a : ℕ × ZMod 2) (b : ℕ × ZMod 2) (c : ℕ × ZMod 2) :

a + b = a + c → b = c

theorem Counterexample.Nxzmod2.add_le_add_left (a : ℕ × ZMod 2) (b : ℕ × ZMod 2) :

a ≤ b → ∀ (c : ℕ × ZMod 2), c + a ≤ c + b

theorem Counterexample.Nxzmod2.le_of_add_le_add_left (a : ℕ × ZMod 2) (b : ℕ × ZMod 2) (c : ℕ × ZMod 2) :

a + b ≤ a + c → b ≤ c

instance Counterexample.Nxzmod2.instZeroLEOneClassProdNatZModOfNatInstOfNatNatInstZeroToZeroLinearOrderedCommMonoidWithZeroToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldInstFieldZModFact_prime_twoInstOneToOneCanonicallyOrderedCommSemiringToOneToSemiringToDivisionSemiringToLEToPreorderPreN2 :

ZeroLEOneClass (ℕ × ZMod 2)

theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_left (a : ℕ × ZMod 2) (b : ℕ × ZMod 2) (c : ℕ × ZMod 2) :

a < b → 0 < c → c * a < c * b

theorem Counterexample.Nxzmod2.mul_lt_mul_of_pos_right (a : ℕ × ZMod 2) (b : ℕ × ZMod 2) (c : ℕ × ZMod 2) :

a < b → 0 < c → a * c < b * c

instance Counterexample.Nxzmod2.socsN2 :

StrictOrderedCommSemiring (ℕ × ZMod 2)

def Counterexample.ExL.L :

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

Instances For

theorem Counterexample.ExL.add_L {a : ℕ × ZMod 2} {b : ℕ × ZMod 2} (ha : a ≠ (0, 1)) (hb : b ≠ (0, 1)) :

a + b ≠ (0, 1)

theorem Counterexample.ExL.mul_L {a : ℕ × ZMod 2} {b : ℕ × ZMod 2} (ha : a ≠ (0, 1)) (hb : b ≠ (0, 1)) :

a * b ≠ (0, 1)

def Counterexample.ExL.lSubsemiring :

Subsemiring (ℕ × ZMod 2)

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

Instances For

instance Counterexample.ExL.instOrderedCommSemiringL :

OrderedCommSemiring Counterexample.ExL.L

instance Counterexample.ExL.inhabited :

Inhabited Counterexample.ExL.L

theorem Counterexample.ExL.bot_le (a : Counterexample.ExL.L) :

0 ≤ a

instance Counterexample.ExL.orderBot :

OrderBot Counterexample.ExL.L

theorem Counterexample.ExL.exists_add_of_le (a : Counterexample.ExL.L) (b : Counterexample.ExL.L) :

a ≤ b → ∃ c, b = a + c

theorem Counterexample.ExL.le_self_add (a : Counterexample.ExL.L) (b : Counterexample.ExL.L) :

a ≤ a + b

theorem Counterexample.ExL.eq_zero_or_eq_zero_of_mul_eq_zero (a : Counterexample.ExL.L) (b : Counterexample.ExL.L) :

a * b = 0 → a = 0 ∨ b = 0

instance Counterexample.ExL.can :

CanonicallyOrderedCommSemiring Counterexample.ExL.L