refactor(logic/relator): turn *_unique and *_total into defs, not cla…

…sses (#9135)

We had (almost) no instances for these classes and (almost) no lemmas taking these assumptions as TC arguments.

src/computability/turing_machine.lean

@@ -605,9 +605,9 @@ theorem reaches₁_eq {σ} {f : σ → option σ} {a b c}
 trans_gen.head'_iff.trans (trans_gen.head'_iff.trans $ by rw h).symm
 
 theorem reaches_total {σ} {f : σ → option σ}
-  {a b c} : reaches f a b → reaches f a c →
+  {a b c} (hab : reaches f a b) (hac : reaches f a c) :
   reaches f b c ∨ reaches f c b :=
-refl_trans_gen.total_of_right_unique ⟨λ _ _ _, option.mem_unique⟩
+refl_trans_gen.total_of_right_unique (λ _ _ _, option.mem_unique) hab hac
 
 theorem reaches₁_fwd {σ} {f : σ → option σ}
   {a b c} (h₁ : reaches₁ f a c) (h₂ : b ∈ f a) : reaches f b c :=

src/data/list/forall2.lean

@@ -93,24 +93,24 @@ lemma forall₂_and_left {r : α → β → Prop} {p : α → Prop} :
 | _ (b :: u) := by simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]
 
 lemma left_unique_forall₂' (hr : left_unique r) :
-  ∀ {a b c}, forall₂ r a b → forall₂ r c b → a = c
+  ∀ {a b c}, forall₂ r a c → forall₂ r b c → a = b
 | a₀ nil a₁ forall₂.nil forall₂.nil := rfl
 | (a₀ :: l₀) (b :: l) (a₁ :: l₁) (forall₂.cons ha₀ h₀) (forall₂.cons ha₁ h₁) :=
-  hr.unique ha₀ ha₁ ▸ left_unique_forall₂' h₀ h₁ ▸ rfl
+  hr ha₀ ha₁ ▸ left_unique_forall₂' h₀ h₁ ▸ rfl
 
-lemma left_unique_forall₂ (hr : left_unique r) : left_unique (forall₂ r) :=
-⟨@left_unique_forall₂' _ _ _ hr⟩
+lemma _root_.relator.left_unique.forall₂ (hr : left_unique r) : left_unique (forall₂ r) :=
+@left_unique_forall₂' _ _ _ hr
 
 lemma right_unique_forall₂' (hr : right_unique r) : ∀ {a b c}, forall₂ r a b → forall₂ r a c → b = c
 | nil a₀ a₁ forall₂.nil forall₂.nil := rfl
 | (b :: l) (a₀ :: l₀) (a₁ :: l₁) (forall₂.cons ha₀ h₀) (forall₂.cons ha₁ h₁) :=
-  hr.unique ha₀ ha₁ ▸ right_unique_forall₂' h₀ h₁ ▸ rfl
+  hr ha₀ ha₁ ▸ right_unique_forall₂' h₀ h₁ ▸ rfl
 
-lemma right_unique_forall₂ (hr : right_unique r) : right_unique (forall₂ r) :=
-⟨@right_unique_forall₂' _ _ _ hr⟩
+lemma _root_.relator.right_unique.forall₂ (hr : right_unique r) : right_unique (forall₂ r) :=
+@right_unique_forall₂' _ _ _ hr
 
-lemma bi_unique_forall₂ (hr : bi_unique r) : bi_unique (forall₂ r) :=
-@@bi_unique.mk _ (left_unique_forall₂ hr.1) (right_unique_forall₂ hr.2)
+lemma _root_.relator.bi_unique.forall₂ (hr : bi_unique r) : bi_unique (forall₂ r) :=
+⟨hr.left.forall₂, hr.right.forall₂⟩
 
 theorem forall₂_length_eq {R : α → β → Prop} :
   ∀ {l₁ l₂}, forall₂ R l₁ l₂ → length l₁ = length l₂

src/data/list/perm.lean

@@ -296,7 +296,7 @@ this ▸ hbd
 lemma rel_perm (hr : bi_unique r) : (forall₂ r ⇒ forall₂ r ⇒ (↔)) perm perm :=
 assume a b hab c d hcd, iff.intro
   (rel_perm_imp hr.2 hab hcd)
-  (rel_perm_imp (left_unique_flip hr.1) hab.flip hcd.flip)
+  (rel_perm_imp hr.left.flip hab.flip hcd.flip)
 
 end rel
 

src/data/option/basic.lean

