Two element set (with `has_repr`)

tuple.lean

import tactic

section

parameter {α : Type}

def r (a b : α × α) : Prop := a = b ∨ (a.snd, a.fst) = b

lemma r_refl : reflexive r :=
λ _, or.inl rfl

lemma r_symm : symmetric r :=
begin
  rintros a ⟨b₁, b₂⟩ (h | h),
  { rw h, left, refl },
  { right, cases h, simp }
end

lemma r_trans : transitive r :=
begin
  rintros a b c (h₁ | h₁) (h₂ | h₂),
  { rw [h₁, h₂], left, refl },
  { rw h₁, right, cases h₂, simp },
  { rw ←h₂, right, cases h₁, simp },
  { cases h₁, cases h₂, left, simp }
end

instance r_setoid : setoid (α × α) :=
⟨r, r_refl, r_symm, r_trans⟩

def tuple : Type := quotient r_setoid

def tuple.mk (a₁ a₂ : α) : tuple := quotient.mk (a₁, a₂)

def distinct : list α → list tuple
| []  := []
| (a :: as) := list.map (tuple.mk a) as ++ distinct as

variables [linear_order α] [decidable_rel ((≤) : α → α → Prop)]

def order_pair : α × α → α × α
| ⟨a₁, a₂⟩ := if a₁ ≤ a₂ then (a₁, a₂) else (a₂, a₁)

def order_tuple (a : tuple) : α × α :=
begin
  apply quotient.lift_on a order_pair,
  rintros ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ (h | h),
  { rw h },
  { cases h, clear h,
    simp only [order_pair],
    rcases lt_trichotomy a₁ a₂ with (h | rfl | h);
    { refl <|> simp [le_of_lt h, not_le_of_lt h] } }
end

instance tuple.has_repr [has_repr α] : has_repr tuple :=
⟨repr ∘ order_tuple⟩

end