comparativeEquiv_trans

formal source

 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
 151  intro c₁ c₂ c₁' c₂' h₁ h₂ hle
 152  have heq₁ := hcompat c₁ c₁' h₁
 153  have heq₂ := hcompat c₂ c₂' h₂
 154  -- c₁' ≤ c₁ ≤ c₂ ≤ c₂'
 155  exact hp.trans c₁' c₂ c₂' (hp.trans c₁' c₁ c₂ heq₁.2 hle) heq₂.1
 156
 157/-! ## Separation by Comparisons -/
 158
 159/-- Two configurations are separated by a comparative recognizer if they are
 160    not comparatively equivalent -/