From bf9f7560f722661442ca625de84069dc8189b94b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 28 Jan 2017 20:56:28 -0800 Subject: [PATCH] feat(frontends/lean): (Type u) can't be a proposition (Type u) is the old (Type (u+1)) (PType u) is the old (Type u) Type* is the old (Type (_+1)) PType* is the old Type* The stdlib can be compiled, but we still have > 70 broken tests See discussion at #1341 --- library/init/category/combinators.lean | 8 +- library/init/cc_lemmas.lean | 10 +- library/init/classical.lean | 2 +- library/init/coe.lean | 52 ++--- library/init/core.lean | 50 +++-- library/init/data/nat/lemmas.lean | 4 +- library/init/data/option/basic.lean | 16 +- library/init/funext.lean | 2 +- library/init/logic.lean | 186 +++++++++--------- library/init/meta/format.lean | 2 +- library/init/meta/options.lean | 2 +- library/init/meta/rb_map.lean | 2 +- library/init/meta/rec_util.lean | 6 +- library/init/meta/tactic.lean | 6 +- library/init/meta/task.lean | 2 +- library/init/meta/vm.lean | 2 +- library/init/native/default.lean | 5 +- library/init/wf.lean | 4 +- library/library.md | 2 +- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_exprs.cpp | 36 +++- src/frontends/lean/builtin_exprs.h | 2 + src/frontends/lean/elaborator.cpp | 13 +- src/frontends/lean/elaborator.h | 1 + src/frontends/lean/parser.cpp | 6 +- src/frontends/lean/pp.cpp | 4 +- src/frontends/lean/token_table.cpp | 3 +- src/library/compiler/simp_pr1_rec.cpp | 10 +- src/library/constants.cpp | 64 ++++-- src/library/constants.h | 16 +- src/library/constants.txt | 16 +- src/library/constructions/brec_on.cpp | 20 +- .../equations_compiler/structural_rec.cpp | 12 +- src/library/inductive_compiler/basic.cpp | 2 +- src/library/inductive_compiler/mutual.cpp | 24 +-- src/library/tactic/ac_tactics.cpp | 8 +- src/library/type_context.cpp | 8 +- src/library/util.cpp | 47 ++--- src/library/util.h | 18 +- tests/lean/run/1163.lean | 2 +- tests/lean/run/1216.lean | 2 +- tests/lean/run/apply4.lean | 6 +- tests/lean/run/cases_tac1.lean | 2 +- tests/lean/run/coe_univ_bug.lean | 2 +- tests/lean/run/compiler_bug3.lean | 2 +- tests/lean/run/e1.lean | 4 +- tests/lean/run/e5.lean | 4 +- tests/lean/run/elab3.lean | 2 +- tests/lean/run/imp2.lean | 2 +- tests/lean/run/ind2.lean | 2 +- tests/lean/run/ind7.lean | 2 +- .../lean/run/inductive_nonrec_after_rec.lean | 2 +- tests/lean/run/match_expr.lean | 2 +- tests/lean/run/nested_inductive.lean | 10 +- tests/lean/run/noncomputable_example.lean | 4 +- tests/lean/run/offset1.lean | 2 +- tests/lean/run/pred_to_subtype_coercion.lean | 2 +- tests/lean/run/record9.lean | 6 +- tests/lean/run/simple.lean | 4 +- tests/lean/run/t9.lean | 2 +- 60 files changed, 438 insertions(+), 303 deletions(-) diff --git a/library/init/category/combinators.lean b/library/init/category/combinators.lean index 54d5137ace..29aa1334d2 100644 --- a/library/init/category/combinators.lean +++ b/library/init/category/combinators.lean @@ -10,9 +10,7 @@ import init.category.monad init.data.list.basic universe variables u v w namespace monad -/- Remark: we use (u+1) to make sure β is not a proposition. - That is, we are making sure that β and (list β) inhabit the same universe -/ -def mapm {m : Type (u+1) → Type v} [monad m] {α : Type w} {β : Type (u+1)} (f : α → m β) : list α → m (list β) +def mapm {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m (list β) | [] := return [] | (h :: t) := do h' ← f h, t' ← mapm t, return (h' :: t') @@ -20,13 +18,13 @@ def mapm' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (f : α → | [] := return () | (h :: t) := f h >> mapm' t -def for {m : Type (u+1) → Type v} [monad m] {α : Type w} {β : Type (u+1)} (l : list α) (f : α → m β) : m (list β) := +def for {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (l : list α) (f : α → m β) : m (list β) := mapm f l def for' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (l : list α) (f : α → m β) : m unit := mapm' f l -def sequence {m : Type (u+1) → Type v} [monad m] {α : Type (u+1)} : list (m α) → m (list α) +def sequence {m : Type u → Type v} [monad m] {α : Type u} : list (m α) → m (list α) | [] := return [] | (h :: t) := do h' ← h, t' ← sequence t, return (h' :: t') diff --git a/library/init/cc_lemmas.lean b/library/init/cc_lemmas.lean index 71cb72532b..3e34c94b3d 100644 --- a/library/init/cc_lemmas.lean +++ b/library/init/cc_lemmas.lean @@ -78,13 +78,13 @@ absurd (eq.mpr h this) this universe variables u -lemma if_eq_of_eq_true {c : Prop} [d : decidable c] {α : Type u} (t e : α) (h : c = true) : (@ite c d α t e) = t := +lemma if_eq_of_eq_true {c : Prop} [d : decidable c] {α : PType u} (t e : α) (h : c = true) : (@ite c d α t e) = t := if_pos (of_eq_true h) -lemma if_eq_of_eq_false {c : Prop} [d : decidable c] {α : Type u} (t e : α) (h : c = false) : (@ite c d α t e) = e := +lemma if_eq_of_eq_false {c : Prop} [d : decidable c] {α : PType u} (t e : α) (h : c = false) : (@ite c d α t e) = e := if_neg (not_of_eq_false h) -lemma if_eq_of_eq (c : Prop) [d : decidable c] {α : Type u} {t e : α} (h : t = e) : (@ite c d α t e) = t := +lemma if_eq_of_eq (c : Prop) [d : decidable c] {α : PType u} {t e : α} (h : t = e) : (@ite c d α t e) = t := match d with | (is_true hc) := rfl | (is_false hnc) := eq.symm h @@ -110,8 +110,8 @@ eq_false_intro (λ ha, absurd ha (eq.mpr h trivial)) lemma eq_true_of_not_eq_false {a : Prop} (h : (not a) = false) : a = true := eq_true_intro (classical.by_contradiction (λ hna, eq.mp h hna)) -lemma ne_of_eq_of_ne {α : Type u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c := +lemma ne_of_eq_of_ne {α : PType u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c := h₁^.symm ▸ h₂ -lemma ne_of_ne_of_eq {α : Type u} {a b c : α} (h₁ : a ≠ b) (h₂ : b = c) : a ≠ c := +lemma ne_of_ne_of_eq {α : PType u} {a b c : α} (h₁ : a ≠ b) (h₂ : b = c) : a ≠ c := h₂ ▸ h₁ diff --git a/library/init/classical.lean b/library/init/classical.lean index 60e4055280..b32412fbbe 100644 --- a/library/init/classical.lean +++ b/library/init/classical.lean @@ -175,7 +175,7 @@ local attribute [instance] prop_decidable noncomputable def type_decidable_eq (a : Type u) : decidable_eq a := λ x y, prop_decidable (x = y) -noncomputable def type_decidable (a : Type u) : sum a (a → false) := +noncomputable def type_decidable (a : Type u) : sum a (a → empty) := match (prop_decidable (nonempty a)) with | (is_true hp) := sum.inl (@inhabited.default _ (inhabited_of_nonempty hp)) | (is_false hn) := sum.inr (λ a, absurd (nonempty.intro a) hn) diff --git a/library/init/coe.lean b/library/init/coe.lean index 53c67b496b..a86212745f 100644 --- a/library/init/coe.lean +++ b/library/init/coe.lean @@ -27,50 +27,50 @@ prelude import init.data.list.basic init.data.subtype.basic init.data.prod universe variables u v -class has_lift (a : Type u) (b : Type v) := +class has_lift (a : PType u) (b : PType v) := (lift : a → b) /- auxiliary class that contains the transitive closure of has_lift. -/ -class has_lift_t (a : Type u) (b : Type v) := +class has_lift_t (a : PType u) (b : PType v) := (lift : a → b) -class has_coe (a : Type u) (b : Type v) := +class has_coe (a : PType u) (b : PType v) := (coe : a → b) /- auxiliary class that contains the transitive closure of has_coe. -/ -class has_coe_t (a : Type u) (b : Type v) := +class has_coe_t (a : PType u) (b : PType v) := (coe : a → b) -class has_coe_to_fun (a : Type u) : Type (max u (v+1)) := -(F : a → Type v) (coe : Π x, F x) +class has_coe_to_fun (a : PType u) : PType (max u (v+1)) := +(F : a → PType v) (coe : Π x, F x) -class has_coe_to_sort (a : Type u) : Type (max u (v+1)) := -(S : Type v) (coe : a → S) +class has_coe_to_sort (a : PType u) : Type (max u (v+1)) := +(S : PType v) (coe : a → S) -def lift {a : Type u} {b : Type v} [has_lift a b] : a → b := +def lift {a : PType u} {b : PType v} [has_lift a b] : a → b := @has_lift.lift a b _ -def lift_t {a : Type u} {b : Type v} [has_lift_t a b] : a → b := +def lift_t {a : PType u} {b : PType v} [has_lift_t a b] : a → b := @has_lift_t.lift a b _ -def coe_b {a : Type u} {b : Type v} [has_coe a b] : a → b := +def coe_b {a : PType u} {b : PType v} [has_coe a b] : a → b := @has_coe.coe a b _ -def coe_t {a : Type u} {b : Type v} [has_coe_t a b] : a → b := +def coe_t {a : PType u} {b : PType v} [has_coe_t a b] : a → b := @has_coe_t.coe a b _ -def coe_fn_b {a : Type u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x := +def coe_fn_b {a : PType u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x := has_coe_to_fun.coe /- User level coercion operators -/ -@[reducible] def coe {a : Type u} {b : Type v} [has_lift_t a b] : a → b := +@[reducible] def coe {a : PType u} {b : PType v} [has_lift_t a b] : a → b := lift_t -@[reducible] def coe_fn {a : Type u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x := +@[reducible] def coe_fn {a : PType u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x := has_coe_to_fun.coe -@[reducible] def coe_sort {a : Type u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a := +@[reducible] def coe_sort {a : PType u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a := has_coe_to_sort.coe /- Notation -/ @@ -85,29 +85,29 @@ universe variables u₁ u₂ u₃ /- Transitive closure for has_lift, has_coe, has_coe_to_fun -/ -instance lift_trans {a : Type u₁} {b : Type u₂} {c : Type u₃} [has_lift a b] [has_lift_t b c] : has_lift_t a c := +instance lift_trans {a : PType u₁} {b : PType u₂} {c : PType u₃} [has_lift a b] [has_lift_t b c] : has_lift_t a c := ⟨λ x, lift_t (lift x : b)⟩ -instance lift_base {a : Type u} {b : Type v} [has_lift a b] : has_lift_t a b := +instance lift_base {a : PType u} {b : PType v} [has_lift a b] : has_lift_t a b := ⟨lift⟩ -instance coe_trans {a : Type u₁} {b : Type u₂} {c : Type u₃} [has_coe a b] [has_coe_t b c] : has_coe_t a c := +instance coe_trans {a : PType u₁} {b : PType u₂} {c : PType u₃} [has_coe a b] [has_coe_t b c] : has_coe_t a c := ⟨λ x, coe_t (coe_b x : b)⟩ -instance coe_base {a : Type u} {b : Type v} [has_coe a b] : has_coe_t a b := +instance coe_base {a : PType u} {b : PType v} [has_coe a b] : has_coe_t a b := ⟨coe_b⟩ -instance coe_fn_trans {a : Type u₁} {b : Type u₂} [has_lift_t a b] [has_coe_to_fun.{u₂ u₃} b] : has_coe_to_fun.{u₁ u₃} a := +instance coe_fn_trans {a : PType u₁} {b : PType u₂} [has_lift_t a b] [has_coe_to_fun.{u₂ u₃} b] : has_coe_to_fun.{u₁ u₃} a := { F := λ x, @has_coe_to_fun.F.{u₂ u₃} b _ (coe x), coe := λ x, coe_fn (coe x) } -instance coe_sort_trans {a : Type u₁} {b : Type u₂} [has_lift_t a b] [has_coe_to_sort.{u₂ u₃} b] : has_coe_to_sort.{u₁ u₃} a := +instance coe_sort_trans {a : PType u₁} {b : PType u₂} [has_lift_t a b] [has_coe_to_sort.{u₂ u₃} b] : has_coe_to_sort.{u₁ u₃} a := { S := has_coe_to_sort.S.{u₂ u₃} b, coe := λ x, coe_sort (coe x) } /- Every coercion is also a lift -/ -instance coe_to_lift {a : Type u} {b : Type v} [has_coe_t a b] : has_lift_t a b := +instance coe_to_lift {a : PType u} {b : PType v} [has_coe_t a b] : has_lift_t a b := ⟨coe_t⟩ /- basic coercions -/ @@ -127,13 +127,13 @@ universe variables ua ua₁ ua₂ ub ub₁ ub₂ /- Remark: we cant use [has_lift_t a₂ a₁] since it will produce non-termination whenever a type class resolution problem does not have a solution. -/ -instance lift_fn {a₁ : Type ua₁} {a₂ : Type ua₂} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift a₂ a₁] [has_lift_t b₁ b₂] : has_lift (a₁ → b₁) (a₂ → b₂) := +instance lift_fn {a₁ : PType ua₁} {a₂ : PType ua₂} {b₁ : PType ub₁} {b₂ : PType ub₂} [has_lift a₂ a₁] [has_lift_t b₁ b₂] : has_lift (a₁ → b₁) (a₂ → b₂) := ⟨λ f x, ↑(f ↑x)⟩ -instance lift_fn_range {a : Type ua} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift_t b₁ b₂] : has_lift (a → b₁) (a → b₂) := +instance lift_fn_range {a : PType ua} {b₁ : PType ub₁} {b₂ : PType ub₂} [has_lift_t b₁ b₂] : has_lift (a → b₁) (a → b₂) := ⟨λ f x, ↑(f x)⟩ -instance lift_fn_dom {a₁ : Type ua₁} {a₂ : Type ua₂} {b : Type ub} [has_lift a₂ a₁] : has_lift (a₁ → b) (a₂ → b) := +instance lift_fn_dom {a₁ : PType ua₁} {a₂ : PType ua₂} {b : PType ub} [has_lift a₂ a₁] : has_lift (a₁ → b) (a₂ → b) := ⟨λ f x, f ↑x⟩ instance lift_pair {a₁ : Type ua₁} {a₂ : Type ub₂} {b₁ : Type ub₁} {b₂ : Type ub₂} [has_lift_t a₁ a₂] [has_lift_t b₁ b₂] : has_lift (a₁ × b₁) (a₂ × b₂) := diff --git a/library/init/core.lean b/library/init/core.lean index 0315eb2c1e..5c754166c4 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -7,9 +7,9 @@ notation, basic datatypes and type classes -/ prelude -notation `Prop` := Type 0 -notation `Type₂` := Type 2 -notation `Type₃` := Type 3 +notation `Prop` := PType 0 +notation `Type₂` := PType 2 +notation `Type₃` := PType 3 /- Logical operations and relations -/ @@ -82,10 +82,10 @@ reserve infixl `; `:1 universe variables u v /- gadget for optional parameter support -/ -@[reducible] def opt_param (α : Type u) (default : α) : Type u := +@[reducible] def opt_param (α : PType u) (default : α) : PType u := α -inductive poly_unit : Type u +inductive poly_unit : PType u | star : poly_unit inductive unit : Type @@ -101,17 +101,22 @@ inductive empty : Type def not (a : Prop) := a → false prefix `¬` := not -inductive eq {α : Type u} (a : α) : α → Prop +inductive eq {α : PType u} (a : α) : α → Prop | refl : eq a init_quotient -inductive heq {α : Type u} (a : α) : Π {β : Type u}, β → Prop +inductive heq {α : PType u} (a : α) : Π {β : PType u}, β → Prop | refl : heq a structure prod (α : Type u) (β : Type v) := (fst : α) (snd : β) +/- Similar to prod, but α and β can be propositions. + We use this type internally to automatically generate the brec_on recursor. -/ +structure pprod (α : PType u) (β : PType v) := +(fst : α) (snd : β) + inductive and (a b : Prop) : Prop | intro : a → b → and @@ -129,6 +134,10 @@ inductive sum (α : Type u) (β : Type v) | inl {} : α → sum | inr {} : β → sum +inductive psum (α : PType u) (β : PType v) +| inl {} : α → psum +| inr {} : β → psum + inductive or (a b : Prop) : Prop | inl {} : a → or | inr {} : b → or @@ -139,7 +148,10 @@ or.inl ha def or.intro_right (a : Prop) {b : Prop} (hb : b) : or a b := or.inr hb -structure sigma {α : Type u} (β : α → Type v) := +structure sigma {α : Type u} (β : α → PType v) := +mk :: (fst : α) (snd : β fst) + +structure psigma {α : PType u} (β : α → PType v) := mk :: (fst : α) (snd : β fst) inductive pos_num : Type @@ -174,15 +186,15 @@ class inductive decidable (p : Prop) | is_true : p → decidable @[reducible] -def decidable_pred {α : Type u} (r : α → Prop) := +def decidable_pred {α : PType u} (r : α → Prop) := Π (a : α), decidable (r a) @[reducible] -def decidable_rel {α : Type u} (r : α → α → Prop) := +def decidable_rel {α : PType u} (r : α → α → Prop) := Π (a b : α), decidable (r a b) @[reducible] -def decidable_eq (α : Type u) := +def decidable_eq (α : PType u) := decidable_rel (@eq α) inductive option (α : Type u) @@ -428,26 +440,26 @@ notation `(` h `, ` t:(foldr `, ` (e r, prod.mk e r)) `)` := prod.mk h t attribute [refl] eq.refl -@[pattern] def rfl {α : Type u} {a : α} : a = a := eq.refl a +@[pattern] def rfl {α : PType u} {a : α} : a = a := eq.refl a @[elab_as_eliminator, subst] -lemma eq.subst {α : Type u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b := +lemma eq.subst {α : PType u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b := eq.rec h₂ h₁ notation h1 ▸ h2 := eq.subst h1 h2 -@[trans] lemma eq.trans {α : Type u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c := +@[trans] lemma eq.trans {α : PType u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c := h₂ ▸ h₁ -@[symm] lemma eq.symm {α : Type u} {a b : α} (h : a = b) : b = a := +@[symm] lemma eq.symm {α : PType u} {a b : α} (h : a = b) : b = a := h ▸ rfl /- sizeof -/ -class has_sizeof (α : Type u) := +class has_sizeof (α : PType u) := (sizeof : α → nat) -def sizeof {α : Type u} [s : has_sizeof α] : α → nat := +def sizeof {α : PType u} [s : has_sizeof α] : α → nat := has_sizeof.sizeof /- @@ -456,13 +468,13 @@ From now on, the inductive compiler will automatically generate sizeof instances -/ /- Every type `α` has a default has_sizeof instance that just returns 0 for every element of `α` -/ -instance default_has_sizeof (α : Type u) : has_sizeof α := +instance default_has_sizeof (α : PType u) : has_sizeof α := ⟨λ a, nat.zero⟩ /- TODO(Leo): the [simp.sizeof] annotations are not really necessary. What we need is a robust way of unfolding sizeof definitions. -/ attribute [simp.sizeof] -lemma default_has_sizeof_eq (α : Type u) (a : α) : @sizeof α (default_has_sizeof α) a = 0 := +lemma default_has_sizeof_eq (α : PType u) (a : α) : @sizeof α (default_has_sizeof α) a = 0 := rfl instance : has_sizeof nat := diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index f37423ded2..98f54cf545 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -259,10 +259,10 @@ protected lemma lt_or_ge : ∀ (a b : ℕ), a < b ∨ a ≥ b end end -protected def {u} lt_ge_by_cases {a b : ℕ} {C : Type u} (h₁ : a < b → C) (h₂ : a ≥ b → C) : C := +protected def {u} lt_ge_by_cases {a b : ℕ} {C : PType u} (h₁ : a < b → C) (h₂ : a ≥ b → C) : C := decidable.by_cases h₁ (λ h, h₂ (or.elim (nat.lt_or_ge a b) (λ a, absurd a h) (λ a, a))) -protected def {u} lt_by_cases {a b : ℕ} {C : Type u} (h₁ : a < b → C) (h₂ : a = b → C) +protected def {u} lt_by_cases {a b : ℕ} {C : PType u} (h₁ : a < b → C) (h₂ : a = b → C) (h₃ : b < a → C) : C := nat.lt_ge_by_cases h₁ (λ h₁, nat.lt_ge_by_cases h₃ (λ h, h₂ (nat.le_antisymm h h₁))) diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean index a483a19fb0..54db24c5eb 100644 --- a/library/init/data/option/basic.lean +++ b/library/init/data/option/basic.lean @@ -57,10 +57,10 @@ def option_orelse {α : Type u} : option α → option α → option α instance {α : Type u} : alternative option := alternative.mk @option_fmap @some (@fapp _ _) @none @option_orelse -def option_t (m : Type (max 1 u) → Type v) [monad m] (α : Type u) : Type v := +def option_t (m : Type u → Type v) [monad m] (α : Type u) : Type v := m (option α) -@[inline] def option_t_fmap {m : Type (max 1 u) → Type v} [monad m] {α β : Type u} (f : α → β) (e : option_t m α) : option_t m β := +@[inline] def option_t_fmap {m : Type u → Type v} [monad m] {α β : Type u} (f : α → β) (e : option_t m α) : option_t m β := show m (option β), from do o ← e, match o with @@ -68,7 +68,7 @@ do o ← e, | (some a) := return (some (f a)) end -@[inline] def option_t_bind {m : Type (max 1 u) → Type v} [monad m] {α β : Type u} (a : option_t m α) (b : α → option_t m β) +@[inline] def option_t_bind {m : Type u → Type v} [monad m] {α β : Type u} (a : option_t m α) (b : α → option_t m β) : option_t m β := show m (option β), from do o ← a, @@ -77,14 +77,14 @@ do o ← a, | (some a) := b a end -@[inline] def option_t_return {m : Type (max 1 u) → Type v} [monad m] {α : Type u} (a : α) : option_t m α := +@[inline] def option_t_return {m : Type u → Type v} [monad m] {α : Type u} (a : α) : option_t m α := show m (option α), from return (some a) -instance {m : Type (max 1 u) → Type v} [monad m] : monad (option_t m) := +instance {m : Type u → Type v} [monad m] : monad (option_t m) := {map := @option_t_fmap m _, ret := @option_t_return m _, bind := @option_t_bind m _} -def option_t_orelse {m : Type (max 1 u) → Type v} [monad m] {α : Type u} (a : option_t m α) (b : option_t m α) : option_t m α := +def option_t_orelse {m : Type u → Type v} [monad m] {α : Type u} (a : option_t m α) (b : option_t m α) : option_t m α := show m (option α), from do o ← a, match o with @@ -92,11 +92,11 @@ do o ← a, | (some v) := return (some v) end -def option_t_fail {m : Type (max 1 u) → Type v} [monad m] {α : Type u} : option_t m α := +def option_t_fail {m : Type u → Type v} [monad m] {α : Type u} : option_t m α := show m (option α), from return none -instance {m : Type (max 1 u) → Type v} [monad m] : alternative (option_t m) := +instance {m : Type u → Type v} [monad m] : alternative (option_t m) := {map := @option_t_fmap m _, pure := @option_t_return m _, seq := @fapp (option_t m) (@option_t.monad m _), diff --git a/library/init/funext.lean b/library/init/funext.lean index 268792e018..a83cf2f5fc 100644 --- a/library/init/funext.lean +++ b/library/init/funext.lean @@ -37,7 +37,7 @@ variables {α : Type u} {β : α → Type v} private def fun_setoid (α : Type u) (β : α → Type v) : setoid (Π x : α, β x) := setoid.mk (@function.equiv α β) (function.equiv.is_equivalence α β) -private def extfun (α : Type u) (β : α → Type v) : Type (imax u v) := +private def extfun (α : Type u) (β : α → Type v) : Type (max u v) := quotient (fun_setoid α β) private def fun_to_extfun (f : Π x : α, β x) : extfun α β := diff --git a/library/init/logic.lean b/library/init/logic.lean index 5665d6ffe6..1df3c97efe 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -8,9 +8,9 @@ import init.core universe variables u v w -@[reducible] def id {α : Type u} (a : α) : α := a +@[reducible] def id {α : PType u} (a : α) : α := a -def flip {α : Type u} {β : Type v} {φ : Type w} (f : α → β → φ) : β → α → φ := +def flip {α : PType u} {β : PType v} {φ : PType w} (f : α → β → φ) : β → α → φ := λ b a, f a b /- implication -/ @@ -22,7 +22,7 @@ assume hp, h₂ (h₁ hp) def trivial : true := ⟨⟩ -@[inline] def absurd {a : Prop} {b : Type v} (h₁ : a) (h₂ : ¬a) : b := +@[inline] def absurd {a : Prop} {b : PType v} (h₁ : a) (h₂ : ¬a) : b := false.rec b (h₂ h₁) lemma not.intro {a : Prop} (h : a → false) : ¬ a := @@ -54,39 +54,39 @@ false.rec c h lemma proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl -@[simp] lemma id.def {α : Type u} (a : α) : id a = a := rfl +@[simp] lemma id.def {α : PType u} (a : α) : id a = a := rfl -- Remark: we provide the universe levels explicitly to make sure `eq.drec` has the same type of `eq.rec` in the hoTT library attribute [elab_as_eliminator] -protected lemma {u₁ u₂} eq.drec {α : Type u₂} {a : α} {φ : Π (x : α), a = x → Type u₁} (h₁ : φ a (eq.refl a)) {b : α} (h₂ : a = b) : φ b h₂ := +protected lemma {u₁ u₂} eq.drec {α : PType u₂} {a : α} {φ : Π (x : α), a = x → PType u₁} (h₁ : φ a (eq.refl a)) {b : α} (h₂ : a = b) : φ b h₂ := eq.rec (λ h₂ : a = a, show φ a h₂, from h₁) h₂ h₂ attribute [elab_as_eliminator] -protected lemma drec_on {α : Type u} {a : α} {φ : Π (x : α), a = x → Type v} {b : α} (h₂ : a = b) (h₁ : φ a (eq.refl a)) : φ b h₂ := +protected lemma drec_on {α : PType u} {a : α} {φ : Π (x : α), a = x → PType v} {b : α} (h₂ : a = b) (h₁ : φ a (eq.refl a)) : φ b h₂ := eq.drec h₁ h₂ -lemma eq.mp {α β : Type u} : (α = β) → α → β := +lemma eq.mp {α β : PType u} : (α = β) → α → β := eq.rec_on -lemma eq.mpr {α β : Type u} : (α = β) → β → α := +lemma eq.mpr {α β : PType u} : (α = β) → β → α := λ h₁ h₂, eq.rec_on (eq.symm h₁) h₂ -lemma eq.substr {α : Type u} {p : α → Prop} {a b : α} (h₁ : b = a) : p a → p b := +lemma eq.substr {α : PType u} {p : α → Prop} {a b : α} (h₁ : b = a) : p a → p b := eq.subst (eq.symm h₁) -lemma congr {α : Type u} {β : Type v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ := +lemma congr {α : PType u} {β : PType v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ := eq.subst h₁ (eq.subst h₂ rfl) -lemma congr_fun {α : Type u} {β : α → Type v} {f g : Π x, β x} (h : f = g) (a : α) : f a = g a := +lemma congr_fun {α : PType u} {β : α → PType v} {f g : Π x, β x} (h : f = g) (a : α) : f a = g a := eq.subst h (eq.refl (f a)) -lemma congr_arg {α : Type u} {β : Type v} {a₁ a₂ : α} (f : α → β) : a₁ = a₂ → f a₁ = f a₂ := +lemma congr_arg {α : PType u} {β : PType v} {a₁ a₂ : α} (f : α → β) : a₁ = a₂ → f a₁ = f a₂ := congr rfl -lemma trans_rel_left {α : Type u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c := +lemma trans_rel_left {α : PType u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c := h₂ ▸ h₁ -lemma trans_rel_right {α : Type u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c := +lemma trans_rel_right {α : PType u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c := h₁^.symm ▸ h₂ lemma of_eq_true {p : Prop} (h : p = true) : p := @@ -95,25 +95,25 @@ h^.symm ▸ trivial lemma not_of_eq_false {p : Prop} (h : p = false) : ¬p := assume hp, h ▸ hp -@[inline] def cast {α β : Type u} (h : α = β) (a : α) : β := +@[inline] def cast {α β : PType u} (h : α = β) (a : α) : β := eq.rec a h -lemma cast_proof_irrel {α β : Type u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a := +lemma cast_proof_irrel {α β : PType u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a := rfl -lemma cast_eq {α : Type u} (h : α = α) (a : α) : cast h a = a := +lemma cast_eq {α : PType u} (h : α = α) (a : α) : cast h a = a := rfl /- ne -/ -@[reducible] def ne {α : Type u} (a b : α) := ¬(a = b) +@[reducible] def ne {α : PType u} (a b : α) := ¬(a = b) notation a ≠ b := ne a b -@[simp] lemma ne.def {α : Type u} (a b : α) : a ≠ b = ¬ (a = b) := +@[simp] lemma ne.def {α : PType u} (a b : α) : a ≠ b = ¬ (a = b) := rfl namespace ne - variable {α : Type u} + variable {α : PType u} variables {a b : α} lemma intro (h : a = b → false) : a ≠ b := h @@ -126,7 +126,7 @@ namespace ne assume (h₁ : b = a), h (h₁^.symm) end ne -lemma false_of_ne {α : Type u} {a : α} : a ≠ a → false := ne.irrefl +lemma false_of_ne {α : PType u} {a : α} : a ≠ a → false := ne.irrefl section variables {p : Prop} @@ -144,18 +144,18 @@ end attribute [refl] heq.refl section -variables {α β φ : Type u} {a a' : α} {b b' : β} {c : φ} +variables {α β φ : PType u} {a a' : α} {b b' : β} {c : φ} lemma eq_of_heq (h : a == a') : a = a' := -have ∀ (α' : Type u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from - λ (α' : Type u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl), +have ∀ (α' : PType u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from + λ (α' : PType u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl), show (eq.rec_on (eq.refl α) a : α) = a', from this α a' h (eq.refl α) -lemma heq.elim {α : Type u} {a : α} {p : α → Type v} {b : α} (h₁ : a == b) +lemma heq.elim {α : PType u} {a : α} {p : α → PType v} {b : α} (h₁ : a == b) : p a → p b := eq.rec_on (eq_of_heq h₁) -lemma heq.subst {p : ∀ T : Type u, T → Prop} : a == b → p α a → p β b := +lemma heq.subst {p : ∀ T : PType u, T → Prop} : a == b → p α a → p β b := heq.rec_on @[symm] lemma heq.symm (h : a == b) : b == a := @@ -177,13 +177,13 @@ def type_eq_of_heq (h : a == b) : α = β := heq.rec_on h (eq.refl α) end -lemma eq_rec_heq {α : Type u} {φ : α → Type v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') == p +lemma eq_rec_heq {α : Type u} {φ : α → PType v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') == p | a .a rfl p := heq.refl p -lemma heq_of_eq_rec_left {α : Type u} {φ : α → Type v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : φ a') = p₂), p₁ == p₂ +lemma heq_of_eq_rec_left {α : PType u} {φ : α → PType v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : φ a') = p₂), p₁ == p₂ | a .a p₁ p₂ (eq.refl .a) h := eq.rec_on h (heq.refl p₁) -lemma heq_of_eq_rec_right {α : Type u} {φ : α → Type v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂ +lemma heq_of_eq_rec_right {α : PType u} {φ : α → PType v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂ | a .a p₁ p₂ (eq.refl .a) h := have p₁ = p₂, from h, this ▸ heq.refl p₁ @@ -191,19 +191,19 @@ lemma heq_of_eq_rec_right {α : Type u} {φ : α → Type v} : ∀ {a a' : α} { lemma of_heq_true {a : Prop} (h : a == true) : a := of_eq_true (eq_of_heq h) -lemma eq_rec_compose : ∀ {α β φ : Type u} (p₁ : β = φ) (p₂ : α = β) (a : α), (eq.rec_on p₁ (eq.rec_on p₂ a : β) : φ) = eq.rec_on (eq.trans p₂ p₁) a +lemma eq_rec_compose : ∀ {α β φ : PType u} (p₁ : β = φ) (p₂ : α = β) (a : α), (eq.rec_on p₁ (eq.rec_on p₂ a : β) : φ) = eq.rec_on (eq.trans p₂ p₁) a | α .α .α (eq.refl .α) (eq.refl .α) a := rfl -lemma eq_rec_eq_eq_rec : ∀ {α₁ α₂ : Type u} {p : α₁ = α₂} {a₁ : α₁} {a₂ : α₂}, (eq.rec_on p a₁ : α₂) = a₂ → a₁ = eq.rec_on (eq.symm p) a₂ +lemma eq_rec_eq_eq_rec : ∀ {α₁ α₂ : PType u} {p : α₁ = α₂} {a₁ : α₁} {a₂ : α₂}, (eq.rec_on p a₁ : α₂) = a₂ → a₁ = eq.rec_on (eq.symm p) a₂ | α .α rfl a .a rfl := rfl -lemma eq_rec_of_heq_left : ∀ {α₁ α₂ : Type u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂), (eq.rec_on (type_eq_of_heq h) a₁ : α₂) = a₂ +lemma eq_rec_of_heq_left : ∀ {α₁ α₂ : PType u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂), (eq.rec_on (type_eq_of_heq h) a₁ : α₂) = a₂ | α .α a .a (heq.refl .a) := rfl -lemma eq_rec_of_heq_right {α₁ α₂ : Type u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ := +lemma eq_rec_of_heq_right {α₁ α₂ : PType u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ := eq_rec_eq_eq_rec (eq_rec_of_heq_left h) -lemma cast_heq : ∀ {α β : Type u} (h : α = β) (a : α), cast h a == a +lemma cast_heq : ∀ {α β : PType u} (h : α = β) (a : α), cast h a == a | α .α (eq.refl .α) a := heq.refl a /- and -/ @@ -354,13 +354,13 @@ iff_true_intro not_false @[congr] lemma not_congr (h : a ↔ b) : ¬a ↔ ¬b := iff.intro (λ h₁ h₂, h₁ (iff.mpr h h₂)) (λ h₁ h₂, h₁ (iff.mp h h₂)) -@[simp] lemma ne_self_iff_false {α : Type u} (a : α) : (not (a = a)) ↔ false := +@[simp] lemma ne_self_iff_false {α : PType u} (a : α) : (not (a = a)) ↔ false := iff.intro false_of_ne false.elim -@[simp] lemma eq_self_iff_true {α : Type u} (a : α) : (a = a) ↔ true := +@[simp] lemma eq_self_iff_true {α : PType u} (a : α) : (a = a) ↔ true := iff_true_intro rfl -@[simp] lemma heq_self_iff_true {α : Type u} (a : α) : (a == a) ↔ true := +@[simp] lemma heq_self_iff_true {α : PType u} (a : α) : (a == a) ↔ true := iff_true_intro (heq.refl a) @[simp] lemma iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false := @@ -537,7 +537,7 @@ iff.intro (λ h, trivial) (λ ha h, false.elim h) /- exists -/ -inductive Exists {α : Type u} (p : α → Prop) : Prop +inductive Exists {α : PType u} (p : α → Prop) : Prop | intro : ∀ (a : α), p a → Exists attribute [intro] Exists.intro @@ -548,24 +548,24 @@ def exists.intro := @Exists.intro notation `exists` binders `, ` r:(scoped P, Exists P) := r notation `∃` binders `, ` r:(scoped P, Exists P) := r -lemma exists.elim {α : Type u} {p : α → Prop} {b : Prop} +lemma exists.elim {α : PType u} {p : α → Prop} {b : Prop} (h₁ : ∃ x, p x) (h₂ : ∀ (a : α), p a → b) : b := Exists.rec h₂ h₁ /- exists unique -/ -def exists_unique {α : Type u} (p : α → Prop) := +def exists_unique {α : PType u} (p : α → Prop) := ∃ x, p x ∧ ∀ y, p y → y = x notation `∃!` binders `, ` r:(scoped P, exists_unique P) := r attribute [intro] -lemma exists_unique.intro {α : Type u} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ y, p y → y = w) : +lemma exists_unique.intro {α : PType u} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ y, p y → y = w) : ∃! x, p x := exists.intro w ⟨h₁, h₂⟩ attribute [recursor 4] -lemma exists_unique.elim {α : Type u} {p : α → Prop} {b : Prop} +lemma exists_unique.elim {α : PType u} {p : α → Prop} {b : Prop} (h₂ : ∃! x, p x) (h₁ : ∀ x, p x → (∀ y, p y → y = x) → b) : b := exists.elim h₂ (λ w hw, h₁ w (and.left hw) (and.right hw)) @@ -573,10 +573,10 @@ lemma exists_unique_of_exists_of_unique {α : Type u} {p : α → Prop} (hex : ∃ x, p x) (hunique : ∀ y₁ y₂, p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x := exists.elim hex (λ x px, exists_unique.intro x px (take y, suppose p y, hunique y x this px)) -lemma exists_of_exists_unique {α : Type u} {p : α → Prop} (h : ∃! x, p x) : ∃ x, p x := +lemma exists_of_exists_unique {α : PType u} {p : α → Prop} (h : ∃! x, p x) : ∃ x, p x := exists.elim h (λ x hx, ⟨x, and.left hx⟩) -lemma unique_of_exists_unique {α : Type u} {p : α → Prop} +lemma unique_of_exists_unique {α : PType u} {p : α → Prop} (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂ := exists_unique.elim h (take x, suppose p x, @@ -584,21 +584,21 @@ exists_unique.elim h show y₁ = y₂, from eq.trans (unique _ py₁) (eq.symm (unique _ py₂))) /- exists, forall, exists unique congruences -/ -@[congr] lemma forall_congr {α : Type u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (∀ a, p a) ↔ ∀ a, q a := +@[congr] lemma forall_congr {α : PType u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (∀ a, p a) ↔ ∀ a, q a := iff.intro (λ p a, iff.mp (h a) (p a)) (λ q a, iff.mpr (h a) (q a)) -lemma exists_imp_exists {α : Type u} {p q : α → Prop} (h : ∀ a, (p a → q a)) (p : ∃ a, p a) : ∃ a, q a := +lemma exists_imp_exists {α : PType u} {p q : α → Prop} (h : ∀ a, (p a → q a)) (p : ∃ a, p a) : ∃ a, q a := exists.elim p (λ a hp, ⟨a, h a hp⟩) -@[congr] lemma exists_congr {α : Type u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (Exists p) ↔ ∃ a, q a := +@[congr] lemma exists_congr {α : PType u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (Exists p) ↔ ∃ a, q a := iff.intro (exists_imp_exists (λ a, iff.mp (h a))) (exists_imp_exists (λ a, iff.mpr (h a))) -@[congr] lemma exists_unique_congr {α : Type u} {p₁ p₂ : α → Prop} (h : ∀ x, p₁ x ↔ p₂ x) : (exists_unique p₁) ↔ (∃! x, p₂ x) := -- +@[congr] lemma exists_unique_congr {α : PType u} {p₁ p₂ : α → Prop} (h : ∀ x, p₁ x ↔ p₂ x) : (exists_unique p₁) ↔ (∃! x, p₂ x) := -- exists_congr (λ x, and_congr (h x) (forall_congr (λ y, imp_congr (h y) iff.rfl))) -lemma forall_not_of_not_exists {α : Type u} {p : α → Prop} : ¬(∃ x, p x) → (∀ x, ¬p x) := +lemma forall_not_of_not_exists {α : PType u} {p : α → Prop} : ¬(∃ x, p x) → (∀ x, ¬p x) := λ hne x hp, hne ⟨x, hp⟩ /- decidable -/ @@ -616,26 +616,26 @@ is_false not_false -- We use "dependent" if-then-else to be able to communicate the if-then-else condition -- to the branches -@[inline] def dite (c : Prop) [h : decidable c] {α : Type u} : (c → α) → (¬ c → α) → α := +@[inline] def dite (c : Prop) [h : decidable c] {α : PType u} : (c → α) → (¬ c → α) → α := λ t e, decidable.rec_on h e t /- if-then-else -/ -@[inline] def ite (c : Prop) [h : decidable c] {α : Type u} (t e : α) : α := +@[inline] def ite (c : Prop) [h : decidable c] {α : PType u} (t e : α) : α := decidable.rec_on h (λ hnc, e) (λ hc, t) namespace decidable variables {p q : Prop} - def rec_on_true [h : decidable p] {h₁ : p → Type u} {h₂ : ¬p → Type u} (h₃ : p) (h₄ : h₁ h₃) + def rec_on_true [h : decidable p] {h₁ : p → PType u} {h₂ : ¬p → PType u} (h₃ : p) (h₄ : h₁ h₃) : decidable.rec_on h h₂ h₁ := decidable.rec_on h (λ h, false.rec _ (h h₃)) (λ h, h₄) - def rec_on_false [h : decidable p] {h₁ : p → Type u} {h₂ : ¬p → Type u} (h₃ : ¬p) (h₄ : h₂ h₃) + def rec_on_false [h : decidable p] {h₁ : p → PType u} {h₂ : ¬p → PType u} (h₃ : ¬p) (h₄ : h₂ h₃) : decidable.rec_on h h₂ h₁ := decidable.rec_on h (λ h, h₄) (λ h, false.rec _ (h₃ h)) - def by_cases {q : Type u} [φ : decidable p] : (p → q) → (¬p → q) → q := dite _ + def by_cases {q : PType u} [φ : decidable p] : (p → q) → (¬p → q) → q := dite _ lemma em (p : Prop) [decidable p] : p ∨ ¬p := by_cases or.inl or.inr @@ -652,7 +652,7 @@ section def decidable_of_decidable_of_eq (hp : decidable p) (h : p = q) : decidable q := decidable_of_decidable_of_iff hp h^.to_iff - protected def or.by_cases [decidable p] [decidable q] {α : Type u} + protected def or.by_cases [decidable p] [decidable q] {α : PType u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α := if hp : p then h₁ hp else if hq : q then h₂ hq else @@ -686,14 +686,14 @@ section decidable_of_decidable_of_iff and.decidable (iff_iff_implies_and_implies p q)^.symm end -instance {α : Type u} [decidable_eq α] (a b : α) : decidable (a ≠ b) := +instance {α : PType u} [decidable_eq α] (a b : α) : decidable (a ≠ b) := implies.decidable lemma bool.ff_ne_tt : ff = tt → false . -def is_dec_eq {α : Type u} (p : α → α → bool) : Prop := ∀ ⦃x y : α⦄, p x y = tt → x = y -def is_dec_refl {α : Type u} (p : α → α → bool) : Prop := ∀ x, p x x = tt +def is_dec_eq {α : PType u} (p : α → α → bool) : Prop := ∀ ⦃x y : α⦄, p x y = tt → x = y +def is_dec_refl {α : PType u} (p : α → α → bool) : Prop := ∀ x, p x x = tt open decidable instance : decidable_eq bool @@ -702,18 +702,18 @@ instance : decidable_eq bool | tt ff := is_false (ne.symm bool.ff_ne_tt) | tt tt := is_true rfl -def decidable_eq_of_bool_pred {α : Type u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq α := +def decidable_eq_of_bool_pred {α : PType u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq α := take x y : α, if hp : p x y = tt then is_true (h₁ hp) else is_false (assume hxy : x = y, absurd (h₂ y) (@eq.rec_on _ _ (λ z, ¬p z y = tt) _ hxy hp)) -lemma decidable_eq_inl_refl {α : Type u} [h : decidable_eq α] (a : α) : h a a = is_true (eq.refl a) := +lemma decidable_eq_inl_refl {α : PType u} [h : decidable_eq α] (a : α) : h a a = is_true (eq.refl a) := match (h a a) with | (is_true e) := rfl | (is_false n) := absurd rfl n end -lemma decidable_eq_inr_neg {α : Type u} [h : decidable_eq α] {a b : α} : Π n : a ≠ b, h a b = is_false n := +lemma decidable_eq_inr_neg {α : PType u} [h : decidable_eq α] {a b : α} : Π n : a ≠ b, h a b = is_false n := assume n, match (h a b) with | (is_true e) := absurd e n @@ -722,22 +722,22 @@ end /- inhabited -/ -class inhabited (α : Type u) := +class inhabited (α : PType u) := (default : α) -def default (α : Type u) [inhabited α] : α := +def default (α : PType u) [inhabited α] : α := inhabited.default α -@[inline, irreducible] def arbitrary (α : Type u) [inhabited α] : α := +@[inline, irreducible] def arbitrary (α : PType u) [inhabited α] : α := default α instance prop.inhabited : inhabited Prop := ⟨true⟩ -instance fun.inhabited (α : Type u) {β : Type v} [h : inhabited β] : inhabited (α → β) := +instance fun.inhabited (α : PType u) {β : PType v} [h : inhabited β] : inhabited (α → β) := inhabited.rec_on h (λ b, ⟨λ a, b⟩) -instance pi.inhabited (α : Type u) {β : α → Type v} [Π x, inhabited (β x)] : inhabited (Π x, β x) := +instance pi.inhabited (α : PType u) {β : α → PType v} [Π x, inhabited (β x)] : inhabited (Π x, β x) := ⟨λ a, default (β a)⟩ instance : inhabited bool := @@ -749,27 +749,27 @@ instance : inhabited pos_num := instance : inhabited num := ⟨num.zero⟩ -class inductive nonempty (α : Type u) : Prop +class inductive nonempty (α : PType u) : Prop | intro : α → nonempty -protected def nonempty.elim {α : Type u} {p : Prop} (h₁ : nonempty α) (h₂ : α → p) : p := +protected def nonempty.elim {α : PType u} {p : Prop} (h₁ : nonempty α) (h₂ : α → p) : p := nonempty.rec h₂ h₁ -instance nonempty_of_inhabited {α : Type u} [inhabited α] : nonempty α := +instance nonempty_of_inhabited {α : PType u} [inhabited α] : nonempty α := ⟨default α⟩ -lemma nonempty_of_exists {α : Type u} {p : α → Prop} : (∃ x, p x) → nonempty α +lemma nonempty_of_exists {α : PType u} {p : α → Prop} : (∃ x, p x) → nonempty α | ⟨w, h⟩ := ⟨w⟩ /- subsingleton -/ -class inductive subsingleton (α : Type u) : Prop +class inductive subsingleton (α : PType u) : Prop | intro : (∀ a b : α, a = b) → subsingleton -protected def subsingleton.elim {α : Type u} [h : subsingleton α] : ∀ (a b : α), a = b := +protected def subsingleton.elim {α : PType u} [h : subsingleton α] : ∀ (a b : α), a = b := subsingleton.rec (λ p, p) h -protected def subsingleton.helim {α β : Type u} [h : subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a == b := +protected def subsingleton.helim {α β : PType 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 := @@ -790,7 +790,7 @@ subsingleton.intro (λ d₁, end) end) -protected lemma rec_subsingleton {p : Prop} [h : decidable p] {h₁ : p → Type u} {h₂ : ¬p → Type u} +protected lemma rec_subsingleton {p : Prop} [h : decidable p] {h₁ : p → PType u} {h₂ : ¬p → PType u} [h₃ : Π (h : p), subsingleton (h₁ h)] [h₄ : Π (h : ¬p), subsingleton (h₂ h)] : subsingleton (decidable.rec_on h h₂ h₁) := match h with @@ -798,20 +798,20 @@ match h with | (is_false h) := h₄ h end -lemma if_pos {c : Prop} [h : decidable c] (hc : c) {α : Type u} {t e : α} : (ite c t e) = t := +lemma if_pos {c : Prop} [h : decidable c] (hc : c) {α : PType u} {t e : α} : (ite c t e) = t := match h with | (is_true hc) := rfl | (is_false hnc) := absurd hc hnc end -lemma if_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : Type u} {t e : α} : (ite c t e) = e := +lemma if_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : PType u} {t e : α} : (ite c t e) = e := match h with | (is_true hc) := absurd hc hnc | (is_false hnc) := rfl end attribute [simp] -lemma if_t_t (c : Prop) [h : decidable c] {α : Type u} (t : α) : (ite c t t) = t := +lemma if_t_t (c : Prop) [h : decidable c] {α : PType u} (t : α) : (ite c t t) = t := match h with | (is_true hc) := rfl | (is_false hnc) := rfl @@ -823,7 +823,7 @@ assume hc, eq.rec_on (if_pos hc : ite c t e = t) h lemma implies_of_if_neg {c t e : Prop} [decidable c] (h : ite c t e) : ¬c → e := assume hnc, eq.rec_on (if_neg hnc : ite c t e = e) h -lemma if_ctx_congr {α : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] +lemma if_ctx_congr {α : PType u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x y u v : α} (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) : ite b x y = ite c u v := @@ -835,29 +835,29 @@ match dec_b, dec_c with end @[congr] -lemma if_congr {α : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] +lemma if_congr {α : PType u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x y u v : α} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) : ite b x y = ite c u v := @if_ctx_congr α b c dec_b dec_c x y u v h_c (λ h, h_t) (λ h, h_e) -lemma if_ctx_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b] {x y u v : α} +lemma if_ctx_simp_congr {α : PType u} {b c : Prop} [dec_b : decidable b] {x y u v : α} (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) : ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) α u v) := @if_ctx_congr α b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x y u v h_c h_t h_e @[congr] -lemma if_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b] {x y u v : α} +lemma if_simp_congr {α : PType u} {b c : Prop} [dec_b : decidable b] {x y u v : α} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) : ite b x y = (@ite c (decidable_of_decidable_of_iff dec_b h_c) α u v) := @if_ctx_simp_congr α b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e) @[simp] -lemma if_true {α : Type u} {h : decidable true} (t e : α) : (@ite true h α t e) = t := +lemma if_true {α : PType u} {h : decidable true} (t e : α) : (@ite true h α t e) = t := if_pos trivial @[simp] -lemma if_false {α : Type u} {h : decidable false} (t e : α) : (@ite false h α t e) = e := +lemma if_false {α : PType u} {h : decidable false} (t e : α) : (@ite false h α t e) = e := if_neg not_false lemma if_ctx_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c] @@ -887,19 +887,19 @@ lemma if_simp_congr_prop {b c x y u v : Prop} [dec_b : decidable b] ite b x y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) := @if_ctx_simp_congr_prop b c x y u v dec_b h_c (λ h, h_t) (λ h, h_e) -lemma dif_pos {c : Prop} [h : decidable c] (hc : c) {α : Type u} {t : c → α} {e : ¬ c → α} : dite c t e = t hc := +lemma dif_pos {c : Prop} [h : decidable c] (hc : c) {α : PType u} {t : c → α} {e : ¬ c → α} : dite c t e = t hc := match h with | (is_true hc) := rfl | (is_false hnc) := absurd hc hnc end -lemma dif_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : Type u} {t : c → α} {e : ¬ c → α} : dite c t e = e hnc := +lemma dif_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : PType u} {t : c → α} {e : ¬ c → α} : dite c t e = e hnc := match h with | (is_true hc) := absurd hc hnc | (is_false hnc) := rfl end -lemma dif_ctx_congr {α : Type u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] +lemma dif_ctx_congr {α : PType u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h_c : b ↔ c) (h_t : ∀ (h : c), x (iff.mpr h_c h) = u h) @@ -912,7 +912,7 @@ match dec_b, dec_c with | (is_true h₁), (is_false h₂) := absurd h₁ (iff.mpr (not_iff_not_of_iff h_c) h₂) end -lemma dif_ctx_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b] +lemma dif_ctx_simp_congr {α : PType u} {b c : Prop} [dec_b : decidable b] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h_c : b ↔ c) (h_t : ∀ (h : c), x (iff.mpr h_c h) = u h) @@ -921,7 +921,7 @@ lemma dif_ctx_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b] @dif_ctx_congr α b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x u y v h_c h_t h_e -- Remark: dite and ite are "defally equal" when we ignore the proofs. -lemma dite_ite_eq (c : Prop) [h : decidable c] {α : Type u} (t : α) (e : α) : dite c (λ h, t) (λ h, e) = ite c t e := +lemma dite_ite_eq (c : Prop) [h : decidable c] {α : PType u} (t : α) (e : α) : dite c (λ h, t) (λ h, e) = ite c t e := match h with | (is_true hc) := rfl | (is_false hnc) := rfl @@ -952,7 +952,7 @@ match h₁, h₂ with end /- Universe lifting operation -/ -structure {r s} ulift (α : Type s) : Type (max 1 s r) := +structure {r s} ulift (α : Type s) : Type (max s r) := up :: (down : α) namespace ulift @@ -965,19 +965,19 @@ rfl end ulift /- Equalities for rewriting let-expressions -/ -lemma let_value_eq {α : Type u} {β : Type v} {a₁ a₂ : α} (b : α → β) : +lemma let_value_eq {α : PType u} {β : PType v} {a₁ a₂ : α} (b : α → β) : a₁ = a₂ → (let x : α := a₁ in b x) = (let x : α := a₂ in b x) := λ h, eq.rec_on h rfl -lemma let_value_heq {α : Type v} {β : α → Type u} {a₁ a₂ : α} (b : Π x : α, β x) : +lemma let_value_heq {α : PType v} {β : α → PType u} {a₁ a₂ : α} (b : Π x : α, β x) : a₁ = a₂ → (let x : α := a₁ in b x) == (let x : α := a₂ in b x) := λ h, eq.rec_on h (heq.refl (b a₁)) -lemma let_body_eq {α : Type v} {β : α → Type u} (a : α) {b₁ b₂ : Π x : α, β x} : +lemma let_body_eq {α : PType v} {β : α → PType u} (a : α) {b₁ b₂ : Π x : α, β x} : (∀ x, b₁ x = b₂ x) → (let x : α := a in b₁ x) = (let x : α := a in b₂ x) := λ h, h a -lemma let_eq {α : Type v} {β : Type u} {a₁ a₂ : α} {b₁ b₂ : α → β} : +lemma let_eq {α : PType v} {β : PType u} {a₁ a₂ : α} {b₁ b₂ : α → β} : a₁ = a₂ → (∀ x, b₁ x = b₂ x) → (let x : α := a₁ in b₁ x) = (let x : α := a₂ in b₂ x) := λ h₁ h₂, eq.rec_on h₁ (h₂ a₁) diff --git a/library/init/meta/format.lean b/library/init/meta/format.lean index 69aa549937..a55e7cc091 100644 --- a/library/init/meta/format.lean +++ b/library/init/meta/format.lean @@ -11,7 +11,7 @@ universe variables u v inductive format.color | red | green | orange | blue | pink | cyan | grey -meta constant format : Type 1 +meta constant format : Type meta constant format.line : format meta constant format.space : format meta constant format.nil : format diff --git a/library/init/meta/options.lean b/library/init/meta/options.lean index e21c292413..10471a8787 100644 --- a/library/init/meta/options.lean +++ b/library/init/meta/options.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import init.meta.name universe variables u -meta constant options : Type 1 +meta constant options : Type meta constant options.size : options → nat meta constant options.mk : options meta constant options.contains : options → name → bool diff --git a/library/init/meta/rb_map.lean b/library/init/meta/rb_map.lean index cd8223d792..dffcc57818 100644 --- a/library/init/meta/rb_map.lean +++ b/library/init/meta/rb_map.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad prelude import init.data.ordering init.function init.meta.name init.meta.format -meta constant {u₁ u₂} rb_map : Type u₁ → Type u₂ → Type (max u₁ u₂ 1) +meta constant {u₁ u₂} rb_map : Type u₁ → Type u₂ → Type (max u₁ u₂) namespace rb_map meta constant mk_core {key : Type} (data : Type) : (key → key → ordering) → rb_map key data diff --git a/library/init/meta/rec_util.lean b/library/init/meta/rec_util.lean index 6ab3227e22..843ca848a9 100644 --- a/library/init/meta/rec_util.lean +++ b/library/init/meta/rec_util.lean @@ -19,10 +19,10 @@ do t ← infer_type e, /- Auxiliary function for using brec_on "dictionary" -/ private meta def mk_rec_inst_aux : expr → nat → tactic expr | F 0 := do - P ← mk_app `prod.fst [F], - mk_app `prod.fst [P] + P ← mk_app `pprod.fst [F], + mk_app `pprod.fst [P] | F (n+1) := do - F' ← mk_app `prod.snd [F], + F' ← mk_app `pprod.snd [F], mk_rec_inst_aux F' n /- Construct brec_on "recursive value". F_name is the name of the brec_on "dictionary". diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index e6467c034e..5f386b2b1f 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -137,7 +137,7 @@ meta def repeat_exactly : nat → tactic unit → tactic unit meta def repeat : tactic unit → tactic unit := repeat_at_most 100000 -meta def returnex {α : Type 1} (e : exceptional α) : tactic α := +meta def returnex {α : Type} (e : exceptional α) : tactic α := λ s, match e with | (exceptional.success a) := tactic_result.success a s | (exceptional.exception .α f) := tactic_result.exception α (λ u, f options.mk) none s -- TODO(Leo): extract options from environment @@ -282,8 +282,8 @@ meta constant get_unused_name : name → option nat → tactic name Example, given rel.{l_1 l_2} : Pi (α : Type.{l_1}) (β : α -> Type.{l_2}), (Pi x : α, β x) -> (Pi x : α, β x) -> , Prop - nat : Type 1 - real : Type 1 + nat : Type + real : Type vec.{l} : Pi (α : Type l) (n : nat), Type.{l1} f g : Pi (n : nat), vec real n then diff --git a/library/init/meta/task.lean b/library/init/meta/task.lean index 6b1847d1ac..8d34056a19 100644 --- a/library/init/meta/task.lean +++ b/library/init/meta/task.lean @@ -1,7 +1,7 @@ prelude import init.category -meta constant {u} task : Type u → Type (max u 1) +meta constant {u} task : Type u → Type u namespace task diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean index 908ab08085..e752435a83 100644 --- a/library/init/meta/vm.lean +++ b/library/init/meta/vm.lean @@ -75,7 +75,7 @@ meta constant vm_core.bind {α β : Type} : vm_core α → (α → vm_core β) meta instance : monad vm_core := {map := @vm_core.map, ret := @vm_core.ret, bind := @vm_core.bind} -@[reducible] meta def vm (α : Type) : Type := option_t.{1 1} vm_core α +@[reducible] meta def vm (α : Type) : Type := option_t vm_core α namespace vm meta constant get_env : vm environment diff --git a/library/init/native/default.lean b/library/init/native/default.lean index 6a19fe0ac8..e41a3a6577 100644 --- a/library/init/native/default.lean +++ b/library/init/native/default.lean @@ -22,10 +22,9 @@ import init.native.config import init.native.result namespace native - -inductive error +inductive error : Type | string : string → error -| many : list error → error +| many : list error → error meta def error.to_string : error → string | (error.string s) := s diff --git a/library/init/wf.lean b/library/init/wf.lean index 547a202f10..0819f606aa 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -20,7 +20,7 @@ acc.rec_on h₁ (λ x₁ ac₁ ih h₂, ac₁ y h₂) h₂ -- dependent elimination for acc attribute [recursor] protected def drec - {C : Π (a : α), acc r a → Type v} + {C : Π (a : α), acc r a → PType v} (h₁ : Π (x : α) (acx : Π (y : α), r y x → acc r y), (Π (y : α) (ryx : r y x), C y (acx y ryx)) → C x (acc.intro x acx)) {a : α} (h₂ : acc r a) : C a h₂ := acc.rec (λ x acx ih h₂, h₁ x acx (λ y ryx, ih y ryx (acx y ryx))) h₂ h₂ @@ -39,7 +39,7 @@ local infix `≺`:50 := r hypothesis hwf : well_founded r -lemma recursion {C : α → Type v} (a : α) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a := +lemma recursion {C : α → PType v} (a : α) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a := acc.rec_on (apply hwf a) (λ x₁ ac₁ ih, h x₁ ih) lemma induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a := diff --git a/library/library.md b/library/library.md index 4ae4a0f175..6e0dc61f8b 100644 --- a/library/library.md +++ b/library/library.md @@ -21,7 +21,7 @@ Constructions with: * an impredicative, proof-irrelevant type `Prop` of propositions * universe polymorphism -* a non-cumulative hierarchy of universes, `Type 1`, `Type 2`, ... above `Prop` +* a non-cumulative hierarchy of universes, `Type 0`, `Type 1`, ... above `Prop` * inductively defined types * quotient types diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 5464e06fe1..c8eb8adc90 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -155,7 +155,7 @@ (,(rx word-start (group "example") ".") (1 'font-lock-keyword-face)) (,(rx (or "∎")) . 'font-lock-keyword-face) ;; Types - (,(rx word-start (or "Prop" "Type" "Type*" "Type₀" "Type₁" "Type₂" "Type₃") symbol-end) . 'font-lock-type-face) + (,(rx word-start (or "Prop" "Type" "Type*" "PType" "PType*" "Type₂" "Type₃") symbol-end) . 'font-lock-type-face) (,(rx word-start (group (or "Prop" "Type")) ".") (1 'font-lock-type-face)) ;; String ("\"[^\"]*\"" . 'font-lock-string-face) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 7b51137890..769a9db8ba 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -48,18 +48,44 @@ bool get_parser_checkpoint_have(options const & opts) { using namespace notation; // NOLINT +static name * g_no_universe_annotation = nullptr; + +bool is_sort_wo_universe(expr const & e) { + return is_annotation(e, *g_no_universe_annotation); +} + +expr mk_sort_wo_universe(parser & p, pos_info const & pos, bool is_type) { + expr r = p.save_pos(mk_sort(is_type ? mk_level_one() : mk_level_zero()), pos); + return p.save_pos(mk_annotation(*g_no_universe_annotation, r), pos); +} + static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) { if (p.curr_is_token(get_llevel_curly_tk())) { p.next(); - level l = p.parse_level(); + level l = mk_succ(p.parse_level()); p.check_token_next(get_rcurly_tk(), "invalid Type expression, '}' expected"); return p.save_pos(mk_sort(l), pos); } else { - return p.save_pos(mk_sort(mk_level_one_placeholder()), pos); + return mk_sort_wo_universe(p, pos, true); + } +} + +static expr parse_PType(parser & p, unsigned, expr const *, pos_info const & pos) { + if (p.curr_is_token(get_llevel_curly_tk())) { + p.next(); + level l = p.parse_level(); + p.check_token_next(get_rcurly_tk(), "invalid PType expression, '}' expected"); + return p.save_pos(mk_sort(l), pos); + } else { + return mk_sort_wo_universe(p, pos, false); } } static expr parse_Type_star(parser & p, unsigned, expr const *, pos_info const & pos) { + return p.save_pos(mk_sort(mk_succ(mk_level_placeholder())), pos); +} + +static expr parse_PType_star(parser & p, unsigned, expr const *, pos_info const & pos) { return p.save_pos(mk_sort(mk_level_placeholder()), pos); } @@ -743,6 +769,8 @@ parse_table init_nud_table() { r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0); r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0); r = r.add({transition("Type*", mk_ext_action(parse_Type_star))}, x0); + r = r.add({transition("PType", mk_ext_action(parse_PType))}, x0); + r = r.add({transition("PType*", mk_ext_action(parse_PType_star))}, x0); r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0); r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0); r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0); @@ -902,6 +930,9 @@ parse_table get_builtin_led_table() { } void initialize_builtin_exprs() { + g_no_universe_annotation = new name("no_univ"); + register_annotation(*g_no_universe_annotation); + g_not = new expr(mk_constant(get_not_name())); g_nud_table = new parse_table(); *g_nud_table = init_nud_table(); @@ -944,5 +975,6 @@ void finalize_builtin_exprs() { delete g_anonymous_constructor; delete g_field_notation_opcode; delete g_field_notation_name; + delete g_no_universe_annotation; } } diff --git a/src/frontends/lean/builtin_exprs.h b/src/frontends/lean/builtin_exprs.h index 222087c4bf..179b53f83e 100644 --- a/src/frontends/lean/builtin_exprs.h +++ b/src/frontends/lean/builtin_exprs.h @@ -7,6 +7,8 @@ Author: Leonardo de Moura #pragma once #include "frontends/lean/parse_table.h" namespace lean { +bool is_sort_wo_universe(expr const & e); + expr mk_anonymous_constructor(expr const & e); bool is_anonymous_constructor(expr const & e); expr const & get_anonymous_constructor_arg(expr const & e); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 51eda793d6..d6bff55e36 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -675,6 +675,15 @@ expr elaborator::visit_typed_expr(expr const & e) { line() + format("but is expected to have type") + pp_indent(pp_fn, new_type)); } +level elaborator::dec_level(level const & l, expr const & ref) { + if (auto d = ::lean::dec_level(l)) + return *d; + level r = m_ctx.mk_univ_metavar_decl(); + if (!m_ctx.is_def_eq(mk_succ(r), l)) + throw elaborator_exception(ref, "invalid pre-numeral, universe level must be > 0"); + return r; +} + expr elaborator::visit_prenum(expr const & e, optional const & expected_type) { lean_assert(is_prenum(e)); expr ref = e; @@ -690,7 +699,7 @@ expr elaborator::visit_prenum(expr const & e, optional const & expected_ty m_numeral_types = cons(A, m_numeral_types); } level A_lvl = get_level(A, ref); - levels ls(A_lvl); + levels ls(dec_level(A_lvl, ref)); if (v.is_neg()) throw elaborator_exception(ref, "invalid pre-numeral, it must be a non-negative value"); if (v.is_zero()) { @@ -2449,6 +2458,8 @@ expr elaborator::visit(expr const & e, optional const & expected_type) { return visit(get_annotation_arg(e), expected_type); } else if (is_emptyc_or_emptys(e)) { return visit_emptyc_or_emptys(e, expected_type); + } else if (is_sort_wo_universe(e)) { + return visit(get_annotation_arg(e), expected_type); } else { switch (e.kind()) { case expr_kind::Var: lean_unreachable(); // LCOV_EXCL_LINE diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 6a5678e7e9..2eccb3b531 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -158,6 +158,7 @@ private: expr visit_scope_trace(expr const & e, optional const & expected_type); expr visit_typed_expr(expr const & e); + level dec_level(level const & l, expr const & ref); expr visit_prenum_core(expr const & e, optional const & expected_type); expr visit_prenum(expr const & e, optional const & expected_type); expr visit_placeholder(expr const & e, optional const & expected_type); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index dcd54d4fab..5f6e74950e 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1950,9 +1950,13 @@ bool parser::curr_starts_expr() { } expr parser::parse_led(expr left) { - if (is_sort(left) && is_one_placeholder(sort_level(left)) && + if (is_sort_wo_universe(left) && (curr_is_numeral() || curr_is_identifier() || curr_is_token(get_lparen_tk()) || curr_is_token(get_placeholder_tk()))) { + left = get_annotation_arg(left); level l = parse_level(get_max_prec()); + lean_assert(sort_level(left) == mk_level_one() || sort_level(left) == mk_level_zero()); + if (sort_level(left) == mk_level_one()) + l = mk_succ(l); return copy_tag(left, update_sort(left, l)); } else { switch (curr()) { diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index cf23df32c3..8c27410acd 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -604,8 +604,10 @@ auto pretty_fn::pp_sort(expr const & e) -> result { return result(format("Prop")); } else if (u == mk_level_one()) { return result(format("Type")); + } else if (optional u1 = dec_level(u)) { + return result(group(format("Type") + space() + nest(5, pp_child(*u1)))); } else { - return result(group(format("Type") + space() + nest(5, pp_child(u)))); + return result(group(format("PType") + space() + nest(5, pp_child(u)))); } } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index fb068a50da..201b955659 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -84,7 +84,8 @@ void init_token_table(token_table & t) { {"from", 0}, {"(", g_max_prec}, {"`(", g_max_prec}, {"`[", g_max_prec}, {"`", g_max_prec}, {"%%", g_max_prec}, {"()", g_max_prec}, {")", 0}, {"'", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, - {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type*", g_max_prec}, + {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, + {"Type", g_max_prec}, {"Type*", g_max_prec}, {"PType", g_max_prec}, {"PType*", g_max_prec}, {"(:", g_max_prec}, {":)", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0}, {"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"without", 0}, {"...", 0}, {",", 0}, diff --git a/src/library/compiler/simp_pr1_rec.cpp b/src/library/compiler/simp_pr1_rec.cpp index ec0af548ed..8581143dd8 100644 --- a/src/library/compiler/simp_pr1_rec.cpp +++ b/src/library/compiler/simp_pr1_rec.cpp @@ -47,7 +47,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor { virtual expr visit_app(expr const & e) { expr const & f = get_app_fn(e); - if (is_constant(f) && const_name(f) == get_prod_fst_name()) { + if (is_constant(f) && const_name(f) == get_pprod_fst_name()) { buffer args; get_app_args(e, args); if (args.size() >= 3 && is_rec_arg(args[2])) { @@ -69,7 +69,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor { optional simplify(expr const & e) { expr const & f = get_app_fn(e); - if (!is_constant(f) || const_name(f) != get_prod_fst_name()) + if (!is_constant(f) || const_name(f) != get_pprod_fst_name()) return none_expr(); buffer args; get_app_args(e, args); @@ -105,7 +105,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor { buffer typeformer_body_args; expr typeformer_body_fn = get_app_args(typeformer_body, typeformer_body_args); if (!is_constant(typeformer_body_fn) || - const_name(typeformer_body_fn) != get_prod_name() || + const_name(typeformer_body_fn) != get_pprod_name() || typeformer_body_args.size() != 2) { return none_expr(); } @@ -143,7 +143,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor { } buffer type_args; expr type_fn = get_app_args(type, type_args); - if (!is_constant(type_fn) || const_name(type_fn) != get_prod_name() || type_args.size() != 2) { + if (!is_constant(type_fn) || const_name(type_fn) != get_pprod_name() || type_args.size() != 2) { return none_expr(); } minor_ctx[k] = update_mlocal(minor_ctx[k], locals.mk_pi(type_args[0])); @@ -154,7 +154,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor { buffer minor_body_args; expr minor_body_fn = get_app_args(minor_body, minor_body_args); if (!is_constant(minor_body_fn) || - const_name(minor_body_fn) != get_prod_mk_name() || + const_name(minor_body_fn) != get_pprod_mk_name() || minor_body_args.size() != 4) { return none_expr(); } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 02fd757e2c..a17561a0a5 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -333,10 +333,11 @@ name const * g_pos_num = nullptr; name const * g_pos_num_bit0 = nullptr; name const * g_pos_num_bit1 = nullptr; name const * g_pos_num_one = nullptr; -name const * g_prod = nullptr; name const * g_prod_mk = nullptr; -name const * g_prod_fst = nullptr; -name const * g_prod_snd = nullptr; +name const * g_pprod = nullptr; +name const * g_pprod_mk = nullptr; +name const * g_pprod_fst = nullptr; +name const * g_pprod_snd = nullptr; name const * g_propext = nullptr; name const * g_pexpr = nullptr; name const * g_pexpr_subst = nullptr; @@ -377,6 +378,11 @@ name const * g_sigma_cases_on = nullptr; name const * g_sigma_mk = nullptr; name const * g_sigma_fst = nullptr; name const * g_sigma_snd = nullptr; +name const * g_psigma = nullptr; +name const * g_psigma_cases_on = nullptr; +name const * g_psigma_mk = nullptr; +name const * g_psigma_fst = nullptr; +name const * g_psigma_snd = nullptr; name const * g_simp = nullptr; name const * g_simplifier_assoc_subst = nullptr; name const * g_simplifier_congr_bin_op = nullptr; @@ -410,6 +416,10 @@ name const * g_sum = nullptr; name const * g_sum_cases_on = nullptr; name const * g_sum_inl = nullptr; name const * g_sum_inr = nullptr; +name const * g_psum = nullptr; +name const * g_psum_cases_on = nullptr; +name const * g_psum_inl = nullptr; +name const * g_psum_inr = nullptr; name const * g_default_smt_config = nullptr; name const * g_smt_state_mk = nullptr; name const * g_smt_tactic_execute = nullptr; @@ -798,10 +808,11 @@ void initialize_constants() { g_pos_num_bit0 = new name{"pos_num", "bit0"}; g_pos_num_bit1 = new name{"pos_num", "bit1"}; g_pos_num_one = new name{"pos_num", "one"}; - g_prod = new name{"prod"}; g_prod_mk = new name{"prod", "mk"}; - g_prod_fst = new name{"prod", "fst"}; - g_prod_snd = new name{"prod", "snd"}; + g_pprod = new name{"pprod"}; + g_pprod_mk = new name{"pprod", "mk"}; + g_pprod_fst = new name{"pprod", "fst"}; + g_pprod_snd = new name{"pprod", "snd"}; g_propext = new name{"propext"}; g_pexpr = new name{"pexpr"}; g_pexpr_subst = new name{"pexpr", "subst"}; @@ -842,6 +853,11 @@ void initialize_constants() { g_sigma_mk = new name{"sigma", "mk"}; g_sigma_fst = new name{"sigma", "fst"}; g_sigma_snd = new name{"sigma", "snd"}; + g_psigma = new name{"psigma"}; + g_psigma_cases_on = new name{"psigma", "cases_on"}; + g_psigma_mk = new name{"psigma", "mk"}; + g_psigma_fst = new name{"psigma", "fst"}; + g_psigma_snd = new name{"psigma", "snd"}; g_simp = new name{"simp"}; g_simplifier_assoc_subst = new name{"simplifier", "assoc_subst"}; g_simplifier_congr_bin_op = new name{"simplifier", "congr_bin_op"}; @@ -875,6 +891,10 @@ void initialize_constants() { g_sum_cases_on = new name{"sum", "cases_on"}; g_sum_inl = new name{"sum", "inl"}; g_sum_inr = new name{"sum", "inr"}; + g_psum = new name{"psum"}; + g_psum_cases_on = new name{"psum", "cases_on"}; + g_psum_inl = new name{"psum", "inl"}; + g_psum_inr = new name{"psum", "inr"}; g_default_smt_config = new name{"default_smt_config"}; g_smt_state_mk = new name{"smt_state", "mk"}; g_smt_tactic_execute = new name{"smt_tactic", "execute"}; @@ -1264,10 +1284,11 @@ void finalize_constants() { delete g_pos_num_bit0; delete g_pos_num_bit1; delete g_pos_num_one; - delete g_prod; delete g_prod_mk; - delete g_prod_fst; - delete g_prod_snd; + delete g_pprod; + delete g_pprod_mk; + delete g_pprod_fst; + delete g_pprod_snd; delete g_propext; delete g_pexpr; delete g_pexpr_subst; @@ -1308,6 +1329,11 @@ void finalize_constants() { delete g_sigma_mk; delete g_sigma_fst; delete g_sigma_snd; + delete g_psigma; + delete g_psigma_cases_on; + delete g_psigma_mk; + delete g_psigma_fst; + delete g_psigma_snd; delete g_simp; delete g_simplifier_assoc_subst; delete g_simplifier_congr_bin_op; @@ -1341,6 +1367,10 @@ void finalize_constants() { delete g_sum_cases_on; delete g_sum_inl; delete g_sum_inr; + delete g_psum; + delete g_psum_cases_on; + delete g_psum_inl; + delete g_psum_inr; delete g_default_smt_config; delete g_smt_state_mk; delete g_smt_tactic_execute; @@ -1729,10 +1759,11 @@ name const & get_pos_num_name() { return *g_pos_num; } name const & get_pos_num_bit0_name() { return *g_pos_num_bit0; } name const & get_pos_num_bit1_name() { return *g_pos_num_bit1; } name const & get_pos_num_one_name() { return *g_pos_num_one; } -name const & get_prod_name() { return *g_prod; } name const & get_prod_mk_name() { return *g_prod_mk; } -name const & get_prod_fst_name() { return *g_prod_fst; } -name const & get_prod_snd_name() { return *g_prod_snd; } +name const & get_pprod_name() { return *g_pprod; } +name const & get_pprod_mk_name() { return *g_pprod_mk; } +name const & get_pprod_fst_name() { return *g_pprod_fst; } +name const & get_pprod_snd_name() { return *g_pprod_snd; } name const & get_propext_name() { return *g_propext; } name const & get_pexpr_name() { return *g_pexpr; } name const & get_pexpr_subst_name() { return *g_pexpr_subst; } @@ -1773,6 +1804,11 @@ name const & get_sigma_cases_on_name() { return *g_sigma_cases_on; } name const & get_sigma_mk_name() { return *g_sigma_mk; } name const & get_sigma_fst_name() { return *g_sigma_fst; } name const & get_sigma_snd_name() { return *g_sigma_snd; } +name const & get_psigma_name() { return *g_psigma; } +name const & get_psigma_cases_on_name() { return *g_psigma_cases_on; } +name const & get_psigma_mk_name() { return *g_psigma_mk; } +name const & get_psigma_fst_name() { return *g_psigma_fst; } +name const & get_psigma_snd_name() { return *g_psigma_snd; } name const & get_simp_name() { return *g_simp; } name const & get_simplifier_assoc_subst_name() { return *g_simplifier_assoc_subst; } name const & get_simplifier_congr_bin_op_name() { return *g_simplifier_congr_bin_op; } @@ -1806,6 +1842,10 @@ name const & get_sum_name() { return *g_sum; } name const & get_sum_cases_on_name() { return *g_sum_cases_on; } name const & get_sum_inl_name() { return *g_sum_inl; } name const & get_sum_inr_name() { return *g_sum_inr; } +name const & get_psum_name() { return *g_psum; } +name const & get_psum_cases_on_name() { return *g_psum_cases_on; } +name const & get_psum_inl_name() { return *g_psum_inl; } +name const & get_psum_inr_name() { return *g_psum_inr; } name const & get_default_smt_config_name() { return *g_default_smt_config; } name const & get_smt_state_mk_name() { return *g_smt_state_mk; } name const & get_smt_tactic_execute_name() { return *g_smt_tactic_execute; } diff --git a/src/library/constants.h b/src/library/constants.h index 85ef3eba70..80f7bf45e6 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -335,10 +335,11 @@ name const & get_pos_num_name(); name const & get_pos_num_bit0_name(); name const & get_pos_num_bit1_name(); name const & get_pos_num_one_name(); -name const & get_prod_name(); name const & get_prod_mk_name(); -name const & get_prod_fst_name(); -name const & get_prod_snd_name(); +name const & get_pprod_name(); +name const & get_pprod_mk_name(); +name const & get_pprod_fst_name(); +name const & get_pprod_snd_name(); name const & get_propext_name(); name const & get_pexpr_name(); name const & get_pexpr_subst_name(); @@ -379,6 +380,11 @@ name const & get_sigma_cases_on_name(); name const & get_sigma_mk_name(); name const & get_sigma_fst_name(); name const & get_sigma_snd_name(); +name const & get_psigma_name(); +name const & get_psigma_cases_on_name(); +name const & get_psigma_mk_name(); +name const & get_psigma_fst_name(); +name const & get_psigma_snd_name(); name const & get_simp_name(); name const & get_simplifier_assoc_subst_name(); name const & get_simplifier_congr_bin_op_name(); @@ -412,6 +418,10 @@ name const & get_sum_name(); name const & get_sum_cases_on_name(); name const & get_sum_inl_name(); name const & get_sum_inr_name(); +name const & get_psum_name(); +name const & get_psum_cases_on_name(); +name const & get_psum_inl_name(); +name const & get_psum_inr_name(); name const & get_default_smt_config_name(); name const & get_smt_state_mk_name(); name const & get_smt_tactic_execute_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 5ec3880530..b5046b7794 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -328,10 +328,11 @@ pos_num pos_num.bit0 pos_num.bit1 pos_num.one -prod prod.mk -prod.fst -prod.snd +pprod +pprod.mk +pprod.fst +pprod.snd propext pexpr pexpr.subst @@ -372,6 +373,11 @@ sigma.cases_on sigma.mk sigma.fst sigma.snd +psigma +psigma.cases_on +psigma.mk +psigma.fst +psigma.snd simp simplifier.assoc_subst simplifier.congr_bin_op @@ -405,6 +411,10 @@ sum sum.cases_on sum.inl sum.inr +psum +psum.cases_on +psum.inl +psum.inr default_smt_config smt_state.mk smt_tactic.execute diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index 8e843f5ea9..2a95064d87 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -125,10 +125,10 @@ static environment mk_below(environment const & env, name const & n, bool ibelow expr fst = mlocal_type(minor_arg); minor_arg = update_mlocal(minor_arg, Pi(minor_arg_args, Type_result)); expr snd = Pi(minor_arg_args, mk_app(minor_arg, minor_arg_args)); - prod_pairs.push_back(mk_prod(tc, fst, snd, ibelow)); + prod_pairs.push_back(mk_pprod(tc, fst, snd, ibelow)); } } - expr new_arg = foldr([&](expr const & a, expr const & b) { return mk_prod(tc, a, b, ibelow); }, + expr new_arg = foldr([&](expr const & a, expr const & b) { return mk_pprod(tc, a, b, ibelow); }, [&]() { return mk_unit(rlvl, ibelow); }, prod_pairs.size(), prod_pairs.data()); rec = mk_app(rec, Fun(minor_args, new_arg)); @@ -273,7 +273,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) to_telescope(mlocal_type(C), C_args); expr C_t = mk_app(C, C_args); expr below_t = mk_app(belows[j], C_args); - expr prod = mk_prod(tc, C_t, below_t, ind); + expr prod = mk_pprod(tc, C_t, below_t, ind); rec = mk_app(rec, Fun(C_args, prod)); } // add minor premises to rec @@ -289,19 +289,19 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) if (auto k = is_typeformer_app(typeformer_names, minor_arg_type)) { buffer C_args; get_app_args(minor_arg_type, C_args); - expr new_minor_arg_type = mk_prod(tc, minor_arg_type, mk_app(belows[*k], C_args), ind); + expr new_minor_arg_type = mk_pprod(tc, minor_arg_type, mk_app(belows[*k], C_args), ind); minor_arg = update_mlocal(minor_arg, Pi(minor_arg_args, new_minor_arg_type)); if (minor_arg_args.empty()) { pairs.push_back(minor_arg); } else { expr r = mk_app(minor_arg, minor_arg_args); - expr r_1 = Fun(minor_arg_args, mk_fst(tc, r, ind)); - expr r_2 = Fun(minor_arg_args, mk_snd(tc, r, ind)); - pairs.push_back(mk_pair(tc, r_1, r_2, ind)); + expr r_1 = Fun(minor_arg_args, mk_pprod_fst(tc, r, ind)); + expr r_2 = Fun(minor_arg_args, mk_pprod_snd(tc, r, ind)); + pairs.push_back(mk_pprod_mk(tc, r_1, r_2, ind)); } } } - expr b = foldr([&](expr const & a, expr const & b) { return mk_pair(tc, a, b, ind); }, + expr b = foldr([&](expr const & a, expr const & b) { return mk_pprod_mk(tc, a, b, ind); }, [&]() { return mk_unit_mk(rlvl, ind); }, pairs.size(), pairs.data()); unsigned F_idx = *is_typeformer_app(typeformer_names, minor_type); @@ -309,7 +309,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) buffer F_args; get_app_args(minor_type, F_args); F_args.push_back(b); - expr new_arg = mk_pair(tc, mk_app(F, F_args), b, ind); + expr new_arg = mk_pprod_mk(tc, mk_app(F, F_args), b, ind); rec = mk_app(rec, Fun(minor_args, new_arg)); } // add indices and major to rec @@ -319,7 +319,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) name brec_on_name = name(n, ind ? "binduction_on" : "brec_on"); expr brec_on_type = Pi(args, result_type); - expr brec_on_value = Fun(args, mk_fst(tc, rec, ind)); + expr brec_on_value = Fun(args, mk_pprod_fst(tc, rec, ind)); declaration new_d = mk_definition_inferring_trusted(env, brec_on_name, blps, brec_on_type, brec_on_value, reducibility_hints::mk_abbreviation()); diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp index 981c16d8fb..34fb5c7881 100644 --- a/src/library/equations_compiler/structural_rec.cpp +++ b/src/library/equations_compiler/structural_rec.cpp @@ -414,13 +414,13 @@ struct structural_rec_fn { optional to_below(expr const & d, expr const & a, expr const & F) { expr const & fn = get_app_fn(d); trace_struct_aux(tout() << "d: " << d << ", a: " << a << ", F: " << F << "\n";); - if (is_constant(fn, get_prod_name()) || is_constant(fn, get_and_name())) { + if (is_constant(fn, get_pprod_name()) || is_constant(fn, get_and_name())) { bool prop = is_constant(fn, get_and_name()); expr d_arg1 = m_ctx.whnf(app_arg(app_fn(d))); expr d_arg2 = m_ctx.whnf(app_arg(d)); - if (auto r = to_below(d_arg1, a, mk_fst(m_ctx, F, prop))) + if (auto r = to_below(d_arg1, a, mk_pprod_fst(m_ctx, F, prop))) return r; - else if (auto r = to_below(d_arg2, a, mk_snd(m_ctx, F, prop))) + else if (auto r = to_below(d_arg2, a, mk_pprod_snd(m_ctx, F, prop))) return r; else return none_expr(); @@ -660,11 +660,11 @@ struct structural_rec_fn { buffer args; expr const & fn = get_app_args(e, args); if (args.size() == 3) { - if (is_constant(fn, get_prod_fst_name())) { + if (is_constant(fn, get_pprod_fst_name())) { bool r = is_F_instance(args[2], path); path.push_back(1); return r; - } else if (is_constant(fn, get_prod_snd_name())) { + } else if (is_constant(fn, get_pprod_snd_name())) { bool r = is_F_instance(args[2], path); path.push_back(2); return r; @@ -788,7 +788,7 @@ struct structural_rec_fn { virtual expr visit_app(expr const & e) { buffer args; expr const & fn = get_app_args(e, args); - if (is_constant(fn, get_prod_fst_name()) && args.size() >= 3) { + if (is_constant(fn, get_pprod_fst_name()) && args.size() >= 3) { buffer path; if (is_F_instance(args[2], path)) { path.push_back(1); diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp index 0bf026694c..f07d891d4b 100644 --- a/src/library/inductive_compiler/basic.cpp +++ b/src/library/inductive_compiler/basic.cpp @@ -76,7 +76,7 @@ class add_basic_inductive_decl_fn { bool has_unit = has_poly_unit_decls(m_env); bool has_eq = has_eq_decls(m_env); bool has_heq = has_heq_decls(m_env); - bool has_prod = has_prod_decls(m_env); + bool has_prod = has_pprod_decls(m_env); bool gen_rec_on = get_inductive_rec_on(m_opts); bool gen_brec_on = get_inductive_brec_on(m_opts); diff --git a/src/library/inductive_compiler/mutual.cpp b/src/library/inductive_compiler/mutual.cpp index 18f654bb9a..00af5f01f3 100644 --- a/src/library/inductive_compiler/mutual.cpp +++ b/src/library/inductive_compiler/mutual.cpp @@ -66,11 +66,11 @@ class add_mutual_inductive_decl_fn { expr l = mk_local_for(ty); expr dom = binding_domain(ty); expr rest = Fun(l, to_sigma_type(instantiate(binding_body(ty), l))); - return mk_app(m_tctx, get_sigma_name(), {dom, rest}); + return mk_app(m_tctx, get_psigma_name(), {dom, rest}); } expr mk_sum(expr const & A, expr const & B) { - return mk_app(m_tctx, get_sum_name(), A, B); + return mk_app(m_tctx, get_psum_name(), A, B); } expr mk_sum(unsigned num_args, expr const * args) { @@ -108,8 +108,8 @@ class add_mutual_inductive_decl_fn { level l1 = get_level(m_tctx, A); level l2 = get_level(m_tctx, stype); stype = Fun(l, stype); - maker = mk_app(mk_constant(get_sigma_mk_name(), {l1, l2}), A, stype, l, maker); - stype = mk_app(m_tctx, get_sigma_name(), {A, stype}); + maker = mk_app(mk_constant(get_psigma_mk_name(), {l1, l2}), A, stype, l, maker); + stype = mk_app(m_tctx, get_psigma_name(), {A, stype}); } return mk_pair(Fun(locals, maker), stype); } @@ -133,7 +133,7 @@ class add_mutual_inductive_decl_fn { expr l = mk_local_pp("rest", mk_sum(m_index_types.size() - i, m_index_types.data() + i)); expr putter = l; for (unsigned j = i; j > 0; --j) { - putter = mk_app(m_tctx, get_sum_inr_name(), m_index_types[j-1], mk_sum(m_index_types.size() - j, m_index_types.data() + j), putter); + putter = mk_app(m_tctx, get_psum_inr_name(), m_index_types[j-1], mk_sum(m_index_types.size() - j, m_index_types.data() + j), putter); } return Fun(l, putter); } @@ -144,13 +144,13 @@ class add_mutual_inductive_decl_fn { expr putter; if (ind_idx == num_inds - 1) { - putter = mk_app(m_tctx, get_sum_inr_name(), m_index_types[ind_idx - 1], m_index_types[ind_idx], l); + putter = mk_app(m_tctx, get_psum_inr_name(), m_index_types[ind_idx - 1], m_index_types[ind_idx], l); ind_idx--; } else { - putter = mk_app(m_tctx, get_sum_inl_name(), m_index_types[ind_idx], mk_sum(num_inds - ind_idx - 1, m_index_types.data() + ind_idx + 1), l); + putter = mk_app(m_tctx, get_psum_inl_name(), m_index_types[ind_idx], mk_sum(num_inds - ind_idx - 1, m_index_types.data() + ind_idx + 1), l); } for (unsigned i = ind_idx; i > 0; --i) { - putter = mk_app(m_tctx, get_sum_inr_name(), m_index_types[i - 1], mk_sum(num_inds - i, m_index_types.data() + i), putter); + putter = mk_app(m_tctx, get_psum_inr_name(), m_index_types[i - 1], mk_sum(num_inds - i, m_index_types.data() + i), putter); } return Fun(l, putter); } @@ -445,8 +445,8 @@ class add_mutual_inductive_decl_fn { level l1 = get_level(m_tctx, A); level l2 = get_level(m_tctx, stype); stype = Fun(sarg, stype); - sigma = mk_app(mk_constant(get_sigma_mk_name(), {l1, l2}), A, stype, sarg, sigma); - stype = mk_app(m_tctx, get_sigma_name(), {A, stype}); + sigma = mk_app(mk_constant(get_psigma_mk_name(), {l1, l2}), A, stype, sarg, sigma); + stype = mk_app(m_tctx, get_psigma_name(), {A, stype}); } return sigma; } @@ -497,7 +497,7 @@ class add_mutual_inductive_decl_fn { minor_premise = Fun({a, b}, rest); } levels lvls = {motive_level, get_level(m_tctx, A), get_level(m_tctx, B)}; - return mk_app(mk_constant(get_sigma_cases_on_name(), lvls), {A, A_to_B, motive, major_premise, minor_premise}); + return mk_app(mk_constant(get_psigma_cases_on_name(), lvls), {A, A_to_B, motive, major_premise, minor_premise}); } expr unpack_sigma_and_apply_C(unsigned ind_idx, expr const & idx, expr const & C) { @@ -551,7 +551,7 @@ class add_mutual_inductive_decl_fn { } level l1 = get_level(m_tctx, A); level l2 = get_level(m_tctx, B); - return mk_app(mk_constant(get_sum_cases_on_name(), {motive_level, l1, l2}), {A, B, motive, index, case1, case2}); + return mk_app(mk_constant(get_psum_cases_on_name(), {motive_level, l1, l2}), {A, B, motive, index, case1, case2}); } expr construct_inner_C(expr const & C, unsigned ind_idx) { diff --git a/src/library/tactic/ac_tactics.cpp b/src/library/tactic/ac_tactics.cpp index 39c01955a0..f88bfbb518 100644 --- a/src/library/tactic/ac_tactics.cpp +++ b/src/library/tactic/ac_tactics.cpp @@ -247,10 +247,16 @@ struct perm_ac_fn : public flat_assoc_fn { return mk_app(m_comm, a, b); } + level dec_level(level const & l) { + if (auto r = ::lean::dec_level(l)) + return *r; + throw_failed(); + } + expr mk_left_comm(expr const & a, expr const & b, expr const & c) { if (!m_left_comm) { expr A = m_ctx.infer(a); - level lvl = get_level(m_ctx, A); + level lvl = dec_level(get_level(m_ctx, A)); m_left_comm = mk_app(mk_constant(get_left_comm_name(), {lvl}), A, m_op, m_comm, m_assoc); } return mk_app(*m_left_comm, a, b, c); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 24c1a6ede5..20c946f56a 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -1325,6 +1325,12 @@ lbool type_context::is_def_eq_core(level const & l1, level const & l2, bool part } } + if (l1.kind() != l2.kind() && (is_succ(l1) || is_succ(l2))) { + if (optional pred_l1 = dec_level(l1)) + if (optional pred_l2 = dec_level(l2)) + return is_def_eq_core(*pred_l1, *pred_l2, partial); + } + if (partial && (is_max_like(l1) || is_max_like(l2))) return l_undef; @@ -2341,7 +2347,7 @@ bool type_context::is_productive(expr const & e) { if (!is_constant(f)) return true; name const & n = const_name(f); - if (n == get_prod_fst_name()) { + if (n == get_pprod_fst_name()) { /* We use prod.fst when compiling recursive equations and brec_on. So, we should check whether the main argument of the projection is productive */ diff --git a/src/library/util.cpp b/src/library/util.cpp index 02bbf784ea..5561e16970 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -142,8 +142,8 @@ bool has_heq_decls(environment const & env) { return has_constructor(env, get_heq_refl_name(), get_heq_name(), 2); } -bool has_prod_decls(environment const & env) { - return has_constructor(env, get_prod_mk_name(), get_prod_name(), 4); +bool has_pprod_decls(environment const & env) { + return has_constructor(env, get_pprod_mk_name(), get_pprod_name(), 4); } bool has_lift_decls(environment const & env) { @@ -441,32 +441,32 @@ expr mk_unit_mk(level const & l) { return mk_constant(get_poly_unit_star_name(), {l}); } -expr mk_prod(abstract_type_context & ctx, expr const & A, expr const & B) { +expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B) { level l1 = get_level(ctx, A); level l2 = get_level(ctx, B); - return mk_app(mk_constant(get_prod_name(), {l1, l2}), A, B); + return mk_app(mk_constant(get_pprod_name(), {l1, l2}), A, B); } -expr mk_pair(abstract_type_context & ctx, expr const & a, expr const & b) { +expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b) { expr A = ctx.infer(a); expr B = ctx.infer(b); level l1 = get_level(ctx, A); level l2 = get_level(ctx, B); - return mk_app(mk_constant(get_prod_mk_name(), {l1, l2}), A, B, a, b); + return mk_app(mk_constant(get_pprod_mk_name(), {l1, l2}), A, B, a, b); } -expr mk_fst(abstract_type_context & ctx, expr const & p) { +expr mk_pprod_fst(abstract_type_context & ctx, expr const & p) { expr AxB = ctx.whnf(ctx.infer(p)); expr const & A = app_arg(app_fn(AxB)); expr const & B = app_arg(AxB); - return mk_app(mk_constant(get_prod_fst_name(), const_levels(get_app_fn(AxB))), A, B, p); + return mk_app(mk_constant(get_pprod_fst_name(), const_levels(get_app_fn(AxB))), A, B, p); } -expr mk_snd(abstract_type_context & ctx, expr const & p) { +expr mk_pprod_snd(abstract_type_context & ctx, expr const & p) { expr AxB = ctx.whnf(ctx.infer(p)); expr const & A = app_arg(app_fn(AxB)); expr const & B = app_arg(AxB); - return mk_app(mk_constant(get_prod_snd_name(), const_levels(get_app_fn(AxB))), A, B, p); + return mk_app(mk_constant(get_pprod_snd_name(), const_levels(get_app_fn(AxB))), A, B, p); } static expr * g_nat = nullptr; @@ -478,11 +478,11 @@ static expr * g_nat_add_fn = nullptr; static void initialize_nat() { g_nat = new expr(mk_constant(get_nat_name())); - g_nat_zero = new expr(mk_app(mk_constant(get_zero_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_zero_name())})); - g_nat_one = new expr(mk_app(mk_constant(get_one_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_one_name())})); - g_nat_bit0_fn = new expr(mk_app(mk_constant(get_bit0_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_add_name())})); - g_nat_bit1_fn = new expr(mk_app(mk_constant(get_bit1_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_one_name()), mk_constant(get_nat_has_add_name())})); - g_nat_add_fn = new expr(mk_app(mk_constant(get_add_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_add_name())})); + g_nat_zero = new expr(mk_app(mk_constant(get_zero_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_zero_name())})); + g_nat_one = new expr(mk_app(mk_constant(get_one_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_one_name())})); + g_nat_bit0_fn = new expr(mk_app(mk_constant(get_bit0_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_add_name())})); + g_nat_bit1_fn = new expr(mk_app(mk_constant(get_bit1_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_one_name()), mk_constant(get_nat_has_add_name())})); + g_nat_add_fn = new expr(mk_app(mk_constant(get_add_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_add_name())})); } static void finalize_nat() { @@ -529,17 +529,18 @@ static void finalize_char() { expr mk_unit(level const & l, bool prop) { return prop ? mk_true() : mk_unit(l); } expr mk_unit_mk(level const & l, bool prop) { return prop ? mk_true_intro() : mk_unit_mk(l); } -expr mk_prod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) { - return prop ? mk_and(a, b) : mk_prod(ctx, a, b); + +expr mk_pprod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) { + return prop ? mk_and(a, b) : mk_pprod(ctx, a, b); } -expr mk_pair(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) { - return prop ? mk_and_intro(ctx, a, b) : mk_pair(ctx, a, b); +expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) { + return prop ? mk_and_intro(ctx, a, b) : mk_pprod_mk(ctx, a, b); } -expr mk_fst(abstract_type_context & ctx, expr const & p, bool prop) { - return prop ? mk_and_elim_left(ctx, p) : mk_fst(ctx, p); +expr mk_pprod_fst(abstract_type_context & ctx, expr const & p, bool prop) { + return prop ? mk_and_elim_left(ctx, p) : mk_pprod_fst(ctx, p); } -expr mk_snd(abstract_type_context & ctx, expr const & p, bool prop) { - return prop ? mk_and_elim_right(ctx, p) : mk_snd(ctx, p); +expr mk_pprod_snd(abstract_type_context & ctx, expr const & p, bool prop) { + return prop ? mk_and_elim_right(ctx, p) : mk_pprod_snd(ctx, p); } bool is_ite(expr const & e) { diff --git a/src/library/util.h b/src/library/util.h index a2ce8dd43f..e1bed06f05 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -44,7 +44,7 @@ optional dec_level(level const & l); bool has_poly_unit_decls(environment const & env); bool has_eq_decls(environment const & env); bool has_heq_decls(environment const & env); -bool has_prod_decls(environment const & env); +bool has_pprod_decls(environment const & env); bool has_lift_decls(environment const & env); /** \brief Return true iff \c n is the name of a recursive datatype in \c env. @@ -167,18 +167,18 @@ expr mk_and_elim_right(abstract_type_context & ctx, expr const & H); expr mk_unit(level const & l); expr mk_unit_mk(level const & l); -expr mk_prod(abstract_type_context & ctx, expr const & A, expr const & B); -expr mk_pair(abstract_type_context & ctx, expr const & a, expr const & b); -expr mk_fst(abstract_type_context & ctx, expr const & p); -expr mk_snd(abstract_type_context & ctx, expr const & p); +expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B); +expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b); +expr mk_pprod_fst(abstract_type_context & ctx, expr const & p); +expr mk_pprod_snd(abstract_type_context & ctx, expr const & p); expr mk_unit(level const & l, bool prop); expr mk_unit_mk(level const & l, bool prop); -expr mk_prod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop); -expr mk_pair(abstract_type_context & ctx, expr const & a, expr const & b, bool prop); -expr mk_fst(abstract_type_context & ctx, expr const & p, bool prop); -expr mk_snd(abstract_type_context & ctx, expr const & p, bool prop); +expr mk_pprod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop); +expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b, bool prop); +expr mk_pprod_fst(abstract_type_context & ctx, expr const & p, bool prop); +expr mk_pprod_snd(abstract_type_context & ctx, expr const & p, bool prop); expr mk_nat_type(); bool is_nat_type(expr const & e); diff --git a/tests/lean/run/1163.lean b/tests/lean/run/1163.lean index fb53c8e85e..ee3374aa11 100644 --- a/tests/lean/run/1163.lean +++ b/tests/lean/run/1163.lean @@ -1,4 +1,4 @@ -inductive Foo : Type → Type* +inductive {u} Foo : Type → Type (u+1) | mk : Π (X : Type), Foo X | wrap : Π (X : Type), Foo X → Foo X diff --git a/tests/lean/run/1216.lean b/tests/lean/run/1216.lean index 714cb93043..d0db2c453c 100644 --- a/tests/lean/run/1216.lean +++ b/tests/lean/run/1216.lean @@ -1,6 +1,6 @@ open nat -inductive Vec (X : Type*) : ℕ → Type* +inductive {u} Vec (X : Type u) : ℕ → Type u | nil {} : Vec 0 | cons : X → Pi {n : nat}, Vec n → Vec (n + 1) diff --git a/tests/lean/run/apply4.lean b/tests/lean/run/apply4.lean index 615c844cf9..e3ea11c88b 100644 --- a/tests/lean/run/apply4.lean +++ b/tests/lean/run/apply4.lean @@ -5,7 +5,7 @@ constant foo {A : Type u} [inhabited A] (a b : A) : a = default A → a = b example (a b : nat) : a = 0 → a = b := by do intro `H, - apply (expr.const `foo [level.of_nat 1]), + apply (expr.const `foo [level.of_nat 0]), trace_state, assumption @@ -20,7 +20,7 @@ set_option pp.all false example (a b : nat) : a = 0 → a = b := by do intro `H, - apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 1]), + apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 0]), trace_state, a ← get_local `a, trace_state, @@ -45,6 +45,6 @@ by do example (a b : nat) : a = 0 → a = b := by do `[intro], - apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 1]), + apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 0]), `[exact inhabited.mk a], reflexivity diff --git a/tests/lean/run/cases_tac1.lean b/tests/lean/run/cases_tac1.lean index d0292886b9..8150cc1bd6 100644 --- a/tests/lean/run/cases_tac1.lean +++ b/tests/lean/run/cases_tac1.lean @@ -1,4 +1,4 @@ -inductive vec (A : Type*) : nat → Type* +inductive {u} vec (A : Type u) : nat → Type u | nil : vec 0 | cons : ∀ {n}, A → vec n → vec (n+1) diff --git a/tests/lean/run/coe_univ_bug.lean b/tests/lean/run/coe_univ_bug.lean index 60aa0e52ad..d947b33137 100644 --- a/tests/lean/run/coe_univ_bug.lean +++ b/tests/lean/run/coe_univ_bug.lean @@ -9,7 +9,7 @@ v + 1 universe variable u instance pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) := -⟨Type (max 1 u), (λ p : A → Prop, subtype p)⟩ +⟨Type u, (λ p : A → Prop, subtype p)⟩ instance coesubtype {A : Type u} {p : A → Prop} : has_coe (@coe_sort _ pred2subtype p) A := ⟨λ s, subtype.elt_of s⟩ diff --git a/tests/lean/run/compiler_bug3.lean b/tests/lean/run/compiler_bug3.lean index 705193fd64..9187b46c15 100644 --- a/tests/lean/run/compiler_bug3.lean +++ b/tests/lean/run/compiler_bug3.lean @@ -1,4 +1,4 @@ -inductive tree (A : Type*) +inductive {u} tree (A : Type u) : Type u | leaf : A -> tree | node : list tree -> tree diff --git a/tests/lean/run/e1.lean b/tests/lean/run/e1.lean index fffe74f7eb..b34bafa2d9 100644 --- a/tests/lean/run/e1.lean +++ b/tests/lean/run/e1.lean @@ -1,7 +1,7 @@ prelude -definition Prop : Type.{1} := Type.{0} +definition Prop : PType.{1} := PType.{0} constant eq : forall {A : Type}, A → A → Prop -constant N : Type.{1} +constant N : Type constants a b c : N infix `=`:50 := eq check a = b diff --git a/tests/lean/run/e5.lean b/tests/lean/run/e5.lean index d234c376ee..021620baf5 100644 --- a/tests/lean/run/e5.lean +++ b/tests/lean/run/e5.lean @@ -1,7 +1,7 @@ prelude -definition Prop := Type.{0} +definition Prop := PType.{0} -definition false : Prop := ∀x : Prop, x +definition false : Prop := ∀ x : Prop, x check false theorem false.elim (C : Prop) (H : false) : C diff --git a/tests/lean/run/elab3.lean b/tests/lean/run/elab3.lean index 9a5eb5ce8c..1a1da647da 100644 --- a/tests/lean/run/elab3.lean +++ b/tests/lean/run/elab3.lean @@ -1,3 +1,3 @@ set_option pp.binder_types true -axiom Sorry {A : Type*} : A +axiom Sorry {A : PType*} : A check (Sorry : ∀ a, a > 0) diff --git a/tests/lean/run/imp2.lean b/tests/lean/run/imp2.lean index 538d13aac8..49a8c8362d 100644 --- a/tests/lean/run/imp2.lean +++ b/tests/lean/run/imp2.lean @@ -1,4 +1,4 @@ -check (λ {A : Type.{1}} (a : A), a) (10:num) +check (λ {A : Type} (a : A), a) (10:num) set_option trace.app_builder true check (λ {A} (a : A), a) 10 check (λ a, a) (10:num) diff --git a/tests/lean/run/ind2.lean b/tests/lean/run/ind2.lean index a1daa10892..133a3b65c6 100644 --- a/tests/lean/run/ind2.lean +++ b/tests/lean/run/ind2.lean @@ -4,7 +4,7 @@ inductive nat : Type | succ : nat → nat namespace nat end nat open nat -inductive vector (A : Type*) : nat → Type* +inductive {u} vector (A : Type u) : nat → Type u | vnil : vector zero | vcons : Π {n : nat}, A → vector n → vector (succ n) namespace vector end vector open vector diff --git a/tests/lean/run/ind7.lean b/tests/lean/run/ind7.lean index 39d9d14366..55414098d3 100644 --- a/tests/lean/run/ind7.lean +++ b/tests/lean/run/ind7.lean @@ -1,5 +1,5 @@ namespace list - inductive list (A : Type*) : Type* + inductive {u} list (A : Type u) : Type u | nil : list | cons : A → list → list diff --git a/tests/lean/run/inductive_nonrec_after_rec.lean b/tests/lean/run/inductive_nonrec_after_rec.lean index 59e1170627..3136f1f087 100644 --- a/tests/lean/run/inductive_nonrec_after_rec.lean +++ b/tests/lean/run/inductive_nonrec_after_rec.lean @@ -66,6 +66,6 @@ begin {intros, unfold size, apply nat.zero_lt_succ } end -inductive tree_list (α : Type u) +inductive tree_list (α : Type u) : Type u | leaf : tree_list | node : list tree_list → α → tree_list diff --git a/tests/lean/run/match_expr.lean b/tests/lean/run/match_expr.lean index c86e784aea..6b2077ab8b 100644 --- a/tests/lean/run/match_expr.lean +++ b/tests/lean/run/match_expr.lean @@ -1,5 +1,5 @@ open tactic -axiom Sorry : ∀ {A:Type*}, A +axiom Sorry : ∀ {A:PType*}, A example (a b c : nat) (h₀ : c > 0) (h₁ : a > 1) (h₂ : b > 0) : a + b + c = 0 := by do diff --git a/tests/lean/run/nested_inductive.lean b/tests/lean/run/nested_inductive.lean index c1ffab3bde..3e6a9a2cac 100644 --- a/tests/lean/run/nested_inductive.lean +++ b/tests/lean/run/nested_inductive.lean @@ -1,34 +1,34 @@ set_option trace.inductive_compiler.nested.define.failure true set_option max_memory 1000000 -inductive vec (A : Type*) : nat -> Type* +inductive {u} vec (A : Type u) : nat -> Type u | vnil : vec 0 | vcons : Pi (n : nat), A -> vec n -> vec (n+1) namespace X1 print "simple" -inductive foo +inductive foo : Type | mk : list foo -> foo end X1 namespace X2 print "with param" -inductive foo (A : Type*) +inductive {u} foo (A : Type u) : Type u | mk : A -> list foo -> foo end X2 namespace X3 print "with indices" -inductive foo (A B : Type*) +inductive {u} foo (A B : Type u) : Type u | mk : A -> B -> vec foo 0 -> foo end X3 namespace X4 print "with locals in indices" -inductive foo (A : Type*) +inductive {u} foo (A : Type u) : Type u | mk : Pi (n : nat), A -> vec foo n -> foo end X4 diff --git a/tests/lean/run/noncomputable_example.lean b/tests/lean/run/noncomputable_example.lean index 680b56d862..646ff98e20 100644 --- a/tests/lean/run/noncomputable_example.lean +++ b/tests/lean/run/noncomputable_example.lean @@ -1,6 +1,6 @@ open classical sum - -noncomputable example (A : Type _) (h : (A → false) → false) : A := +universe variable u +noncomputable example (A : Type u) (h : (A → empty) → false) : A := match type_decidable A with | (inl ha) := ha | (inr hna) := false.rec _ (h hna) diff --git a/tests/lean/run/offset1.lean b/tests/lean/run/offset1.lean index 7e068bdda5..507970fb6c 100644 --- a/tests/lean/run/offset1.lean +++ b/tests/lean/run/offset1.lean @@ -1,6 +1,6 @@ open nat -inductive vec (α : Type*) : ℕ → Type* +inductive {u} vec (α : Type u) : ℕ → Type u | nil {} : vec 0 | cons : α → Π {n : nat}, vec n → vec (n+1) diff --git a/tests/lean/run/pred_to_subtype_coercion.lean b/tests/lean/run/pred_to_subtype_coercion.lean index d1c560240f..d9716ac190 100644 --- a/tests/lean/run/pred_to_subtype_coercion.lean +++ b/tests/lean/run/pred_to_subtype_coercion.lean @@ -2,7 +2,7 @@ universe variables u attribute [instance] definition pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) := -⟨Type (max 1 u), λ p : A → Prop, subtype p⟩ +⟨Type u, λ p : A → Prop, subtype p⟩ definition below (n : nat) : nat → Prop := λ i, i < n diff --git a/tests/lean/run/record9.lean b/tests/lean/run/record9.lean index 3cf0c476dd..c32c2d56ea 100644 --- a/tests/lean/run/record9.lean +++ b/tests/lean/run/record9.lean @@ -1,6 +1,6 @@ -constant fibrant : Type* → Prop +constant {u} fibrant : Type u → Prop -structure Fib : Type* := -{type : Type*} (pred : fibrant type) +structure {u} Fib : Type (u+1) := +{type : Type u} (pred : fibrant type) check Fib.mk diff --git a/tests/lean/run/simple.lean b/tests/lean/run/simple.lean index 7073a17c34..42e1ed54e3 100644 --- a/tests/lean/run/simple.lean +++ b/tests/lean/run/simple.lean @@ -1,7 +1,7 @@ prelude -definition Prop : Type.{1} := Type.{0} +definition Prop : PType.{1} := PType.{0} section - parameter A : Type* + parameter A : PType* definition Eq (a b : A) : Prop := ∀P : A → Prop, P a → P b diff --git a/tests/lean/run/t9.lean b/tests/lean/run/t9.lean index 5d0b77409b..ba384ad284 100644 --- a/tests/lean/run/t9.lean +++ b/tests/lean/run/t9.lean @@ -1,5 +1,5 @@ prelude -definition bool : Type.{1} := Type.{0} +definition bool : PType 1 := PType 0 definition and (p q : bool) : bool := ∀ c : bool, (p → q → c) → c infixl `∧`:25 := and