From 4e04d373e46d1de6fc884666de444b9cc74cda55 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Mar 2019 07:38:09 -0800 Subject: [PATCH] =?UTF-8?q?feat(library/init):=20unicode=20notation=20for?= =?UTF-8?q?=20heq:=20=E2=89=85?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- library/init/core.lean | 48 ++++++++++++++++++++++-------------------- library/init/wf.lean | 10 ++++----- 2 files changed, 30 insertions(+), 28 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 1b01456573..4a185b6719 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -23,6 +23,7 @@ reserve infix ` ↔ `:20 reserve infix ` = `:50 reserve infix ` == `:50 reserve infix ` ~= `:50 +reserve infix ` ≅ `:50 reserve infix ` ≠ `:50 reserve infix ` ≈ `:50 reserve infix ` ~ `:50 @@ -250,10 +251,11 @@ theorem eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a := h ▸ rfl infix ~= := heq +infix ≅ := heq -@[pattern] def heq.rfl {α : Sort u} {a : α} : a ~= a := heq.refl a +@[pattern] def heq.rfl {α : Sort u} {a : α} : a ≅ a := heq.refl a -theorem eq_of_heq {α : Sort u} {a a' : α} (h : a ~= a') : a = a' := +theorem eq_of_heq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' := have ∀ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from λ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl), show (eq.ndrec_on (eq.refl α) a : α) = a', from @@ -731,53 +733,53 @@ section variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ} @[elab_as_eliminator] -theorem {u1 u2} heq.ndrec {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ~= b) : C b := +theorem {u1 u2} heq.ndrec {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b := @heq.rec α a (λ β b _, C b) m β b h @[elab_as_eliminator] -theorem {u1 u2} heq.ndrec_on {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ~= b) (m : C a) : C b := +theorem {u1 u2} heq.ndrec_on {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b := @heq.rec α a (λ β b _, C b) m β b h -theorem heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ~= b) (h₂ : p a) : p b := +theorem heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b := eq.rec_on (eq_of_heq h₁) h₂ -theorem heq.subst {p : ∀ T : Sort u, T → Prop} (h₁ : a ~= b) (h₂ : p α a) : p β b := +theorem heq.subst {p : ∀ T : Sort u, T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b := heq.ndrec_on h₁ h₂ -theorem heq.symm (h : a ~= b) : b ~= a := +theorem heq.symm (h : a ≅ b) : b ≅ a := heq.ndrec_on h (heq.refl a) -theorem heq_of_eq (h : a = a') : a ~= a' := +theorem heq_of_eq (h : a = a') : a ≅ a' := eq.subst h (heq.refl a) -theorem heq.trans (h₁ : a ~= b) (h₂ : b ~= c) : a ~= c := +theorem heq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c := heq.subst h₂ h₁ -theorem heq_of_heq_of_eq (h₁ : a ~= b) (h₂ : b = b') : a ~= b' := +theorem heq_of_heq_of_eq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' := heq.trans h₁ (heq_of_eq h₂) -theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : a' ~= b) : a ~= b := +theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b := heq.trans (heq_of_eq h₁) h₂ -def type_eq_of_heq (h : a ~= b) : α = β := +def type_eq_of_heq (h : a ≅ b) : α = β := heq.ndrec_on h (eq.refl α) end -theorem eq_rec_heq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') ~= p +theorem eq_rec_heq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') ≅ p | a _ rfl p := heq.refl p -theorem heq_of_eq_rec_left {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : φ a') = p₂), p₁ ~= p₂ +theorem heq_of_eq_rec_left {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : φ a') = p₂), p₁ ≅ p₂ | a _ p₁ p₂ rfl h := eq.rec_on h (heq.refl p₁) -theorem heq_of_eq_rec_right {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ ~= p₂ +theorem heq_of_eq_rec_right {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ ≅ p₂ | a _ p₁ p₂ rfl h := have p₁ = p₂, from h, this ▸ heq.refl p₁ -theorem of_heq_true {a : Prop} (h : a ~= true) : a := +theorem of_heq_true {a : Prop} (h : a ≅ true) : a := of_eq_true (eq_of_heq h) -theorem cast_heq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ~= a +theorem cast_heq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a | α _ rfl a := heq.refl a variables {a b c d : Prop} @@ -905,7 +907,7 @@ iff.intro false_of_ne false.elim theorem eq_self_iff_true {α : Sort u} (a : α) : (a = a) ↔ true := iff_true_intro rfl -theorem heq_self_iff_true {α : Sort u} (a : α) : (a ~= a) ↔ true := +theorem heq_self_iff_true {α : Sort u} (a : α) : (a ≅ a) ↔ true := iff_true_intro (heq.refl a) theorem iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false := @@ -1435,7 +1437,7 @@ class inductive subsingleton (α : Sort u) : Prop protected def subsingleton.elim {α : Sort u} [h : subsingleton α] : ∀ (a b : α), a = b := subsingleton.cases_on h (λ p, p) -protected def subsingleton.helim {α β : Sort u} [h : subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a ~= b := +protected def subsingleton.helim {α β : Sort u} [h : subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a ≅ b := eq.rec_on h (λ a b : α, heq_of_eq (subsingleton.elim a b)) instance subsingleton_prop (p : Prop) : subsingleton p := @@ -1466,7 +1468,7 @@ theorem let_value_eq {α : Sort u} {β : Sort v} {a₁ a₂ : α} (b : α → β λ h, eq.ndrec_on h rfl theorem let_value_heq {α : Sort v} {β : α → Sort u} {a₁ a₂ : α} (b : Π x : α, β x) : - a₁ = a₂ → (let x : α := a₁ in b x) ~= (let x : α := a₂ in b x) := + a₁ = a₂ → (let x : α := a₁ in b x) ≅ (let x : α := a₂ in b x) := λ h, eq.ndrec_on h (heq.refl (b a₁)) theorem let_body_eq {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : Π x : α, β x} : @@ -1824,10 +1826,10 @@ quot.rec f (λ a b h, subsingleton.elim _ (f b)) q @[reducible, elab_as_eliminator, inline] protected def hrec_on - (q : quot r) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : r a b), f a ~= f b) : β q := + (q : quot r) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q := quot.rec_on q f $ λ a b p, eq_of_heq $ - have p₁ : (eq.rec (f a) (sound p) : β ⟦b⟧) ~= f a, from eq_rec_heq (sound p) (f a), + have p₁ : (eq.rec (f a) (sound p) : β ⟦b⟧) ≅ f a, from eq_rec_heq (sound p) (f a), heq.trans p₁ (c a b p) end @@ -1889,7 +1891,7 @@ protected def rec_on_subsingleton @[reducible, elab_as_eliminator, inline] protected def hrec_on - (q : quotient s) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : a ≈ b), f a ~= f b) : β q := + (q : quotient s) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : a ≈ b), f a ≅ f b) : β q := quot.hrec_on q f c end diff --git a/library/init/wf.lean b/library/init/wf.lean index b8b85e32db..309e337509 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -228,18 +228,18 @@ acc.ndrec_on aca (λ xb acb (ihb : ∀ (y : β xa), s xa y xb → acc (lex r s) ⟨xa, y⟩), acc.intro ⟨xa, xb⟩ (λ p (lt : p ≺ ⟨xa, xb⟩), - have aux : xa = xa → xb ~= xb → acc (lex r s) p, from - @psigma.lex.rec_on α β r s (λ p₁ p₂ _, p₂.1 = xa → p₂.2 ~= xb → acc (lex r s) p₁) + have aux : xa = xa → xb ≅ xb → acc (lex r s) p, from + @psigma.lex.rec_on α β r s (λ p₁ p₂ _, p₂.1 = xa → p₂.2 ≅ xb → acc (lex r s) p₁) p ⟨xa, xb⟩ lt - (λ (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ ~= xb), + (λ (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ ≅ xb), have aux : (∀ (y : α), r y xa → ∀ (b : β y), acc (lex r s) ⟨y, b⟩) → r a₁ a₂ → ∀ (b₁ : β a₁), acc (lex r s) ⟨a₁, b₁⟩, from eq.subst eq₂ (λ iha h b₁, iha a₁ h b₁), aux iha h b₁) - (λ (a : α) (b₁ b₂ : β a) (h : s a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ ~= xb), + (λ (a : α) (b₁ b₂ : β a) (h : s a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ ≅ xb), have aux : ∀ (xb : β xa), (∀ (y : β xa), s xa y xb → acc (s xa) y) → (∀ (y : β xa), s xa y xb → acc (lex r s) ⟨xa, y⟩) → - lex r s p ⟨xa, xb⟩ → ∀ (b₁ : β a), s a b₁ b₂ → b₂ ~= xb → acc (lex r s) ⟨a, b₁⟩, + lex r s p ⟨xa, xb⟩ → ∀ (b₁ : β a), s a b₁ b₂ → b₂ ≅ xb → acc (lex r s) ⟨a, b₁⟩, from eq.subst eq₂ (λ xb acb ihb lt b₁ h eq₃, have new_eq₃ : b₂ = xb, from eq_of_heq eq₃, have aux : (∀ (y : β a), s a y xb → acc (lex r s) ⟨a, y⟩) →