bhavik_owned.lean

/-
Copyright (c) 2021 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa
-/
import data.zmod.basic
import ring_theory.subsemiring.basic
import algebra.order.monoid
/-!

A `canonically_ordered_comm_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_comm_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
-/

namespace list

lemma subset_singleton {α} {a : α} : ∀ L : list α, L ⊆ [a] ↔ ∃ n, L = repeat a n
| [] := ⟨λ h, ⟨0, by simp⟩, by simp⟩
| (h :: L) := begin
  refine ⟨λ h, _, λ ⟨k, hk⟩, by simp [hk, repeat_subset_singleton]⟩,
  rw [cons_subset] at h,
  obtain ⟨n, rfl⟩ := (subset_singleton L).mp h.2,
  exact ⟨n.succ, by simp [mem_singleton.mp h.1]⟩
end

end list


namespace from_Bhavik

/--  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. -/
@[derive [comm_semiring]]
def K : Type := subsemiring.closure ({1.5} : set ℚ)

instance : has_coe K ℚ := ⟨λ x, x.1⟩

instance inhabited_K : inhabited K := ⟨0⟩

instance : preorder K :=
{ le := λ x y, x = y ∨ (x : ℚ) + 1 ≤ (y : ℚ),
  le_refl := λ x, or.inl rfl,
  le_trans := λ x y z xy yz,
  begin
    rcases xy with (rfl | _), { apply yz },
    rcases yz with (rfl | _), { right, apply xy },
    right,
    exact xy.trans (le_trans ((le_add_iff_nonneg_right _).mpr zero_le_one) yz)
  end }

example {x} (h : x ∈ subsemiring.closure ({1.5} : set ℚ)) : x = 0 ∨ 1 ≤ x :=
begin
  rw subsemiring.mem_closure_iff_exists_list at h,
  obtain ⟨L, hmem, rfl⟩ := h,
  replace hmem : ∀ t ∈ L, t ⊆ [(3 / 2 : ℚ)],
  { intros t ht,
    specialize hmem t ht,
    rw list.subset_def,
    simpa using hmem },
  induction L with b L ih,
  { simp },
  right,
  simp only [list.map, list.sum_cons],
  have triv : 0 ≤ (L.map list.prod).sum,
  { cases ih (λ t ht, hmem t $ or.inr ht) ; linarith },
  suffices : 1 ≤ b.prod, { linarith },
  obtain ⟨-|k, rfl⟩ := b.subset_singleton.mp (hmem b (by simp)),
  { simp },
  rw [list.prod_repeat],
  nth_rewrite 0 [← one_pow k.succ],
  refine pow_le_pow_of_le_left zero_le_one (by norm_num) k.succ,
end