dcreager.net

Intersection of s₁..t₁ and ≠ t₂

The intersection of a range and a non-equivalent depends on how the two types are related.

(s₁..t₁) ∧ (≠ t₂) = ∅                  if s₁ = t₁ = t₂
                  = (s₁..t₁) ∧ (≠ t₂)  otherwise

Equationally

⟦s₁..t₁⟧ = {x | s₁ ⊆ x ∧ x ⊆ t₁}
⟦≠ t₂⟧   = {x | x ⊈ t₂ ∨ t₂ ⊈ x}

If s₁ = t₁, then the range constraint s₁..t₁ is actually an equivalence constraint = s₁; if also s₁ = t₂, then it's intuitive that the constraints should conflict with each other.

⟦(s..s) ∧ (≠ s)⟧
  = {x | s ⊆ x ∧ x ⊆ s} ∩ {x | x ⊈ s ∨ s ⊈ x}
  = {x | (s ⊆ x ∧ x ⊆ s) ∧ (x ⊈ s ∨ s ⊈ x)}
  = {x | (s ⊆ x ∧ x ⊆ s ∧ x ⊈ s) ∨ (s ⊆ x ∧ x ⊆ s ∧ s ⊈ x)}
  = {x | (s ⊆ x ∧ false) ∨ (false ∧ x ⊆ s)}
  = {x | false ∨ false}
  = {x | false}
  = ∅

Otherwise, the two constraints cannot be simplified.

» Theory » Constraints on sets