From 18313bfab056b20ee38b0340cd2ae2e76afa73b2 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 10 Feb 2017 12:04:08 -0500 Subject: [PATCH] feat(hott): make Type.{0} impredicative Warnings: - no_confusion is not generated, which means that injection and cases tactics might not work - there are some sorry's in the init folder - most files out of the init folder don't compile --- hott/init/datatypes.hlean | 23 +++++++++++-------- hott/init/funext.hlean | 2 +- hott/init/logic.hlean | 10 ++++---- hott/init/nat.hlean | 34 ++++++++++++---------------- hott/init/trunc.hlean | 6 ++--- hott/init/wf.hlean | 25 ++++++++++---------- library/init/subtype.lean | 2 ++ src/frontends/lean/builtin_cmds.cpp | 4 ++-- src/frontends/lean/inductive_cmd.cpp | 14 ++++++++---- src/frontends/lean/structure_cmd.cpp | 2 ++ src/kernel/inductive/inductive.cpp | 23 +++++++++++-------- src/library/hott_kernel.cpp | 2 +- 12 files changed, 78 insertions(+), 69 deletions(-) diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean index 7e626f8ac..cb70ac592 100644 --- a/hott/init/datatypes.hlean +++ b/hott/init/datatypes.hlean @@ -28,7 +28,7 @@ refl : eq a a structure lift.{l₁ l₂} (A : Type.{l₁}) : Type.{max l₁ l₂} := up :: (down : A) -inductive prod (A B : Type) := +inductive prod.{u v} (A : Type.{u}) (B : Type.{v}) : Type.{max u v} := mk : A → B → prod A B definition prod.pr1 [reducible] [unfold 3] {A B : Type} (p : prod A B) : A := @@ -39,7 +39,7 @@ prod.rec (λ a b, b) p definition prod.destruct [reducible] := @prod.cases_on -inductive sum (A B : Type) : Type := +inductive sum.{u v} (A : Type.{u}) (B : Type.{v}) : Type.{max u v} := | inl {} : A → sum A B | inr {} : B → sum A B @@ -49,7 +49,7 @@ sum.inl a definition sum.intro_right [reducible] (A : Type) {B : Type} (b : B) : sum A B := sum.inr b -inductive sigma {A : Type} (B : A → Type) := +inductive sigma.{u v} {A : Type.{u}} (B : A → Type.{v}) : Type.{max u v} := mk : Π (a : A), B a → sigma B definition sigma.pr1 [reducible] [unfold 3] {A : Type} {B : A → Type} (p : sigma B) : A := @@ -61,7 +61,7 @@ sigma.rec (λ a b, b) p -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26. -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))). -- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc). -inductive pos_num : Type := +inductive pos_num : Type₀ := | one : pos_num | bit1 : pos_num → pos_num | bit0 : pos_num → pos_num @@ -71,7 +71,7 @@ namespace pos_num pos_num.rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n) end pos_num -inductive num : Type := +inductive num : Type₀ := | zero : num | pos : pos_num → num @@ -81,18 +81,18 @@ namespace num num.rec_on a (pos one) (λp, pos (succ p)) end num -inductive bool : Type := +inductive bool : Type₀ := | ff : bool | tt : bool -inductive char : Type := +inductive char : Type₀ := mk : bool → bool → bool → bool → bool → bool → bool → bool → char -inductive string : Type := +inductive string : Type₀ := | empty : string | str : char → string → string -inductive option (A : Type) : Type := +inductive option.{u} (A : Type.{u}) : Type.{u} := | none {} : option A | some : A → option A @@ -100,6 +100,9 @@ inductive option (A : Type) : Type := -- We do that because we want 0 instead of nat.zero in these eliminators. set_option inductive.rec_on false set_option inductive.cases_on false -inductive nat := +inductive nat : Type₀ := | zero : nat | succ : nat → nat + +set_option pp.universes true +print prod diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean index 3037b04d0..57b1e04f5 100644 --- a/hott/init/funext.hlean +++ b/hott/init/funext.hlean @@ -63,7 +63,7 @@ section have t1 : Πx, is_contr (Σ y, f x = y), from (λx, !is_contr_sigma_eq), have t2 : is_contr (Πx, Σ y, f x = y), - from !wf, + from sorry, have t3 : (λ x, @sigma.mk _ (λ y, f x = y) (f x) idp) = s g h, from @eq_of_is_contr (Π x, Σ y, f x = y) t2 _ _, have t4 : r (λ x, sigma.mk (f x) idp) = r (s g h), diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index e7ec11291..07f546dd3 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -25,7 +25,7 @@ assume Ha : a, absurd (H₁ Ha) H₂ definition not_empty : ¬empty := assume H : empty, H -definition non_contradictory (a : Type) : Type := ¬¬a +definition non_contradictory (a : Type) : Type₀ := ¬¬a definition non_contradictory_intro {a : Type} (Ha : a) : ¬¬a := assume Hna : ¬a, absurd Ha Hna @@ -498,13 +498,13 @@ definition decidable_ne [instance] {A : Type} [H : decidable_eq A] (a b : A) : d decidable_implies namespace bool - theorem ff_ne_tt : ff = tt → empty - | [none] + theorem ff_ne_tt : ff = tt → empty := + sorry end bool open bool -definition is_dec_eq {A : Type} (p : A → A → bool) : Type := Π ⦃x y : A⦄, p x y = tt → x = y -definition is_dec_refl {A : Type} (p : A → A → bool) : Type := Πx, p x x = tt +definition is_dec_eq {A : Type} (p : A → A → bool) : Type := Π ⦃x y : A⦄, p x y = tt → x = y +definition is_dec_refl {A : Type} (p : A → A → bool) : Type₀ := Πx, p x x = tt open decidable protected definition bool.has_decidable_eq [instance] : Πa b : bool, decidable (a = b) diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index be8aff41a..ac9031e38 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -26,22 +26,16 @@ namespace nat protected definition no_confusion_type.{u} [reducible] (P : Type.{u}) (v₁ v₂ : ℕ) : Type.{u} := nat.rec - (nat.rec - (P → lift P) - (λ a₂ ih, lift P) - v₂) - (λ a₁ ih, nat.rec - (lift P) - (λ a₂ ih, (a₁ = a₂ → P) → lift P) - v₂) + (nat.rec (P → P) (λ a₂ ih, P) v₂) + (λ a₁ ih, nat.rec P (λ a₂ ih, (a₁ = a₂ → P) → P) v₂) v₁ protected definition no_confusion [reducible] [unfold 4] {P : Type} {v₁ v₂ : ℕ} (H : v₁ = v₂) : nat.no_confusion_type P v₁ v₂ := - eq.rec (λ H₁ : v₁ = v₁, nat.rec (λ h, lift.up h) (λ a ih h, lift.up (h (eq.refl a))) v₁) H H + eq.rec (λ H₁ : v₁ = v₁, nat.rec (λ h, h) (λa ih h, h rfl) v₁) H H /- basic definitions on natural numbers -/ - inductive le (a : ℕ) : ℕ → Type := + inductive le (a : ℕ) : ℕ → Type₀ := | nat_refl : le a a -- use nat_refl to avoid overloading le.refl | step : Π {b}, le a b → le a (succ b) @@ -75,15 +69,15 @@ namespace nat protected definition is_inhabited [instance] : inhabited nat := inhabited.mk zero - protected definition has_decidable_eq [instance] [priority nat.prio] : Π x y : nat, decidable (x = y) - | has_decidable_eq zero zero := inl rfl - | has_decidable_eq (succ x) zero := inr (by contradiction) - | has_decidable_eq zero (succ y) := inr (by contradiction) - | has_decidable_eq (succ x) (succ y) := - match has_decidable_eq x y with - | inl xeqy := inl (by rewrite xeqy) - | inr xney := inr (λ h : succ x = succ y, by injection h with xeqy; exact absurd xeqy xney) - end + protected definition has_decidable_eq [instance] [priority nat.prio] : Π x y : nat, decidable (x = y) := sorry + -- | has_decidable_eq zero zero := inl rfl + -- | has_decidable_eq (succ x) zero := inr (by contradiction) + -- | has_decidable_eq zero (succ y) := inr (by contradiction) + -- | has_decidable_eq (succ x) (succ y) := + -- match has_decidable_eq x y with + -- | inl xeqy := inl (by rewrite xeqy) + -- | inr xney := inr (λ h : succ x = succ y, by injection h with xeqy; exact absurd xeqy xney) + -- end /- properties of inequality -/ @@ -121,7 +115,7 @@ namespace nat nat.cases_on n le.step (λa, succ_le_succ) theorem not_succ_le_zero (n : ℕ) : ¬succ n ≤ 0 := - by intro H; cases H + sorry --by intro H; cases H theorem succ_le_zero_iff_empty (n : ℕ) : succ n ≤ 0 ↔ empty := iff_empty_intro !not_succ_le_zero diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 4b5ebb4e4..0b234d7ec 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -58,7 +58,7 @@ namespace trunc_index /- we give a weird name to the reflexivity step to avoid overloading le.refl (which can be used if types.trunc is imported) -/ - inductive le (a : ℕ₋₂) : ℕ₋₂ → Type := + inductive le (a : ℕ₋₂) : ℕ₋₂ → Type₀ := | tr_refl : le a a | step : Π {b}, le a b → le a (b.+1) @@ -105,7 +105,7 @@ namespace is_trunc use `is_trunc` and `is_contr` -/ - structure contr_internal (A : Type) := + structure contr_internal (A : Type) : Type := (center : A) (center_eq : Π(a : A), center = a) @@ -354,7 +354,7 @@ namespace is_trunc end is_trunc -structure trunctype (n : ℕ₋₂) := +structure trunctype (n : ℕ₋₂) : Type := (carrier : Type) (struct : is_trunc n carrier) diff --git a/hott/init/wf.hlean b/hott/init/wf.hlean index 82c688a6e..a4c285efc 100644 --- a/hott/init/wf.hlean +++ b/hott/init/wf.hlean @@ -163,18 +163,19 @@ namespace nat -- less-than is well-founded definition lt.wf [instance] : well_founded (lt : ℕ → ℕ → Type₀) := - begin - constructor, intro n, induction n with n IH, - { constructor, intros n H, exfalso, exact !not_lt_zero H}, - { constructor, intros m H, - have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, - begin - intros n₁ hlt, induction hlt, - { intro p, injection p with q, exact q ▸ IH}, - { intro p, injection p with q, exact (acc.inv (q ▸ IH) a)} - end, - apply aux H rfl}, - end + sorry + -- begin + -- constructor, intro n, induction n with n IH, + -- { constructor, intros n H, exfalso, exact !not_lt_zero H}, + -- { constructor, intros m H, + -- have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, + -- begin + -- intros n₁ hlt, induction hlt, + -- { intro p, injection p with q, exact q ▸ IH}, + -- { intro p, injection p with q, exact (acc.inv (q ▸ IH) a)} + -- end, + -- apply aux H rfl}, + -- end definition measure {A : Type} : (A → ℕ) → A → A → Type₀ := inv_image lt diff --git a/library/init/subtype.lean b/library/init/subtype.lean index a6304f512..6e845eb54 100644 --- a/library/init/subtype.lean +++ b/library/init/subtype.lean @@ -11,6 +11,8 @@ set_option structure.proj_mk_thm true structure subtype {A : Type} (P : A → Prop) := tag :: (elt_of : A) (has_property : P elt_of) +print prefix subtype +set_option pp.universes true namespace subtype notation `{` binder ` | ` r:(scoped:1 P, subtype P) `}` := r diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 224592fb6..e5d5193b6 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -479,8 +479,8 @@ static environment init_quotient_cmd(parser & p) { } static environment init_hits_cmd(parser & p) { - if (p.env().prop_proof_irrel() || p.env().impredicative()) - throw parser_error("invalid init_hits command, this command is only available for proof relevant and predicative kernels", p.cmd_pos()); + if (p.env().prop_proof_irrel()) + throw parser_error("invalid init_hits command, this command is only available for proof relevant kernels", p.cmd_pos()); return module::declare_hits(p.env()); } diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 2c1d1b22e..3e17f1377 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -484,7 +484,7 @@ struct inductive_cmd_fn { throw_error("resultant universe must be provided, when using explicit universe levels"); type = update_result_sort(type, m_u); m_infer_result_universe = true; - } else if (m_env.impredicative() && !is_zero(l) && !is_not_zero(l)) { + } else if (m_env.impredicative() && m_env.prop_proof_irrel() && !is_zero(l) && !is_not_zero(l)) { // If the resultant universe can be Prop for some parameter instantiations, then // the kernel will produce an eliminator that only eliminates to Prop. // There is on exception the singleton case. We perform a concervative check here, @@ -809,7 +809,7 @@ struct inductive_cmd_fn { env = mk_rec_on(env, n); save_def_info(name(n, "rec_on"), pos); } - if (gen_rec_on && env.impredicative()) { + if (gen_rec_on && env.impredicative() && m_env.prop_proof_irrel()) { env = mk_induction_on(env, n); save_def_info(name(n, "induction_on"), pos); } @@ -818,12 +818,15 @@ struct inductive_cmd_fn { env = mk_cases_on(env, n); save_def_info(name(n, "cases_on"), pos); } - if (gen_cases_on && gen_no_confusion && has_eq && ((env.prop_proof_irrel() && has_heq) || (!env.prop_proof_irrel() && has_lift))) { + if (gen_cases_on && gen_no_confusion && has_eq && env.prop_proof_irrel() && has_heq) { + // if (gen_cases_on && gen_no_confusion && has_eq && ((env.prop_proof_irrel() && has_heq) || (!env.prop_proof_irrel() && has_lift))) { + // TODO: we are skipping no_confusion if impredicative HoTT env = mk_no_confusion(env, n); save_if_defined(name{n, "no_confusion_type"}, pos); save_if_defined(name(n, "no_confusion"), pos); } - if (gen_brec_on && has_prod) { + if (gen_brec_on && has_prod && env.prop_proof_irrel()) { + // TODO: we are skipping below if impredicative HoTT env = mk_below(env, n); save_if_defined(name{n, "below"}, pos); if (env.impredicative()) { @@ -836,7 +839,8 @@ struct inductive_cmd_fn { for (inductive_decl const & d : decls) { name const & n = inductive_decl_name(d); pos_info pos = *m_decl_pos_map.find(n); - if (gen_brec_on && has_unit && has_prod) { + if (gen_brec_on && has_unit && has_prod && env.prop_proof_irrel()) { + // TODO: we are skipping brec_on if impredicative HoTT env = mk_brec_on(env, n); save_if_defined(name{n, "brec_on"}, pos); if (env.impredicative()) { diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index d53718e97..edc4a43ca 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -926,6 +926,8 @@ struct structure_cmd_fn { return; if (!m_env.impredicative() && !has_lift_decls(m_env)) return; + if (!m_env.prop_proof_irrel()) + return; // TODO: we are skipping no_confusion if impredicative HoTT m_env = mk_no_confusion(m_env, m_name); name no_confusion_name(m_name, "no_confusion"); save_def_info(no_confusion_name); diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 7f2c6c0d0..eadbf47f0 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -349,11 +349,12 @@ struct add_inductive_fn { if (i != m_num_params) throw kernel_exception(m_env, "number of parameters mismatch in inductive datatype declaration"); t = tc().ensure_sort(t).first; - if (m_env.impredicative()) { - // If the environment is impredicative, we track whether the resultant universe - // is never zero (under any parameter assignment). - // TODO(Leo): when the resultant universe may be 0 and not zero depending on parameter assignment, - // we may generate two recursors: one when it is 0, and another one when it is not. + if (m_env.impredicative() && m_env.prop_proof_irrel()) { + // If the environment is impredicative and proof irrelevant, we track whether the + // resultant universe is never zero (under any parameter assignment). TODO(Leo): + // when the resultant universe may be 0 and not zero depending on parameter + // assignment, we may generate two recursors: one when it is 0, and another one when + // it is not. if (first) { m_is_not_zero = is_not_zero(sort_level(t)); } else { @@ -467,7 +468,7 @@ struct add_inductive_fn { // the sort is ok IF // 1- its level is <= inductive datatype level, OR // 2- m_env is impredicative and inductive datatype is at level 0 - if (!(is_geq(m_it_levels[d_idx], sort_level(s)) || (is_zero(m_it_levels[d_idx]) && m_env.impredicative()))) + if (!(is_geq(m_it_levels[d_idx], sort_level(s)) || (is_zero(m_it_levels[d_idx]) && m_env.impredicative() && m_env.prop_proof_irrel()))) throw kernel_exception(m_env, sstream() << "universe level of type_of(arg #" << (i + 1) << ") " << "of '" << n << "' is too big for the corresponding inductive datatype"); check_positivity(binding_domain(t), n, i); @@ -522,9 +523,10 @@ struct add_inductive_fn { /** \brief Return true if type formers C in the recursors can only map to Type.{0} */ bool elim_only_at_universe_zero() { - if (!m_env.impredicative() || m_is_not_zero) { - // If Type.{0} is not impredicative or the resultant inductive datatype is not in Type.{0}, - // then the recursor may return Type.{l} where l is a universe level parameter. + if (!m_env.impredicative() || !m_env.prop_proof_irrel() || m_is_not_zero) { + // If Type.{0} is not impredicative or not proof irrelevant or the resultant inductive + // datatype is not in Type.{0}, then the recursor may return Type.{l} where l is a + // universe level parameter. return false; } if (get_num_its() > 1) @@ -575,7 +577,8 @@ struct add_inductive_fn { /** \brief Initialize m_elim_level. */ void mk_elim_level() { if (elim_only_at_universe_zero()) { - // environment is impredicative, datatype maps to Prop, we have more than one introduction rule. + // environment is impredicative and proof irrelevant, datatype maps to Prop, we have + // more than one introduction rule. m_elim_level = mk_level_zero(); } else { name l("l"); diff --git a/src/library/hott_kernel.cpp b/src/library/hott_kernel.cpp index 96e3123a5..8ca82fad2 100644 --- a/src/library/hott_kernel.cpp +++ b/src/library/hott_kernel.cpp @@ -15,7 +15,7 @@ environment mk_hott_environment(unsigned trust_lvl) { environment env = environment(trust_lvl, false /* Type.{0} is not proof irrelevant */, true /* Eta */, - false /* Type.{0} is not impredicative */, + true /* Type.{0} is impredicative */, /* builtin support for inductive and hits */ compose(std::unique_ptr(new inductive_normalizer_extension()), std::unique_ptr(new hits_normalizer_extension())));