comparativeEquiv_refl

formal source

 117/-! ## Comparative Equivalence -/
 118
 119/-- Comparative equivalence is an equivalence relation -/
 120theorem comparativeEquiv_refl (R : ComparativeRecognizer C E) (gt_events : Set E)
 121    (h : InducesPreorder R gt_events) (c : C) :
 122    comparativeEquiv R gt_events c c :=
 123  ⟨preorder_refl R gt_events h c, preorder_refl R gt_events h c⟩
 124
 125theorem comparativeEquiv_symm (R : ComparativeRecognizer C E) (gt_events : Set E)
 126    {c₁ c₂ : C} (h : comparativeEquiv R gt_events c₁ c₂) :
 127    comparativeEquiv R gt_events c₂ c₁ :=
 128  ⟨h.2, h.1⟩
 129
 130theorem comparativeEquiv_trans (R : ComparativeRecognizer C E) (gt_events : Set E)
 131    (hp : InducesPreorder R gt_events)
 132    {c₁ c₂ c₃ : C} (h₁ : comparativeEquiv R gt_events c₁ c₂)
 133    (h₂ : comparativeEquiv R gt_events c₂ c₃) :
 134    comparativeEquiv R gt_events c₁ c₃ :=
 135  ⟨hp.trans c₁ c₂ c₃ h₁.1 h₂.1, hp.trans c₃ c₂ c₁ h₂.2 h₁.2⟩
 136
 137/-! ## Order-Respecting Recognizers -/
 138
 139/-- A standard recognizer R is compatible with a comparative recognizer R_cmp if
 140    indistinguishable configurations are also comparatively equivalent -/
 141def IsOrderCompatible (R : Recognizer C E) (R_cmp : ComparativeRecognizer C E')
 142    (gt_events : Set E') (hp : InducesPreorder R_cmp gt_events) : Prop :=
 143  ∀ c₁ c₂, Indistinguishable R c₁ c₂ → comparativeEquiv R_cmp gt_events c₁ c₂
 144
 145/-- If R is order-compatible, the order descends to the quotient -/
 146theorem order_descends_to_quotient (R : Recognizer C E) (R_cmp : ComparativeRecognizer C E')
 147    (gt_events : Set E') (hp : InducesPreorder R_cmp gt_events)
 148    (hcompat : IsOrderCompatible R R_cmp gt_events hp) :
 149    ∀ c₁ c₂ c₁' c₂', Indistinguishable R c₁ c₁' → Indistinguishable R c₂ c₂' →
 150      notGreaterThan R_cmp gt_events c₁ c₂ → notGreaterThan R_cmp gt_events c₁' c₂' := by