@@ -71,7 +71,7 @@ theorem mem_unique {o : option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a
 option.some.inj $ ha.symm.trans hb
 
 theorem mem.left_unique : relator.left_unique ((∈) : α → option α → Prop) :=
-⟨λ a o b, mem_unique⟩
+λ a o b, mem_unique
 
 theorem some_injective (α : Type*) : function.injective (@some α) :=
 λ _ _, some_inj.mp

src/data/part.lean

@@ -69,7 +69,7 @@ theorem mem_unique : ∀ {a b : α} {o : part α}, a ∈ o → b ∈ o → a = b
 | _ _ ⟨p, f⟩ ⟨h₁, rfl⟩ ⟨h₂, rfl⟩ := rfl
 
 theorem mem.left_unique : relator.left_unique ((∈) : α → part α → Prop) :=
-⟨λ a o b, mem_unique⟩
+λ a o b, mem_unique
 
 theorem get_eq_of_mem {o : part α} {a} (h : a ∈ o) (h') : get o h' = a :=
 mem_unique ⟨_, rfl⟩ h

src/data/seq/computation.lean

@@ -240,7 +240,7 @@ theorem mem_unique {s : computation α} {a b : α} : a ∈ s → b ∈ s → a =
   (le_stable s (le_max_right m n) hb.symm)
 
 theorem mem.left_unique : relator.left_unique ((∈) : α → computation α → Prop) :=
-⟨λ a s b, mem_unique⟩
+λ a s b, mem_unique
 
 /-- `terminates s` asserts that the computation `s` eventually terminates with some value. -/
 class terminates (s : computation α) : Prop := (term : ∃ a, a ∈ s)

src/logic/relation.lean

@@ -257,7 +257,7 @@ begin
   { rcases IH with IH | IH,
     { rcases cases_head IH with rfl | ⟨e, be, ec⟩,
       { exact or.inr (single bd) },
-      { cases U.unique bd be, exact or.inl ec } },
+      { cases U bd be, exact or.inl ec } },
     { exact or.inr (IH.tail bd) } }
 end
 

src/logic/relator.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl
 Relator for functions, pairs, sums, and lists.
 -/
 
-import tactic.reserved_notation
+import logic.basic
 
 namespace relator
 universe variables u₁ u₂ v₁ v₂
@@ -30,50 +30,40 @@ infixr ⇒ := lift_fun
 
 end
 
-section
-variables {α : Type u₁} {β : out_param $ Type u₂} (R : out_param $ α → β → Prop)
-
-class right_total : Prop := (right : ∀b, ∃a, R a b)
-class left_total : Prop := (left : ∀a, ∃b, R a b)
-class bi_total extends left_total R, right_total R : Prop
-
-end
-
 section
 variables {α : Type u₁} {β : Type u₂} (R : α → β → Prop)
 
-class left_unique : Prop := (left : ∀{a b c}, R a b → R c b → a = c)
-class right_unique : Prop := (right : ∀{a b c}, R a b → R a c → b = c)
+def right_total : Prop := ∀ b, ∃ a, R a b
+def left_total : Prop := ∀ a, ∃ b, R a b
+def bi_total : Prop := left_total R ∧ right_total R
 
-lemma left_unique.unique {R : α → β → Prop} (h : left_unique R) {a b c} :
-  R a b → R c b → a = c := left_unique.left β
+def left_unique : Prop := ∀ ⦃a b c⦄, R a c → R b c → a = b
+def right_unique : Prop := ∀ ⦃a b c⦄, R a b → R a c → b = c
+def bi_unique : Prop := left_unique R ∧ right_unique R
 
-lemma right_unique.unique {R : α → β → Prop} (h : right_unique R) {a b c} :
-  R a b → R a c → b = c := right_unique.right α
+variable {R}
 
-lemma rel_forall_of_right_total [right_total R] :
+lemma right_total.rel_forall (h : right_total R) :
   ((R ⇒ implies) ⇒ implies) (λp, ∀i, p i) (λq, ∀i, q i) :=
-assume p q Hrel H b, exists.elim (right_total.right b) (assume a Rab, Hrel Rab (H _))
+assume p q Hrel H b, exists.elim (h b) (assume a Rab, Hrel Rab (H _))
 
-lemma rel_exists_of_left_total [left_total R] :
+lemma left_total.rel_exists (h : left_total R) :
   ((R ⇒ implies) ⇒ implies) (λp, ∃i, p i) (λq, ∃i, q i) :=
-assume p q Hrel ⟨a, pa⟩, let ⟨b, Rab⟩ := left_total.left a in ⟨b, Hrel Rab pa⟩
+assume p q Hrel ⟨a, pa⟩, (h a).imp $ λ b Rab, Hrel Rab pa
 
-lemma rel_forall_of_total [bi_total R] : ((R ⇒ iff) ⇒ iff) (λp, ∀i, p i) (λq, ∀i, q i) :=
+lemma bi_total.rel_forall (h : bi_total R) :
+  ((R ⇒ iff) ⇒ iff) (λp, ∀i, p i) (λq, ∀i, q i) :=
 assume p q Hrel,
-  ⟨assume H b, exists.elim (right_total.right b) (assume a Rab, (Hrel Rab).mp (H _)),
-    assume H a, exists.elim (left_total.left a) (assume b Rab, (Hrel Rab).mpr (H _))⟩
+  ⟨assume H b, exists.elim (h.right b) (assume a Rab, (Hrel Rab).mp (H _)),
+    assume H a, exists.elim (h.left a) (assume b Rab, (Hrel Rab).mpr (H _))⟩
 
-lemma rel_exists_of_total [bi_total R] : ((R ⇒ iff) ⇒ iff) (λp, ∃i, p i) (λq, ∃i, q i) :=
+lemma bi_total.rel_exists (h : bi_total R) : ((R ⇒ iff) ⇒ iff) (λp, ∃i, p i) (λq, ∃i, q i) :=
 assume p q Hrel,
-  ⟨assume ⟨a, pa⟩, let ⟨b, Rab⟩ := left_total.left a in ⟨b, (Hrel Rab).1 pa⟩,
-    assume ⟨b, qb⟩, let ⟨a, Rab⟩ := right_total.right b in ⟨a, (Hrel Rab).2 qb⟩⟩
+  ⟨assume ⟨a, pa⟩, (h.left a).imp $ λ b Rab, (Hrel Rab).1 pa,
+    assume ⟨b, qb⟩, (h.right b).imp $ λ a Rab, (Hrel Rab).2 qb⟩
 
 lemma left_unique_of_rel_eq {eq' : β → β → Prop} (he : (R ⇒ (R ⇒ iff)) eq eq') : left_unique R :=
-⟨λ a b c (ab : R a b) (cb : R c b),
-have eq' b b,
-  from iff.mp (he ab ab) rfl,
-iff.mpr (he ab cb) this⟩
+λ a b c (ac : R a c) (bc : R b c), (he ac bc).mpr ((he bc bc).mp rfl)
 
 end
 
@@ -83,18 +73,14 @@ assume p q h r s l, imp_congr h l
 lemma rel_not : (iff ⇒ iff) not not :=
 assume p q h, not_congr h
 
-@[priority 100] -- see Note [lower instance priority]
--- (this is an instance is always applies, since the relation is an out-param)
-instance bi_total_eq {α : Type u₁} : relator.bi_total (@eq α) :=
+lemma bi_total_eq {α : Type u₁} : relator.bi_total (@eq α) :=
 { left := λ a, ⟨a, rfl⟩, right := λ a, ⟨a, rfl⟩ }
 
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 variables {r : α → β → Prop} {p : β → γ → Prop} {q : γ → δ → Prop}
 
-class bi_unique (r : α → β → Prop) extends left_unique r, right_unique r : Prop
-
-lemma left_unique_flip : left_unique r → right_unique (flip r)
-| ⟨h⟩ := ⟨λ a b c h₁ h₂, h h₁ h₂⟩
+lemma left_unique.flip (h : left_unique r) : right_unique (flip r) :=
+λ a b c h₁ h₂, h h₁ h₂
 
 lemma rel_and : ((↔) ⇒ (↔) ⇒ (↔)) (∧) (∧) :=
 assume a b h₁ c d h₂, and_congr h₁ h₂
@@ -108,7 +94,7 @@ assume a b h₁ c d h₂, iff_congr h₁ h₂
 lemma rel_eq {r : α → β → Prop} (hr : bi_unique r) : (r ⇒ r ⇒ (↔)) (=) (=) :=
 assume a b h₁ c d h₂,
 iff.intro
-  begin intro h, subst h, exact right_unique.right α h₁ h₂ end
-  begin intro h, subst h, exact left_unique.left β h₁ h₂ end
+  begin intro h, subst h, exact hr.right h₁ h₂ end
+  begin intro h, subst h, exact hr.left h₁ h₂ end
 
 end relator