From 9f18d6545c45d3f1f29047963063d1fd09f071aa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Apr 2018 09:13:35 -0700 Subject: [PATCH] chore(library/init): remove `funext` and `quot` modules The spaghetti initialization is almost over. --- library/init/classical.lean | 2 +- library/init/core.lean | 308 ++++++++++++++++++++++++++++++++++- library/init/data/basic.lean | 2 +- library/init/data/quot.lean | 268 ------------------------------ library/init/default.lean | 2 +- library/init/function.lean | 2 +- library/init/funext.lean | 59 ------- 7 files changed, 310 insertions(+), 333 deletions(-) delete mode 100644 library/init/data/quot.lean delete mode 100644 library/init/funext.lean diff --git a/library/init/classical.lean b/library/init/classical.lean index c6b1bfad2a..ad6700409f 100644 --- a/library/init/classical.lean +++ b/library/init/classical.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro -/ prelude -import init.funext +import init.core namespace classical universes u v diff --git a/library/init/core.lean b/library/init/core.lean index 3eb35bea30..ee76edc875 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -1234,7 +1234,6 @@ theorem bool.ff_ne_tt : ff = tt → false def is_dec_eq {α : Sort u} (p : α → α → bool) : Prop := ∀ ⦃x y : α⦄, p x y = tt → x = y def is_dec_refl {α : Sort u} (p : α → α → bool) : Prop := ∀ x, p x x = tt -open decidable instance : decidable_eq bool | ff ff := is_true rfl | ff tt := is_false bool.ff_ne_tt @@ -1259,7 +1258,7 @@ match (h a b) with | (is_false n₁) := proof_irrel n n₁ ▸ eq.refl (is_false n) end - +/- if-then-else expression theorems -/ theorem if_pos {c : Prop} [h : decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t := match h with @@ -1770,3 +1769,308 @@ eq.subst (@iff_eq_eq a false) this theorem eq_true {a : Prop} : (a = true) = a := have (a ↔ true) = a, from propext (iff_true a), eq.subst (@iff_eq_eq a true) this + +/- Quotients -/ + +-- iff can now be used to do substitutions in a calculation +@[subst] theorem iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b := +eq.subst (propext h₁) h₂ + +namespace quot +constant sound : Π {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b + +attribute [elab_as_eliminator] lift ind + +protected theorem lift_beta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀ a b, r a b → f a = f b) (a : α) : lift f c (quot.mk r a) = f a := +rfl + +protected theorem ind_beta {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} (p : ∀ a, β (quot.mk r a)) (a : α) : (ind p (quot.mk r a) : β (quot.mk r a)) = p a := +rfl + +@[reducible, elab_as_eliminator] +protected def lift_on {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : quot r) (f : α → β) (c : ∀ a b, r a b → f a = f b) : β := +lift f c q + +@[elab_as_eliminator] +protected theorem induction_on {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} (q : quot r) (h : ∀ a, β (quot.mk r a)) : β q := +ind h q + +theorem exists_rep {α : Sort u} {r : α → α → Prop} (q : quot r) : ∃ a : α, (quot.mk r a) = q := +quot.induction_on q (λ a, ⟨a, rfl⟩) + +section +variable {α : Sort u} +variable {r : α → α → Prop} +variable {β : quot r → Sort v} + +local notation `⟦`:max a `⟧` := quot.mk r a + +@[reducible] +protected def indep (f : Π a, β ⟦a⟧) (a : α) : psigma β := +⟨⟦a⟧, f a⟩ + +protected theorem indep_coherent (f : Π a, β ⟦a⟧) + (h : ∀ (a b : α) (p : r a b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b) + : ∀ a b, r a b → quot.indep f a = quot.indep f b := +λ a b e, psigma.eq (sound e) (h a b e) + +protected theorem lift_indep_pr1 + (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b) + (q : quot r) : (lift (quot.indep f) (quot.indep_coherent f h) q).1 = q := +quot.ind (λ (a : α), eq.refl (quot.indep f a).1) q + +@[reducible, elab_as_eliminator] +protected def rec + (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b) + (q : quot r) : β q := +eq.rec_on (quot.lift_indep_pr1 f h q) ((lift (quot.indep f) (quot.indep_coherent f h) q).2) + +@[reducible, elab_as_eliminator] +protected def rec_on + (q : quot r) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b) : β q := +quot.rec f h q + +@[reducible, elab_as_eliminator] +protected def rec_on_subsingleton + [h : ∀ a, subsingleton (β ⟦a⟧)] (q : quot r) (f : Π a, β ⟦a⟧) : β q := +quot.rec f (λ a b h, subsingleton.elim _ (f b)) q + +@[reducible, elab_as_eliminator] +protected def hrec_on + (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 (calc + (eq.rec (f a) (sound p) : β ⟦b⟧) == f a : eq_rec_heq (sound p) (f a) + ... == f b : c a b p)) +end +end quot + +def quotient {α : Sort u} (s : setoid α) := +@quot α setoid.r + +namespace quotient + +protected def mk {α : Sort u} [s : setoid α] (a : α) : quotient s := +quot.mk setoid.r a + +notation `⟦`:max a `⟧`:0 := quotient.mk a + +def sound {α : Sort u} [s : setoid α] {a b : α} : a ≈ b → ⟦a⟧ = ⟦b⟧ := +quot.sound + +@[reducible, elab_as_eliminator] +protected def lift {α : Sort u} {β : Sort v} [s : setoid α] (f : α → β) : (∀ a b, a ≈ b → f a = f b) → quotient s → β := +quot.lift f + +@[elab_as_eliminator] +protected theorem ind {α : Sort u} [s : setoid α] {β : quotient s → Prop} : (∀ a, β ⟦a⟧) → ∀ q, β q := +quot.ind + +@[reducible, elab_as_eliminator] +protected def lift_on {α : Sort u} {β : Sort v} [s : setoid α] (q : quotient s) (f : α → β) (c : ∀ a b, a ≈ b → f a = f b) : β := +quot.lift_on q f c + +@[elab_as_eliminator] +protected theorem induction_on {α : Sort u} [s : setoid α] {β : quotient s → Prop} (q : quotient s) (h : ∀ a, β ⟦a⟧) : β q := +quot.induction_on q h + +theorem exists_rep {α : Sort u} [s : setoid α] (q : quotient s) : ∃ a : α, ⟦a⟧ = q := +quot.exists_rep q + +section +variable {α : Sort u} +variable [s : setoid α] +variable {β : quotient s → Sort v} + +protected def rec + (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (eq.rec (f a) (quotient.sound p) : β ⟦b⟧) = f b) + (q : quotient s) : β q := +quot.rec f h q + +@[reducible, elab_as_eliminator] +protected def rec_on + (q : quotient s) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (eq.rec (f a) (quotient.sound p) : β ⟦b⟧) = f b) : β q := +quot.rec_on q f h + +@[reducible, elab_as_eliminator] +protected def rec_on_subsingleton + [h : ∀ a, subsingleton (β ⟦a⟧)] (q : quotient s) (f : Π a, β ⟦a⟧) : β q := +@quot.rec_on_subsingleton _ _ _ h q f + +@[reducible, elab_as_eliminator] +protected def hrec_on + (q : quotient s) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : a ≈ b), f a == f b) : β q := +quot.hrec_on q f c +end + +section +universes u_a u_b u_c +variables {α : Sort u_a} {β : Sort u_b} {φ : Sort u_c} +variables [s₁ : setoid α] [s₂ : setoid β] +include s₁ s₂ + +@[reducible, elab_as_eliminator] +protected def lift₂ + (f : α → β → φ)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) + (q₁ : quotient s₁) (q₂ : quotient s₂) : φ := +quotient.lift + (λ (a₁ : α), quotient.lift (f a₁) (λ (a b : β), c a₁ a a₁ b (setoid.refl a₁)) q₂) + (λ (a b : α) (h : a ≈ b), + @quotient.ind β s₂ + (λ (a_1 : quotient s₂), + (quotient.lift (f a) (λ (a_1 b : β), c a a_1 a b (setoid.refl a)) a_1) + = + (quotient.lift (f b) (λ (a b_1 : β), c b a b b_1 (setoid.refl b)) a_1)) + (λ (a' : β), c a a' b a' h (setoid.refl a')) + q₂) + q₁ + +@[reducible, elab_as_eliminator] +protected def lift_on₂ + (q₁ : quotient s₁) (q₂ : quotient s₂) (f : α → β → φ) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : φ := +quotient.lift₂ f c q₁ q₂ + +@[elab_as_eliminator] +protected theorem ind₂ {φ : quotient s₁ → quotient s₂ → Prop} (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) (q₁ : quotient s₁) (q₂ : quotient s₂) : φ q₁ q₂ := +quotient.ind (λ a₁, quotient.ind (λ a₂, h a₁ a₂) q₂) q₁ + +@[elab_as_eliminator] +protected theorem induction_on₂ + {φ : quotient s₁ → quotient s₂ → Prop} (q₁ : quotient s₁) (q₂ : quotient s₂) (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂ := +quotient.ind (λ a₁, quotient.ind (λ a₂, h a₁ a₂) q₂) q₁ + +@[elab_as_eliminator] +protected theorem induction_on₃ + [s₃ : setoid φ] + {δ : quotient s₁ → quotient s₂ → quotient s₃ → Prop} (q₁ : quotient s₁) (q₂ : quotient s₂) (q₃ : quotient s₃) (h : ∀ a b c, δ ⟦a⟧ ⟦b⟧ ⟦c⟧) + : δ q₁ q₂ q₃ := +quotient.ind (λ a₁, quotient.ind (λ a₂, quotient.ind (λ a₃, h a₁ a₂ a₃) q₃) q₂) q₁ +end + +section exact +variable {α : Sort u} +variable [s : setoid α] +include s + +private def rel (q₁ q₂ : quotient s) : Prop := +quotient.lift_on₂ q₁ q₂ + (λ a₁ a₂, a₁ ≈ a₂) + (λ a₁ a₂ b₁ b₂ a₁b₁ a₂b₂, + propext (iff.intro + (λ a₁a₂, setoid.trans (setoid.symm a₁b₁) (setoid.trans a₁a₂ a₂b₂)) + (λ b₁b₂, setoid.trans a₁b₁ (setoid.trans b₁b₂ (setoid.symm a₂b₂))))) + +local infix `~` := rel + +private theorem rel.refl : ∀ q : quotient s, q ~ q := +λ q, quot.induction_on q (λ a, setoid.refl a) + +private theorem eq_imp_rel {q₁ q₂ : quotient s} : q₁ = q₂ → q₁ ~ q₂ := +assume h, eq.rec_on h (rel.refl q₁) + +theorem exact {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b := +assume h, eq_imp_rel h +end exact + +section +universes u_a u_b u_c +variables {α : Sort u_a} {β : Sort u_b} +variables [s₁ : setoid α] [s₂ : setoid β] +include s₁ s₂ + +@[reducible, elab_as_eliminator] +protected def rec_on_subsingleton₂ + {φ : quotient s₁ → quotient s₂ → Sort u_c} [h : ∀ a b, subsingleton (φ ⟦a⟧ ⟦b⟧)] + (q₁ : quotient s₁) (q₂ : quotient s₂) (f : Π a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂:= +@quotient.rec_on_subsingleton _ s₁ (λ q, φ q q₂) (λ a, quotient.ind (λ b, h a b) q₂) q₁ + (λ a, quotient.rec_on_subsingleton q₂ (λ b, f a b)) + +end +end quotient + +section +variable {α : Type u} +variable (r : α → α → Prop) + +inductive eqv_gen : α → α → Prop +| rel {} : Π x y, r x y → eqv_gen x y +| refl {} : Π x, eqv_gen x x +| symm {} : Π x y, eqv_gen x y → eqv_gen y x +| trans {} : Π x y z, eqv_gen x y → eqv_gen y z → eqv_gen x z + +theorem eqv_gen.is_equivalence : equivalence (@eqv_gen α r) := +mk_equivalence _ eqv_gen.refl eqv_gen.symm eqv_gen.trans + +def eqv_gen.setoid : setoid α := +setoid.mk _ (eqv_gen.is_equivalence r) + +theorem quot.exact {a b : α} (H : quot.mk r a = quot.mk r b) : eqv_gen r a b := +@quotient.exact _ (eqv_gen.setoid r) a b (@congr_arg _ _ _ _ + (quot.lift (@quotient.mk _ (eqv_gen.setoid r)) (λx y h, quot.sound (eqv_gen.rel x y h))) H) + +theorem quot.eqv_gen_sound {r : α → α → Prop} {a b : α} (H : eqv_gen r a b) : quot.mk r a = quot.mk r b := +eqv_gen.rec_on H + (λ x y h, quot.sound h) + (λ x, rfl) + (λ x y _ IH, eq.symm IH) + (λ x y z _ _ IH₁ IH₂, eq.trans IH₁ IH₂) +end + +instance {α : Sort u} {s : setoid α} [d : ∀ a b : α, decidable (a ≈ b)] : decidable_eq (quotient s) := +λ q₁ q₂ : quotient s, + quotient.rec_on_subsingleton₂ q₁ q₂ + (λ a₁ a₂, + match (d a₁ a₂) with + | (is_true h₁) := is_true (quotient.sound h₁) + | (is_false h₂) := is_false (λ h, absurd (quotient.exact h) h₂) + end) + +/- Function extensionality -/ + +namespace function +variables {α : Sort u} {β : α → Sort v} + +protected def equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x + +local infix `~` := function.equiv + +protected theorem equiv.refl (f : Π x : α, β x) : f ~ f := assume x, rfl + +protected theorem equiv.symm {f₁ f₂ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₁ := +λ h x, eq.symm (h x) + +protected theorem equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ := +λ h₁ h₂ x, eq.trans (h₁ x) (h₂ x) + +protected theorem equiv.is_equivalence (α : Sort u) (β : α → Sort v) : equivalence (@function.equiv α β) := +mk_equivalence (@function.equiv α β) (@equiv.refl α β) (@equiv.symm α β) (@equiv.trans α β) +end function + +section +open quotient +variables {α : Sort u} {β : α → Sort v} + +@[instance] +private def fun_setoid (α : Sort u) (β : α → Sort v) : setoid (Π x : α, β x) := +setoid.mk (@function.equiv α β) (function.equiv.is_equivalence α β) + +private def extfun (α : Sort u) (β : α → Sort v) : Sort (imax u v) := +quotient (fun_setoid α β) + +private def fun_to_extfun (f : Π x : α, β x) : extfun α β := +⟦f⟧ +private def extfun_app (f : extfun α β) : Π x : α, β x := +assume x, +quot.lift_on f + (λ f : Π x : α, β x, f x) + (λ f₁ f₂ h, h x) + +theorem funext {f₁ f₂ : Π x : α, β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := +show extfun_app ⟦f₁⟧ = extfun_app ⟦f₂⟧, from +congr_arg extfun_app (sound h) +end + +local infix `~` := function.equiv + +instance pi.subsingleton {α : Sort u} {β : α → Sort v} [∀ a, subsingleton (β a)] : subsingleton (Π a, β a) := +⟨λ f₁ f₂, funext (λ a, subsingleton.elim (f₁ a) (f₂ a))⟩ diff --git a/library/init/data/basic.lean b/library/init/data/basic.lean index 047f5c585f..9b47ca6cb7 100644 --- a/library/init/data/basic.lean +++ b/library/init/data/basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.data.quot init.data.nat.basic init.data.sum.basic +import init.data.nat.basic init.data.sum.basic import init.data.fin.basic init.data.list.basic init.data.char.basic import init.data.string.basic init.data.option.basic init.data.set import init.data.uint init.data.ordering.basic init.data.repr diff --git a/library/init/data/quot.lean b/library/init/data/quot.lean deleted file mode 100644 index ed951cebb0..0000000000 --- a/library/init/data/quot.lean +++ /dev/null @@ -1,268 +0,0 @@ -/- -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura - -Quotient types. --/ -prelude -/- We import propext here, otherwise we would need a quot.lift for propositions. -/ -import init.core - -universes u v - --- iff can now be used to do substitutions in a calculation -attribute [subst] -lemma iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b := -eq.subst (propext h₁) h₂ - -namespace quot -constant sound : Π {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b - -attribute [elab_as_eliminator] lift ind - -protected lemma lift_beta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀ a b, r a b → f a = f b) (a : α) : lift f c (quot.mk r a) = f a := -rfl - -protected lemma ind_beta {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} (p : ∀ a, β (quot.mk r a)) (a : α) : (ind p (quot.mk r a) : β (quot.mk r a)) = p a := -rfl - -attribute [reducible, elab_as_eliminator] -protected def lift_on {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : quot r) (f : α → β) (c : ∀ a b, r a b → f a = f b) : β := -lift f c q - -attribute [elab_as_eliminator] -protected lemma induction_on {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} (q : quot r) (h : ∀ a, β (quot.mk r a)) : β q := -ind h q - -lemma exists_rep {α : Sort u} {r : α → α → Prop} (q : quot r) : ∃ a : α, (quot.mk r a) = q := -quot.induction_on q (λ a, ⟨a, rfl⟩) - -section -variable {α : Sort u} -variable {r : α → α → Prop} -variable {β : quot r → Sort v} - -local notation `⟦`:max a `⟧` := quot.mk r a - -attribute [reducible] -protected def indep (f : Π a, β ⟦a⟧) (a : α) : psigma β := -⟨⟦a⟧, f a⟩ - -protected lemma indep_coherent (f : Π a, β ⟦a⟧) - (h : ∀ (a b : α) (p : r a b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b) - : ∀ a b, r a b → quot.indep f a = quot.indep f b := -λ a b e, psigma.eq (sound e) (h a b e) - -protected lemma lift_indep_pr1 - (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b) - (q : quot r) : (lift (quot.indep f) (quot.indep_coherent f h) q).1 = q := -quot.ind (λ (a : α), eq.refl (quot.indep f a).1) q - -attribute [reducible, elab_as_eliminator] -protected def rec - (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b) - (q : quot r) : β q := -eq.rec_on (quot.lift_indep_pr1 f h q) ((lift (quot.indep f) (quot.indep_coherent f h) q).2) - -attribute [reducible, elab_as_eliminator] -protected def rec_on - (q : quot r) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b) : β q := -quot.rec f h q - -attribute [reducible, elab_as_eliminator] -protected def rec_on_subsingleton - [h : ∀ a, subsingleton (β ⟦a⟧)] (q : quot r) (f : Π a, β ⟦a⟧) : β q := -quot.rec f (λ a b h, subsingleton.elim _ (f b)) q - -attribute [reducible, elab_as_eliminator] -protected def hrec_on - (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 (calc - (eq.rec (f a) (sound p) : β ⟦b⟧) == f a : eq_rec_heq (sound p) (f a) - ... == f b : c a b p)) -end -end quot - -def quotient {α : Sort u} (s : setoid α) := -@quot α setoid.r - -namespace quotient - -protected def mk {α : Sort u} [s : setoid α] (a : α) : quotient s := -quot.mk setoid.r a - -notation `⟦`:max a `⟧`:0 := quotient.mk a - -def sound {α : Sort u} [s : setoid α] {a b : α} : a ≈ b → ⟦a⟧ = ⟦b⟧ := -quot.sound - -attribute [reducible, elab_as_eliminator] -protected def lift {α : Sort u} {β : Sort v} [s : setoid α] (f : α → β) : (∀ a b, a ≈ b → f a = f b) → quotient s → β := -quot.lift f - -attribute [elab_as_eliminator] -protected lemma ind {α : Sort u} [s : setoid α] {β : quotient s → Prop} : (∀ a, β ⟦a⟧) → ∀ q, β q := -quot.ind - -attribute [reducible, elab_as_eliminator] -protected def lift_on {α : Sort u} {β : Sort v} [s : setoid α] (q : quotient s) (f : α → β) (c : ∀ a b, a ≈ b → f a = f b) : β := -quot.lift_on q f c - -attribute [elab_as_eliminator] -protected lemma induction_on {α : Sort u} [s : setoid α] {β : quotient s → Prop} (q : quotient s) (h : ∀ a, β ⟦a⟧) : β q := -quot.induction_on q h - -lemma exists_rep {α : Sort u} [s : setoid α] (q : quotient s) : ∃ a : α, ⟦a⟧ = q := -quot.exists_rep q - -section -variable {α : Sort u} -variable [s : setoid α] -variable {β : quotient s → Sort v} - -protected def rec - (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (eq.rec (f a) (quotient.sound p) : β ⟦b⟧) = f b) - (q : quotient s) : β q := -quot.rec f h q - -attribute [reducible, elab_as_eliminator] -protected def rec_on - (q : quotient s) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (eq.rec (f a) (quotient.sound p) : β ⟦b⟧) = f b) : β q := -quot.rec_on q f h - -attribute [reducible, elab_as_eliminator] -protected def rec_on_subsingleton - [h : ∀ a, subsingleton (β ⟦a⟧)] (q : quotient s) (f : Π a, β ⟦a⟧) : β q := -@quot.rec_on_subsingleton _ _ _ h q f - -attribute [reducible, elab_as_eliminator] -protected def hrec_on - (q : quotient s) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : a ≈ b), f a == f b) : β q := -quot.hrec_on q f c -end - -section -universes u_a u_b u_c -variables {α : Sort u_a} {β : Sort u_b} {φ : Sort u_c} -variables [s₁ : setoid α] [s₂ : setoid β] -include s₁ s₂ - -attribute [reducible, elab_as_eliminator] -protected def lift₂ - (f : α → β → φ)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) - (q₁ : quotient s₁) (q₂ : quotient s₂) : φ := -quotient.lift - (λ (a₁ : α), quotient.lift (f a₁) (λ (a b : β), c a₁ a a₁ b (setoid.refl a₁)) q₂) - (λ (a b : α) (h : a ≈ b), - @quotient.ind β s₂ - (λ (a_1 : quotient s₂), - (quotient.lift (f a) (λ (a_1 b : β), c a a_1 a b (setoid.refl a)) a_1) - = - (quotient.lift (f b) (λ (a b_1 : β), c b a b b_1 (setoid.refl b)) a_1)) - (λ (a' : β), c a a' b a' h (setoid.refl a')) - q₂) - q₁ - -attribute [reducible, elab_as_eliminator] -protected def lift_on₂ - (q₁ : quotient s₁) (q₂ : quotient s₂) (f : α → β → φ) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : φ := -quotient.lift₂ f c q₁ q₂ - -attribute [elab_as_eliminator] -protected lemma ind₂ {φ : quotient s₁ → quotient s₂ → Prop} (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) (q₁ : quotient s₁) (q₂ : quotient s₂) : φ q₁ q₂ := -quotient.ind (λ a₁, quotient.ind (λ a₂, h a₁ a₂) q₂) q₁ - -attribute [elab_as_eliminator] -protected lemma induction_on₂ - {φ : quotient s₁ → quotient s₂ → Prop} (q₁ : quotient s₁) (q₂ : quotient s₂) (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂ := -quotient.ind (λ a₁, quotient.ind (λ a₂, h a₁ a₂) q₂) q₁ - -attribute [elab_as_eliminator] -protected lemma induction_on₃ - [s₃ : setoid φ] - {δ : quotient s₁ → quotient s₂ → quotient s₃ → Prop} (q₁ : quotient s₁) (q₂ : quotient s₂) (q₃ : quotient s₃) (h : ∀ a b c, δ ⟦a⟧ ⟦b⟧ ⟦c⟧) - : δ q₁ q₂ q₃ := -quotient.ind (λ a₁, quotient.ind (λ a₂, quotient.ind (λ a₃, h a₁ a₂ a₃) q₃) q₂) q₁ -end - -section exact -variable {α : Sort u} -variable [s : setoid α] -include s - -private def rel (q₁ q₂ : quotient s) : Prop := -quotient.lift_on₂ q₁ q₂ - (λ a₁ a₂, a₁ ≈ a₂) - (λ a₁ a₂ b₁ b₂ a₁b₁ a₂b₂, - propext (iff.intro - (λ a₁a₂, setoid.trans (setoid.symm a₁b₁) (setoid.trans a₁a₂ a₂b₂)) - (λ b₁b₂, setoid.trans a₁b₁ (setoid.trans b₁b₂ (setoid.symm a₂b₂))))) - -local infix `~` := rel - -private lemma rel.refl : ∀ q : quotient s, q ~ q := -λ q, quot.induction_on q (λ a, setoid.refl a) - -private lemma eq_imp_rel {q₁ q₂ : quotient s} : q₁ = q₂ → q₁ ~ q₂ := -assume h, eq.rec_on h (rel.refl q₁) - -lemma exact {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b := -assume h, eq_imp_rel h -end exact - -section -universes u_a u_b u_c -variables {α : Sort u_a} {β : Sort u_b} -variables [s₁ : setoid α] [s₂ : setoid β] -include s₁ s₂ - -attribute [reducible, elab_as_eliminator] -protected def rec_on_subsingleton₂ - {φ : quotient s₁ → quotient s₂ → Sort u_c} [h : ∀ a b, subsingleton (φ ⟦a⟧ ⟦b⟧)] - (q₁ : quotient s₁) (q₂ : quotient s₂) (f : Π a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂:= -@quotient.rec_on_subsingleton _ s₁ (λ q, φ q q₂) (λ a, quotient.ind (λ b, h a b) q₂) q₁ - (λ a, quotient.rec_on_subsingleton q₂ (λ b, f a b)) - -end -end quotient - -section -variable {α : Type u} -variable (r : α → α → Prop) - -inductive eqv_gen : α → α → Prop -| rel {} : Π x y, r x y → eqv_gen x y -| refl {} : Π x, eqv_gen x x -| symm {} : Π x y, eqv_gen x y → eqv_gen y x -| trans {} : Π x y z, eqv_gen x y → eqv_gen y z → eqv_gen x z - -theorem eqv_gen.is_equivalence : equivalence (@eqv_gen α r) := -mk_equivalence _ eqv_gen.refl eqv_gen.symm eqv_gen.trans - -def eqv_gen.setoid : setoid α := -setoid.mk _ (eqv_gen.is_equivalence r) - -theorem quot.exact {a b : α} (H : quot.mk r a = quot.mk r b) : eqv_gen r a b := -@quotient.exact _ (eqv_gen.setoid r) a b (@congr_arg _ _ _ _ - (quot.lift (@quotient.mk _ (eqv_gen.setoid r)) (λx y h, quot.sound (eqv_gen.rel x y h))) H) - -theorem quot.eqv_gen_sound {r : α → α → Prop} {a b : α} (H : eqv_gen r a b) : quot.mk r a = quot.mk r b := -eqv_gen.rec_on H - (λ x y h, quot.sound h) - (λ x, rfl) - (λ x y _ IH, eq.symm IH) - (λ x y z _ _ IH₁ IH₂, eq.trans IH₁ IH₂) -end - - -open decidable -instance {α : Sort u} {s : setoid α} [d : ∀ a b : α, decidable (a ≈ b)] : decidable_eq (quotient s) := -λ q₁ q₂ : quotient s, - quotient.rec_on_subsingleton₂ q₁ q₂ - (λ a₁ a₂, - match (d a₁ a₂) with - | (is_true h₁) := is_true (quotient.sound h₁) - | (is_false h₂) := is_false (λ h, absurd (quotient.exact h) h₂) - end) diff --git a/library/init/default.lean b/library/init/default.lean index bb1e6ec7c8..5fa99018fe 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ prelude import init.core init.control init.data.basic init.version -import init.funext init.function init.classical +import init.function init.classical import init.util init.coe init.wf init.meta init.meta.well_founded_tactics init.data @[user_attribute] diff --git a/library/init/function.lean b/library/init/function.lean index c369fa4102..df5968b3cf 100644 --- a/library/init/function.lean +++ b/library/init/function.lean @@ -6,7 +6,7 @@ Author: Leonardo de Moura, Jeremy Avigad, Haitao Zhang General operations on functions. -/ prelude -import init.funext init.core +import init.core universes u₁ u₂ u₃ u₄ namespace function diff --git a/library/init/funext.lean b/library/init/funext.lean deleted file mode 100644 index 9fff18d76d..0000000000 --- a/library/init/funext.lean +++ /dev/null @@ -1,59 +0,0 @@ -/- -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Jeremy Avigad - -Extensional equality for functions, and a proof of function extensionality from quotients. --/ -prelude -import init.data.quot init.core - -universes u v - -namespace function -variables {α : Sort u} {β : α → Sort v} - -protected def equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x - -local infix `~` := function.equiv - -protected theorem equiv.refl (f : Π x : α, β x) : f ~ f := assume x, rfl - -protected theorem equiv.symm {f₁ f₂ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₁ := -λ h x, eq.symm (h x) - -protected theorem equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ := -λ h₁ h₂ x, eq.trans (h₁ x) (h₂ x) - -protected theorem equiv.is_equivalence (α : Sort u) (β : α → Sort v) : equivalence (@function.equiv α β) := -mk_equivalence (@function.equiv α β) (@equiv.refl α β) (@equiv.symm α β) (@equiv.trans α β) -end function - -section -open quotient -variables {α : Sort u} {β : α → Sort v} - -@[instance] -private def fun_setoid (α : Sort u) (β : α → Sort v) : setoid (Π x : α, β x) := -setoid.mk (@function.equiv α β) (function.equiv.is_equivalence α β) - -private def extfun (α : Sort u) (β : α → Sort v) : Sort (imax u v) := -quotient (fun_setoid α β) - -private def fun_to_extfun (f : Π x : α, β x) : extfun α β := -⟦f⟧ -private def extfun_app (f : extfun α β) : Π x : α, β x := -assume x, -quot.lift_on f - (λ f : Π x : α, β x, f x) - (λ f₁ f₂ h, h x) - -theorem funext {f₁ f₂ : Π x : α, β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := -show extfun_app ⟦f₁⟧ = extfun_app ⟦f₂⟧, from -congr_arg extfun_app (sound h) -end - -local infix `~` := function.equiv - -instance pi.subsingleton {α : Sort u} {β : α → Sort v} [∀ a, subsingleton (β a)] : subsingleton (Π a, β a) := -⟨λ f₁ f₂, funext (λ a, subsingleton.elim (f₁ a) (f₂ a))⟩