michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hott): make Type.{0} impredicative

Browse source 
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
This commit is contained in:
Floris van Doorn 2017-02-10 12:04:08 -05:00
parent 5eafb1f6b2
commit 18313bfab0
12 changed files with 78 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
hott/init/datatypes.hlean
View file

@ -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

2
hott/init/funext.hlean
View file

@ -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),

8
hott/init/logic.hlean
View file

@ -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_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)

34
hott/init/nat.hlean
View file

@ -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

6
hott/init/trunc.hlean
View file

@ -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)

25
hott/init/wf.hlean
View file

@ -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

2
library/init/subtype.lean
View file

@ -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

4
src/frontends/lean/builtin_cmds.cpp
View file

@ -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());
}

14
src/frontends/lean/inductive_cmd.cpp
View file

@ -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()) {

2
src/frontends/lean/structure_cmd.cpp
View file

@ -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);

23
src/kernel/inductive/inductive.cpp
View file

@ -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");

2
src/library/hott_kernel.cpp
View file

@ -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<normalizer_extension>(new inductive_normalizer_extension()),
std::unique_ptr<normalizer_extension>(new hits_normalizer_extension())));