From 41bf46dbba2c1846ebcb9319f326170c41f17fd4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Jan 2017 12:38:13 -0800 Subject: [PATCH] chore(library/init): adjust Sort vs Type in definitions --- library/init/core.lean | 2 +- library/init/data/sigma/basic.lean | 3 +- library/init/function.lean | 60 ++++++++++++++------------ library/init/logic.lean | 2 +- tests/lean/anc1.lean | 2 +- tests/lean/anc1.lean.expected.out | 2 +- tests/lean/elab6.lean.expected.out | 4 +- tests/lean/notation4.lean | 2 +- tests/lean/notation4.lean.expected.out | 2 +- tests/lean/run/match_convoy.lean | 10 ++--- tests/lean/run/struct_value.lean | 8 ++-- 11 files changed, 52 insertions(+), 45 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 0417d95a79..9a1976abad 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -146,7 +146,7 @@ or.inl ha def or.intro_right (a : Prop) {b : Prop} (hb : b) : or a b := or.inr hb -structure sigma {α : Type u} (β : α → Sort v) := +structure sigma {α : Type u} (β : α → Type v) := mk :: (fst : α) (snd : β fst) structure psigma {α : Sort u} (β : α → Sort v) := diff --git a/library/init/data/sigma/basic.lean b/library/init/data/sigma/basic.lean index 98c3134a90..25b13475ca 100644 --- a/library/init/data/sigma/basic.lean +++ b/library/init/data/sigma/basic.lean @@ -7,10 +7,11 @@ prelude import init.logic init.wf notation `Σ` binders `, ` r:(scoped p, sigma p) := r +notation `Σ'` binders `, ` r:(scoped p, psigma p) := r universe variables u v -lemma ex_of_sig {α : Type u} {p : α → Prop} : (Σ x, p x) → ∃ x, p x +lemma ex_of_psig {α : Type u} {p : α → Prop} : (Σ' x, p x) → ∃ x, p x | ⟨x, hx⟩ := ⟨x, hx⟩ namespace sigma diff --git a/library/init/function.lean b/library/init/function.lean index 4d04c805cf..3e308852fe 100644 --- a/library/init/function.lean +++ b/library/init/function.lean @@ -7,22 +7,23 @@ General operations on functions. -/ prelude import init.data.prod init.funext init.logic -notation f ` $ `:1 a:0 := f a universe variables u₁ u₂ u₃ u₄ -variables {α : Type u₁} {β : Type u₂} {φ : Type u₃} {δ : Type u₄} {ζ : Type u₁} -@[inline, reducible] def function.comp (f : β → φ) (g : α → β) : α → φ := +namespace function +notation f ` $ `:1 a:0 := f a + +variables {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₁} + +@[inline, reducible] def comp (f : β → φ) (g : α → β) : α → φ := λ x, f (g x) -@[inline, reducible] def function.dcomp {β : α → Type u₂} {φ : Π {x : α}, β x → Type u₃} +@[inline, reducible] def dcomp {β : α → Sort u₂} {φ : Π {x : α}, β x → Sort u₃} (f : Π {x : α} (y : β x), φ y) (g : Π x, β x) : Π x, φ (g x) := λ x, f (g x) infixr ` ∘ ` := function.comp infixr ` ∘' `:80 := function.dcomp -namespace function - @[reducible] def comp_right (f : β → β → β) (g : α → β) : β → α → β := λ b a, f b (g a) @@ -36,27 +37,15 @@ namespace function : α → β → ζ := λ x y, op (f x y) (g x y) -@[reducible] def const (β : Type u₂) (a : α) : β → α := +@[reducible] def const (β : Sort u₂) (a : α) : β → α := λ x, a -@[reducible] def swap {φ : α → β → Type u₃} (f : Π x y, φ x y) : Π y x, φ x y := +@[reducible] def swap {φ : α → β → Sort u₃} (f : Π x y, φ x y) : Π y x, φ x y := λ y x, f x y -@[reducible] def app {β : α → Type u₂} (f : Π x, β x) (x : α) : β x := +@[reducible] def app {β : α → Sort u₂} (f : Π x, β x) (x : α) : β x := f x -@[reducible] def curry : (α × β → φ) → α → β → φ := -λ f a b, f (a, b) - -@[reducible] def uncurry : (α → β → φ) → α × β → φ := -λ f ⟨a, b⟩, f a b - -lemma curry_uncurry (f : α → β → φ) : curry (uncurry f) = f := -rfl - -lemma uncurry_curry (f : α × β → φ) : uncurry (curry f) = f := -funext (λ ⟨a, b⟩, rfl) - infixl ` on `:1 := on_fun notation f ` -[` op `]- ` g := combine f op g @@ -91,17 +80,11 @@ lemma bijective_comp {g : β → φ} {f : α → β} : bijective g → bijective -- g is a left inverse to f def left_inverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x -def id_of_left_inverse {g : β → α} {f : α → β} : left_inverse g f → g ∘ f = id := -assume h, funext h - def has_left_inverse (f : α → β) : Prop := ∃ finv : β → α, left_inverse finv f -- g is a right inverse to f def right_inverse (g : β → α) (f : α → β) : Prop := left_inverse f g -def id_of_right_inverse {g : β → α} {f : α → β} : right_inverse g f → f ∘ g = id := -assume h, funext h - def has_right_inverse (f : α → β) : Prop := ∃ finv : β → α, right_inverse finv f lemma injective_of_left_inverse {g : β → α} {f : α → β} : left_inverse g f → injective f := @@ -139,3 +122,26 @@ lemma surjective_id : surjective (@id α) := take a, ⟨a, rfl⟩ lemma bijective_id : bijective (@id α) := ⟨injective_id, surjective_id⟩ end function + +namespace function +variables {α : Type u₁} {β : Type u₂} {φ : Type u₃} + +@[reducible] def curry : (α × β → φ) → α → β → φ := +λ f a b, f (a, b) + +@[reducible] def uncurry : (α → β → φ) → α × β → φ := +λ f ⟨a, b⟩, f a b + +lemma curry_uncurry (f : α → β → φ) : curry (uncurry f) = f := +rfl + +lemma uncurry_curry (f : α × β → φ) : uncurry (curry f) = f := +funext (λ ⟨a, b⟩, rfl) + +def id_of_left_inverse {g : β → α} {f : α → β} : left_inverse g f → g ∘ f = id := +assume h, funext h + +def id_of_right_inverse {g : β → α} {f : α → β} : right_inverse g f → f ∘ g = id := +assume h, funext h + +end function diff --git a/library/init/logic.lean b/library/init/logic.lean index d0040eaa53..efc26b4c92 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -982,7 +982,7 @@ lemma let_eq {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β λ h₁ h₂, eq.rec_on h₁ (h₂ a₁) section relation -variables {α : Type u} {β : Type v} (r : β → β → Prop) +variables {α : Sort u} {β : Sort v} (r : β → β → Prop) local infix `≺`:50 := r def reflexive := ∀ x, x ≺ x diff --git a/tests/lean/anc1.lean b/tests/lean/anc1.lean index 581a45abff..079106b0e4 100644 --- a/tests/lean/anc1.lean +++ b/tests/lean/anc1.lean @@ -4,7 +4,7 @@ check (⟨trivial, trivial⟩ : true ∧ true) example : true := sorry -check (⟨1, sorry⟩ : Σ x : nat, x > 0) +check (⟨1, sorry⟩ : Σ' x : nat, x > 0) open tactic diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out index 5996d30e91..25736cd0da 100644 --- a/tests/lean/anc1.lean.expected.out +++ b/tests/lean/anc1.lean.expected.out @@ -1,6 +1,6 @@ (1, 2) : ℕ × ℕ and.intro trivial trivial : true ∧ true -sigma.mk 1 sorry : Σ (x : ℕ), x > 0 +psigma.mk 1 sorry : Σ' (x : ℕ), x > 0 show true, from true.intro : true Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from and.intro Hb Ha : diff --git a/tests/lean/elab6.lean.expected.out b/tests/lean/elab6.lean.expected.out index 754361f843..ff4b1ada64 100644 --- a/tests/lean/elab6.lean.expected.out +++ b/tests/lean/elab6.lean.expected.out @@ -1,9 +1,9 @@ -H : @transitive.{0} nat R +H : @transitive.{1} nat R @F.{u_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1 @F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃e : bool⦄, bool → bool → bool @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt : bool → bool @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt bool.tt : bool -H : @transitive.{0} nat R +H : @transitive.{1} nat R @F.{u_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1 @F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃e : bool⦄, bool → bool → bool @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt : bool → bool diff --git a/tests/lean/notation4.lean b/tests/lean/notation4.lean index 41c90e4df2..8362f6a440 100644 --- a/tests/lean/notation4.lean +++ b/tests/lean/notation4.lean @@ -3,5 +3,5 @@ open sigma inductive List (T : Type) : Type | nil {} : List | cons : T → List → List open List notation h :: t := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l check ∃ (A : Type) (x y : A), x = y check ∃ (x : num), x = 0 -check Σ (x : num), x = 10 +check Σ' (x : num), x = 10 check Σ (A : Type), List A diff --git a/tests/lean/notation4.lean.expected.out b/tests/lean/notation4.lean.expected.out index 503dc6ac0a..2605f98941 100644 --- a/tests/lean/notation4.lean.expected.out +++ b/tests/lean/notation4.lean.expected.out @@ -1,4 +1,4 @@ ∃ (A : Type) (x y : A), x = y : Prop ∃ (x : num), x = 0 : Prop -Σ (x : num), x = 10 : Type +Σ' (x : num), x = 10 : Type Σ (A : Type), List A : Type 1 diff --git a/tests/lean/run/match_convoy.lean b/tests/lean/run/match_convoy.lean index 4ffeb38ae0..03ba823406 100644 --- a/tests/lean/run/match_convoy.lean +++ b/tests/lean/run/match_convoy.lean @@ -53,19 +53,19 @@ quotient.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂, attribute [instance] noncomputable definition decidable_subbag2 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) := quotient.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂, - match sigma.mk (subcount l₁ l₂) rfl : (Σ (b : _), subcount l₁ l₂ = b) → _ with - | sigma.mk tt H := is_true (all_of_subcount_eq_tt H) - | sigma.mk ff H := is_false (λ h, + match psigma.mk (subcount l₁ l₂) rfl : (Σ' (b : _), subcount l₁ l₂ = b) → _ with + | psigma.mk tt H := is_true (all_of_subcount_eq_tt H) + | psigma.mk ff H := is_false (λ h, exists.elim (ex_of_subcount_eq_ff H) (λ w hw, absurd (h w) hw)) end) -local notation ⟦ a , b ⟧ := sigma.mk a b +local notation ⟦ a , b ⟧ := psigma.mk a b attribute [instance] noncomputable definition decidable_subbag3 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) := quotient.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂, - match ⟦subcount l₁ l₂, rfl⟧ : (Σ (b : _), subcount l₁ l₂ = b) → _ with + match ⟦subcount l₁ l₂, rfl⟧ : (Σ' (b : _), subcount l₁ l₂ = b) → _ with | ⟦tt, H⟧ := is_true (all_of_subcount_eq_tt H) | ⟦ff, H⟧ := is_false (λ h, exists.elim (ex_of_subcount_eq_ff H) diff --git a/tests/lean/run/struct_value.lean b/tests/lean/run/struct_value.lean index 2502a8f0bc..477a77ce4c 100644 --- a/tests/lean/run/struct_value.lean +++ b/tests/lean/run/struct_value.lean @@ -31,13 +31,13 @@ print p3 check { point3d . x := 1, y := 2, z := 3 } -check (⟨10, rfl⟩ : Σ x : nat, x = x) +check (⟨10, rfl⟩ : Σ' x : nat, x = x) -check ((| 10, rfl |) : Σ x : nat, x = x) +check ((| 10, rfl |) : Σ' x : nat, x = x) -check ({ fst := 10, snd := rfl } : Σ x : nat, x = x) +check ({ fst := 10, snd := rfl } : Σ' x : nat, x = x) -definition f (a : nat) : Σ x : nat, x = x := +definition f (a : nat) : Σ' x : nat, x = x := { fst := a, snd := rfl } print f