Soft Constraint Semirings.

constraint.lean

import algebra.ring
import data.real.ennreal
import tactic

-- Bistarelli, S. Semirings for Soft Constraint Solving and Programming
-- Minicz, M. Construção de Árvore de Multicast para Redes de Missão Crítica

universe u

class constraint_semiring (α : Type u) extends comm_semiring α :=
(add_idem : ∀ a : α, a + a = a)
(one_add : ∀ a : α, 1 + a = 1)
(add_one : ∀ a : α, a + 1 = 1)

namespace constraint_semiring

variables {α : Type u} [constraint_semiring α] {a b c : α}

instance : partial_order α :=
{ le := λ a b, a + b = b,
  le_refl := add_idem,
  le_trans :=
  begin
    change ∀ a b c, _ = _ → _ = _ → _ = _,
    intros _ _ _ h₁ h₂,
    rw [←h₂, ←add_assoc, h₁]
  end,
  le_antisymm :=
  begin
    change ∀ a b, _ = _ → _ = _ → _ = _,
    intros _ _ h₁ h₂,
    rwa [←h₂, add_comm]
  end }

instance {β : Type u} [constraint_semiring β] :
  constraint_semiring (α × β) :=
{ add := λ a b, ⟨a.1 + b.1, a.2 + b.2⟩,
  add_assoc := λ _ _ _, by simp [@add_assoc α, @add_assoc β],
  zero := ⟨0, 0⟩,
  zero_add := λ _, by { change (_ + _, _ + _) = _, simp },
  add_zero := λ _, by { change (_ + _, _ + _) = _, simp },
  add_comm :=
  begin
    change ∀ _ _, (_ + _, _ + _) = (_ + _, _ + _),
    simp [@add_comm α, @add_comm β]
  end,
  mul := λ a b, ⟨a.1 * b.1, a.2 * b.2⟩,
  mul_assoc := λ _ _ _, by simp [@mul_assoc α, @mul_assoc β],
  one := ⟨1, 1⟩,
  one_mul := by { change ∀ _, (_ * _, _ * _) = _, simp },
  mul_one := by { change ∀ _, (_ * _, _ * _) = _, simp },
  left_distrib := λ _ _ _, by simp [@left_distrib α, @left_distrib β],
  right_distrib := λ _ _ _, by simp [@right_distrib α, @right_distrib β],
  zero_mul := by simp,
  mul_zero := by simp,
  mul_comm :=
  begin
    change ∀ _ _, (_ * _, _ * _) = (_ * _, _ * _),
    simp [@mul_comm α, @mul_comm β]
  end,
  add_idem :=
  begin
    change ∀ _, (_ + _, _ + _) = _,
    simp [@add_idem α, @add_idem β]
  end,
  one_add :=
  begin
    change ∀ _, (_ + _, _ + _) = _,
    unfold has_one.one monoid.one semiring.one,
    unfold comm_semiring.one,
    simp [@one_add α, @one_add β]
  end,
  add_one :=
  begin
    change ∀ _, (_ + _, _ + _) = _,
    unfold has_one.one monoid.one semiring.one,
    unfold comm_semiring.one,
    simp [@add_one α, @add_one β]
  end }

end constraint_semiring

noncomputable theory

variables {a b : ennreal}

@[simp] lemma ennreal.min_top_left : min ⊤ a = a := by simp

@[simp] lemma ennreal.min_top_right : min a ⊤ = a := by simp

@[simp] lemma ennreal.min_zero_left : min 0 a = 0 := by simp

@[simp] lemma ennreal.min_zero_right : min a 0 = 0 := by simp

@[simp] lemma ennreal.max_top_left : max ⊤ a = ⊤ := by simp

@[simp] lemma ennreal.max_top_right : max a ⊤ = ⊤ := by simp

-- ⟨ℝ⁺, max, min, 0, ∞⟩
def bandwidth : constraint_semiring ennreal :=
{ add := max,
  add_assoc := max_assoc,
  zero := 0,
  zero_add := @ennreal.max_zero_left,
  add_zero := @ennreal.max_zero_right,
  add_comm := max_comm,
  mul := min,
  mul_assoc := min_assoc,
  one := ⊤,
  one_mul := @ennreal.min_top_left,
  mul_one := @ennreal.min_top_right,
  left_distrib := @min_max_distrib_left _ _,
  right_distrib := @min_max_distrib_right _ _,
  zero_mul := @ennreal.min_zero_left,
  mul_zero := @ennreal.min_zero_right,
  mul_comm := min_comm,
  add_idem := max_self,
  one_add := @ennreal.max_top_left,
  add_one := @ennreal.max_top_right }

-- ⟨ℝ⁺, min, +, ∞, 0⟩
def delay : constraint_semiring ennreal :=
{ add := min,
  add_assoc := min_assoc,
  zero := ⊤,
  zero_add := @ennreal.min_top_left,
  add_zero := @ennreal.min_top_right,
  add_comm := min_comm,
  mul := (+),
  mul_assoc := add_assoc,
  one := 0,
  one_mul := zero_add,
  mul_one := add_zero,
  left_distrib :=
  begin
    rintros ⟨⟩ ⟨⟩ ⟨⟩; try { simp },
    norm_cast,
    unfold min,
    by_cases b ≤ c,
    { simp [show b ≤ c, from h] },
    { simp [show ¬ b ≤ c, from h] }
  end,
  right_distrib :=
  begin
    rintros ⟨⟩ ⟨⟩ ⟨⟩; try { simp },
    norm_cast,
    unfold min,
    by_cases a ≤ b,
    { simp [show a ≤ b, from h] },
    { simp [show ¬ a ≤ b, from h] }
  end,
  zero_mul := by simp,
  mul_zero := by simp,
  mul_comm := add_comm,
  add_idem := min_self,
  one_add := @ennreal.min_zero_left,
  add_one := @ennreal.min_zero_right }