Documentation

Linglib.Core.Data.Option.Compatible

Compatibility and agreement of partial values #

Two relations on Option α viewed as partial specifications: Option.Compatible holds when the two values do not disagree (if both are some, they coincide), Option.Agrees when both are some of the same value. Agrees is the positive-evidence strengthening of Compatible: none is compatible with everything and agrees with nothing.

[UPSTREAM] Mathlib candidate: no counterpart exists (Option.Rel relates none only to none, so it is not compatibility).

source
def Option.Compatible {α : Type u_1} (a b : Option α) :
Prop

Two partial values are compatible: if both are some, they coincide.

Equations
  • a.Compatible b = ∀ (x : α), x ∈ a → ∀ (y : α), y ∈ b → x = y
Instances For
    source
    def Option.Agrees {α : Type u_1} (a b : Option α) :
    Prop

    Two partial values agree: both are some of the same value.

    Equations
    • a.Agrees b = ∃ (x : α), x ∈ a ∧ x ∈ b
    Instances For
      source
      @[simp]
      theorem Option.compatible_none_left {α : Type u_1} {b : Option α} :
      none.Compatible b
      source
      @[simp]
      theorem Option.compatible_none_right {α : Type u_1} {a : Option α} :
      a.Compatible none
      source
      @[simp]
      theorem Option.compatible_some_some {α : Type u_1} {x y : α} :
      (some x).Compatible (some y) ↔ x = y
      source
      theorem Option.compatible_iff {α : Type u_1} {a b : Option α} :
      a.Compatible b ↔ a = none ∨ b = none ∨ a = b
      source
      theorem Option.Compatible.symm {α : Type u_1} {a b : Option α} (h : a.Compatible b) :
      b.Compatible a
      source
      @[simp]
      theorem Option.not_agrees_none_left {α : Type u_1} {b : Option α} :
      ¬none.Agrees b
      source
      @[simp]
      theorem Option.not_agrees_none_right {α : Type u_1} {a : Option α} :
      ¬a.Agrees none
      source
      @[simp]
      theorem Option.agrees_some_some {α : Type u_1} {x y : α} :
      (some x).Agrees (some y) ↔ x = y
      source
      theorem Option.agrees_iff {α : Type u_1} {a b : Option α} :
      a.Agrees b ↔ a ≠ none ∧ a = b
      source
      theorem Option.Agrees.symm {α : Type u_1} {a b : Option α} (h : a.Agrees b) :
      b.Agrees a
      source
      theorem Option.Agrees.compatible {α : Type u_1} {a b : Option α} (h : a.Agrees b) :
      a.Compatible b
      source
      @[instance_reducible]
      instance Option.instDecidableCompatibleOfDecidableEq {α : Type u_1} {a b : Option α} [DecidableEq α] :
      Decidable (a.Compatible b)
      Equations
      source
      @[instance_reducible]
      instance Option.instDecidableAgreesOfDecidableEq {α : Type u_1} {a b : Option α} [DecidableEq α] :
      Decidable (a.Agrees b)
      Equations