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

feat(datatypes): let the type of unit be the lowest non-Prop universe

Browse source 
The definitional package (brec_on and cases_on) now use poly_unit instead of unit

closes #698
This commit is contained in:
Floris van Doorn 2015-06-24 17:59:17 -04:00 committed by Leonardo de Moura
parent a0461262d0
commit fa1979c128
20 changed files with 63 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/category/groupoid.hlean
View file

@ -66,7 +66,7 @@ namespace category
end
-- Conversely we can turn each group into a groupoid on the unit type
definition groupoid_of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{l l} unit :=
definition groupoid_of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{0 l} unit :=
begin
fapply groupoid.mk, fapply precategory.mk,
intros, exact A,

2
hott/hit/suspension.hlean
View file

@ -10,7 +10,7 @@ import .pushout types.pointed
open pushout unit eq equiv equiv.ops pointed
definition suspension (A : Type) : Type := pushout (λ(a : A), star.{0}) (λ(a : A), star.{0})
definition suspension (A : Type) : Type := pushout (λ(a : A), star) (λ(a : A), star)
namespace suspension
variable {A : Type}

5
hott/init/datatypes.hlean
View file

@ -14,7 +14,10 @@ notation `Type₁` := Type.{1}
notation `Type₂` := Type.{2}
notation `Type₃` := Type.{3}
inductive unit.{l} : Type.{l} :=
inductive poly_unit.{l} : Type.{l} :=
star : poly_unit
inductive unit : Type₀ :=
star : unit
inductive empty : Type₀

7
hott/init/equiv.hlean
View file

