19eac5f341
This PR ensures that the configuration in `Simp.Config` is used when reducing terms and checking definitional equality in `simp`. closes #5455 --------- Co-authored-by: Kim Morrison <kim@tqft.net>
36 lines
1.3 KiB
Text
36 lines
1.3 KiB
Text
namespace Ordering
|
||
|
||
@[simp] theorem swap_swap {o : Ordering} : o.swap.swap = o := by cases o <;> rfl
|
||
|
||
@[simp] theorem swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂ :=
|
||
⟨fun h => by simpa using congrArg swap h, congrArg _⟩
|
||
|
||
end Ordering
|
||
|
||
/-- `OrientedCmp cmp` asserts that `cmp` is determined by the relation `cmp x y = .lt`. -/
|
||
class OrientedCmp (cmp : α → α → Ordering) : Prop where
|
||
/-- The comparator operation is symmetric, in the sense that if `cmp x y` equals `.lt` then
|
||
`cmp y x = .gt` and vice versa. -/
|
||
symm (x y) : (cmp x y).swap = cmp y x
|
||
|
||
namespace OrientedCmp
|
||
|
||
theorem cmp_eq_gt [OrientedCmp cmp] : cmp x y = .gt ↔ cmp y x = .lt := by
|
||
rw [← Ordering.swap_inj, symm]; exact .rfl
|
||
|
||
end OrientedCmp
|
||
|
||
/-- `TransCmp cmp` asserts that `cmp` induces a transitive relation. -/
|
||
class TransCmp (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
|
||
/-- The comparator operation is transitive. -/
|
||
le_trans : cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt
|
||
|
||
namespace TransCmp
|
||
variable [TransCmp cmp]
|
||
open OrientedCmp
|
||
|
||
theorem ge_trans (h₁ : cmp x y ≠ .lt) (h₂ : cmp y z ≠ .lt) : cmp x z ≠ .lt := by
|
||
have := @TransCmp.le_trans _ cmp _ z y x
|
||
simp [cmp_eq_gt] at *
|
||
-- `simp` did not fire at `this`
|
||
exact this h₂ h₁
|