@ -8,7 +8,7 @@ Ported from Coq HoTT
prelude
import .path .function
open eq function
open eq function lift
/- Equivalences -/
@ -140,6 +140,9 @@ namespace is_equiv
end
definition is_equiv_up [instance] (A : Type) : is_equiv (up : A → lift A) :=
adjointify up down (λa, by induction a;reflexivity) (λa, idp)
section
variables {A B C : Type} (f : A → B) {f' : A → B} [Hf : is_equiv f] (g : B → C)
include Hf
@ -293,6 +296,8 @@ namespace equiv
definition equiv_of_equiv_of_eq {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▸ q
definition equiv_of_eq_of_equiv {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q ▸ p
definition equiv_lift (A : Type) : A ≃ lift A := equiv.mk up _
namespace ops
postfix `⁻¹` := equiv.symm -- overloaded notation for inverse
end ops

21
hott/init/funext.hlean
View file

@ -8,7 +8,7 @@ Ported from Coq HoTT
prelude
import .trunc .equiv .ua
open eq is_trunc sigma function is_equiv equiv prod unit prod.ops
open eq is_trunc sigma function is_equiv equiv prod unit prod.ops lift
/-
We now prove that funext follows from a couple of weaker-looking forms
@ -208,24 +208,21 @@ end
-- implies (with dependent eta) also the strong dependent funext.
theorem weak_funext_of_ua : weak_funext :=
(λ (A : Type) (P : A → Type) allcontr,
let U := (λ (x : A), unit) in
have pequiv : Π (x : A), P x ≃ U x,
let U := (λ (x : A), lift unit) in
have pequiv : Π (x : A), P x ≃ unit,
from (λ x, @equiv_unit_of_is_contr (P x) (allcontr x)),
have psim : Π (x : A), P x = U x,
from (λ x, @is_equiv.inv _ _
equiv_of_eq (univalence _ _) (pequiv x)),
from (λ x, eq_of_equiv_lift (pequiv x)),
have p : P = U,
from @nondep_funext_from_ua A Type P U psim,
have tU' : is_contr (A → unit),
from is_contr.mk (λ x, ⋆)
(λ f, @nondep_funext_from_ua A unit (λ x, ⋆) f
(λ x, unit.rec_on (f x) idp)),
have tU' : is_contr (A → lift unit),
from is_contr.mk (λ x, up ⋆)
(λ f, nondep_funext_from_ua (λa, by induction (f a) with u;induction u;reflexivity)),
have tU : is_contr (Π x, U x),
from tU',
have tlast : is_contr (Πx, P x),
from eq.transport _ p⁻¹ tU,
tlast
)
from p⁻¹ ▸ tU,
tlast)
-- In the following we will proof function extensionality using the univalence axiom
definition funext_of_ua : funext :=

3
hott/init/ua.hlean
View file

@ -46,7 +46,8 @@ ap10 (cast_ua_fn f) a
definition ua_equiv_of_eq [reducible] {A B : Type} (p : A = B) : ua (equiv_of_eq p) = p :=
left_inv equiv_of_eq p
definition eq_of_equiv_lift {A B : Type} (f : A ≃ B) : A = lift B :=
ua (f ⬝e !equiv_lift)
namespace equiv
-- One consequence of UA is that we can transport along equivalencies of types

7
library/init/datatypes.lean
View file

@ -16,7 +16,10 @@ notation `Type₃` := Type.{3}
set_option structure.eta_thm true
set_option structure.proj_mk_thm true
inductive unit.{l} : Type.{l} :=
inductive poly_unit.{l} : Type.{l} :=
star : poly_unit
inductive unit : Type₁ :=
star : unit
inductive true : Prop :=
@ -24,7 +27,7 @@ intro : true
inductive false : Prop
inductive empty : Type
inductive empty : Type₁
inductive eq {A : Type} (a : A) : A → Prop :=
refl : eq a a

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

@ -726,7 +726,7 @@ struct inductive_cmd_fn {
}
environment mk_aux_decls(environment env, buffer<inductive_decl> const & decls) {
bool has_unit = has_unit_decls(env);
bool has_unit = has_poly_unit_decls(env);
bool has_eq = has_eq_decls(env);
bool has_heq = has_heq_decls(env);
bool has_prod = has_prod_decls(env);

16
src/library/constants.cpp
View file

@ -140,8 +140,8 @@ name const * g_true = nullptr;
name const * g_true_intro = nullptr;
name const * g_is_trunc_is_hset = nullptr;
name const * g_is_trunc_is_hprop = nullptr;
name const * g_unit = nullptr;
name const * g_unit_star = nullptr;
name const * g_poly_unit = nullptr;
name const * g_poly_unit_star = nullptr;
name const * g_well_founded = nullptr;
void initialize_constants() {
g_absurd = new name{"absurd"};
@ -281,8 +281,8 @@ void initialize_constants() {
g_true_intro = new name{"true", "intro"};
g_is_trunc_is_hset = new name{"is_trunc", "is_hset"};
g_is_trunc_is_hprop = new name{"is_trunc", "is_hprop"};
g_unit = new name{"unit"};
g_unit_star = new name{"unit", "star"};
g_poly_unit = new name{"poly_unit"};
g_poly_unit_star = new name{"poly_unit", "star"};
g_well_founded = new name{"well_founded"};
}
void finalize_constants() {
@ -423,8 +423,8 @@ void finalize_constants() {
delete g_true_intro;
delete g_is_trunc_is_hset;
delete g_is_trunc_is_hprop;
delete g_unit;
delete g_unit_star;
delete g_poly_unit;
delete g_poly_unit_star;
delete g_well_founded;
}
name const & get_absurd_name() { return *g_absurd; }
@ -564,7 +564,7 @@ name const & get_true_name() { return *g_true; }
name const & get_true_intro_name() { return *g_true_intro; }
name const & get_is_trunc_is_hset_name() { return *g_is_trunc_is_hset; }
name const & get_is_trunc_is_hprop_name() { return *g_is_trunc_is_hprop; }
name const & get_unit_name() { return *g_unit; }
name const & get_unit_star_name() { return *g_unit_star; }
name const & get_poly_unit_name() { return *g_poly_unit; }
name const & get_poly_unit_star_name() { return *g_poly_unit_star; }
name const & get_well_founded_name() { return *g_well_founded; }
}

4
src/library/constants.h
View file

@ -142,7 +142,7 @@ name const & get_true_name();
name const & get_true_intro_name();
name const & get_is_trunc_is_hset_name();
name const & get_is_trunc_is_hprop_name();
name const & get_unit_name();
name const & get_unit_star_name();
name const & get_poly_unit_name();
name const & get_poly_unit_star_name();
name const & get_well_founded_name();
}

4
src/library/definitional/cases_on.cpp
View file

@ -83,8 +83,8 @@ environment mk_cases_on(environment const & env, name const & n) {
optional<expr> star;
// we use unit if num_types > 1
if (num_types > 1) {
unit = mk_constant(get_unit_name(), to_list(elim_univ));
star = mk_constant(get_unit_star_name(), to_list(elim_univ));
unit = mk_constant(get_poly_unit_name(), to_list(elim_univ));
star = mk_constant(get_poly_unit_star_name(), to_list(elim_univ));
}
// rec_params order

4
src/library/definitional/equations.cpp
View file

@ -1663,7 +1663,7 @@ class equation_compiler_fn {
C = Fun(C_args, type);
} else {
expr d = binding_domain(C_type);
expr unit = mk_constant(get_unit_name(), rlvl);
expr unit = mk_constant(get_poly_unit_name(), rlvl);
to_telescope_ext(d, C_args);
C = Fun(C_args, unit);
}
@ -1706,7 +1706,7 @@ class equation_compiler_fn {
new_ctx.append(rest);
F = compile_pat_match(program(prg_i, to_list(new_ctx)), *p_idx);
} else {
expr star = mk_constant(get_unit_star_name(), rlvl);
expr star = mk_constant(get_poly_unit_star_name(), rlvl);
buffer<expr> F_args;
F_args.append(C_args);
below = mk_app(below, F_args);

8
src/library/util.cpp
View file

@ -97,8 +97,8 @@ bool has_constructor(environment const & env, name const & c, name const & I, un
return is_constant(type) && const_name(type) == I;
}
bool has_unit_decls(environment const & env) {
return has_constructor(env, get_unit_star_name(), get_unit_name(), 0);
bool has_poly_unit_decls(environment const & env) {
return has_constructor(env, get_poly_unit_star_name(), get_poly_unit_name(), 0);
}
bool has_eq_decls(environment const & env) {
@ -408,11 +408,11 @@ expr mk_and_elim_right(type_checker & tc, expr const & H) {
}
expr mk_unit(level const & l) {
return mk_constant(get_unit_name(), {l});
return mk_constant(get_poly_unit_name(), {l});
}
expr mk_unit_mk(level const & l) {
return mk_constant(get_unit_star_name(), {l});
return mk_constant(get_poly_unit_star_name(), {l});
}
expr mk_prod(type_checker & tc, expr const & A, expr const & B) {

6
src/library/util.h
View file

@ -33,7 +33,7 @@ bool is_standard(environment const & env);
*/
bool is_norm_pi(type_checker & tc, expr & e, constraint_seq & cs);
bool has_unit_decls(environment const & env);
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);
@ -117,8 +117,8 @@ expr mk_and_intro(type_checker & tc, expr const & Ha, expr const & Hb);
expr mk_and_elim_left(type_checker & tc, expr const & H);
expr mk_and_elim_right(type_checker & tc, expr const & H);
expr mk_unit(level const & l);
expr mk_unit_mk(level const & l);
expr mk_poly_unit(level const & l);
expr mk_poly_unit_mk(level const & l);
expr mk_prod(type_checker & tc, expr const & A, expr const & B);
expr mk_pair(type_checker & tc, expr const & a, expr const & b);
expr mk_pr1(type_checker & tc, expr const & p);

2
tests/lean/run/fib_brec.lean
View file

@ -6,7 +6,7 @@ namespace nat
definition brec_on {C : nat → Type} (n : nat) (F : Π (n : nat), @nat.below C n → C n) : C n :=
have general : C n × @nat.below C n, from
nat.rec_on n
(pair (F zero unit.star) unit.star)
(pair (F zero poly_unit.star) poly_unit.star)
(λ (n₁ : nat) (r₁ : C n₁ × @nat.below C n₁),
have b : @nat.below C (succ n₁), from
r₁,

10
tests/lean/run/forest.lean
View file

@ -1,4 +1,4 @@
import data.prod data.unit
import data.prod
open prod
inductive tree (A : Type) : Type :=
@ -18,7 +18,7 @@ definition tree.below.{l₁ l₂}
(λ t : forest A, Type.{max 1 l₂})
t
(λ (a : A) (f : forest A) (r : Type.{max 1 l₂}), prod.{l₂ (max 1 l₂)} (C₂ f) r)
unit.{max 1 l₂}
poly_unit.{max 1 l₂}
(λ (t : tree A) (f : forest A) (rt : Type.{max 1 l₂}) (rf : Type.{max 1 l₂}),
prod.{(max 1 l₂) (max 1 l₂)} (prod.{l₂ (max 1 l₂)} (C₁ t) rt) (prod.{l₂ (max 1 l₂)} (C₂ f) rf))
@ -32,7 +32,7 @@ definition forest.below.{l₁ l₂}
(λ t : forest A, Type.{max 1 l₂})
f
(λ (a : A) (f : forest A) (r : Type.{max 1 l₂}), prod.{l₂ (max 1 l₂)} (C₂ f) r)
unit.{max 1 l₂}
poly_unit.{max 1 l₂}
(λ (t : tree A) (f : forest A) (rt : Type.{max 1 l₂}) (rf : Type.{max 1 l₂}),
prod.{(max 1 l₂) (max 1 l₂)} (prod.{l₂ (max 1 l₂)} (C₁ t) rt) (prod.{l₂ (max 1 l₂)} (C₂ f) rf))
@ -57,7 +57,7 @@ have general : prod.{l₂ (max 1 l₂)} (C₁ t) (tree.below A C₁ C₂ t), fro
F₁ (tree.node a f) b,
prod.mk.{l₂ (max 1 l₂)} c b)
(have b : forest.below A C₁ C₂ (forest.nil A), from
unit.star.{max 1 l₂},
poly_unit.star.{max 1 l₂},
have c : C₂ (forest.nil A), from
F₂ (forest.nil A) b,
prod.mk.{l₂ (max 1 l₂)} c b)
@ -93,7 +93,7 @@ have general : prod.{l₂ (max 1 l₂)} (C₂ f) (forest.below A C₁ C₂ f), f
F₁ (tree.node a f) b,
prod.mk.{l₂ (max 1 l₂)} c b)
(have b : forest.below A C₁ C₂ (forest.nil A), from
unit.star.{max 1 l₂},
poly_unit.star.{max 1 l₂},
have c : C₂ (forest.nil A), from
F₂ (forest.nil A) b,
prod.mk.{l₂ (max 1 l₂)} c b)

6
tests/lean/run/ftree_brec.lean
View file

@ -1,4 +1,4 @@
import data.unit data.prod
import data.prod
inductive ftree (A : Type) (B : Type) : Type :=
| leafa : ftree A B
@ -16,7 +16,7 @@ definition below.{l l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (C : ftree A
A
B
(λ t : ftree A B, Type.{max l₁ l₂ (l+1)})
unit.{max l₁ l₂ (l+1)}
poly_unit.{max l₁ l₂ (l+1)}
(λ (f₁ : A → B → ftree A B)
(f₂ : B → ftree A B)
(r₁ : Π (a : A) (b : B), Type.{max l₁ l₂ (l+1)})
@ -60,7 +60,7 @@ have gen : prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (@below A B C t), from
B
(λ t : ftree A B, prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (@below A B C t))
(have b : @below A B C (leafa A B), from
unit.star.{max l₁ l₂ (l+1)},
poly_unit.star.{max l₁ l₂ (l+1)},
have c : C (leafa A B), from
F (leafa A B) b,
prod.mk.{(l+1) (max l₁ l₂ (l+1))} c b)

2
tests/lean/run/tree.lean
View file

@ -44,7 +44,7 @@ end manual
definition below_rec_on (t : tree A) (H : Π (n : tree A), @tree.below A C n → C n) : C t
:= have general : C t × @tree.below A C t, from
tree.rec_on t
(λa, (H (leaf a) unit.star, unit.star))
(λa, (H (leaf a) poly_unit.star, poly_unit.star))
(λ (l r : tree A) (Hl : C l × @tree.below A C l) (Hr : C r × @tree.below A C r),
have b : @tree.below A C (node l r), from
((pr₁ Hl, pr₂ Hl), (pr₁ Hr, pr₂ Hr)),

4
tests/lean/run/univ_problem.lean
View file

@ -1,4 +1,4 @@
import logic data.nat.basic data.prod data.unit
import logic data.nat.basic data.prod
open nat prod
inductive vector (A : Type) : nat → Type :=
@ -17,7 +17,7 @@ namespace vector
definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @vector.below A C n v → C n v) : C n v :=
have general : C n v × @vector.below A C n v, from
vector.rec_on v
(pair (H zero vnil unit.star) unit.star)
(pair (H zero vnil poly_unit.star) poly_unit.star)
(λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @vector.below A C n₁ v₁),
have b : @vector.below A C _ (vcons a₁ v₁), from
r₁,

2
tests/lean/run/vector.lean
View file

@ -33,7 +33,7 @@ namespace vector
definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @vector.below A C n v → C n v) : C n v :=
have general : C n v × @vector.below A C n v, from
vector.rec_on v
(pair (H zero vnil unit.star) unit.star)
(pair (H zero vnil poly_unit.star) poly_unit.star)
(λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @vector.below A C n₁ v₁),
have b : @vector.below A C _ (vcons a₁ v₁), from
r₁,