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

refactor(library/reducible): simplify reducible/irreducible semantics

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-08 18:47:44 -08:00
parent a23f3e9102
commit 2e4a2451e6
22 changed files with 69 additions and 55 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
doc/lean/reducible.org
View file

@ -42,10 +42,6 @@ if simple unfolding decision then
else -- complex unfolding decision
if reducible(C) then
unfold
else if irreducible(C) then
do not unfold
else if C was defined in the current module then
unfold
else
do not unfold
end
@ -55,7 +51,6 @@ end
For an opaque definition =D=, the higher-order unification procedure uses the
same decision tree if =D= was declared in the current module. Otherwise, it does
not unfold =D=.
#+END_SRC
The following command declares a transparent definition =pr= and mark it as reducible.

2
hott/algebra/group.hlean
View file

@ -404,7 +404,7 @@ section add_group
/- minus -/
-- TODO: derive corresponding facts for div in a field
definition minus (a b : A) : A := a + -b
definition minus [reducible] (a b : A) : A := a + -b
infix `-` := minus

1
hott/init/axioms/funext_varieties.hlean
View file

@ -85,6 +85,7 @@ context
@transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f idhtpy) (sigma.mk g h)
(@path_contr _ contr_basedhtpy _ _) d
reducible htpy_ind
definition htpy_ind_beta : htpy_ind f idhtpy = d :=
(@path2_contr _ _ _ _ !path_contr idp)⁻¹ ▹ idp

4
hott/init/hedberg.hlean
View file

@ -20,12 +20,12 @@ context
hypothesis (h : decidable_eq A)
variables {x y : A}
private definition pc : path_coll A :=
private definition pc [reducible] : path_coll A :=
λ a b, decidable.rec_on (h a b)
(λ p : a = b, ⟨(λ q, p), λ q r, rfl⟩)
(λ np : ¬ a = b, ⟨(λ q, q), λ q r, absurd q np⟩)
private definition f : x = y → x = y :=
private definition f [reducible] : x = y → x = y :=
sigma.rec_on (pc x y) (λ f c, f)
private definition f_const (p q : x = y) : f p = f q :=

1
hott/init/nat.hlean
View file

@ -296,6 +296,7 @@ namespace nat
notation a * b := mul a b
reducible sub
definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
rec_on b
rfl

1
hott/types/sigma.hlean
View file

@ -142,6 +142,7 @@ namespace sigma
apply dpair_eq_dpair_pp_pp
end
reducible dpair_eq_dpair
definition dpair_eq_dpair_p1_1p (p : a = a') (q : p ▹ b = b') :
dpair_eq_dpair p q = dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q :=
begin

1
library/algebra/category/constructions.lean
View file

@ -77,6 +77,7 @@ namespace category
(λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _)
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
reducible discrete_category
definition Discrete_category (A : Type) [H : decidable_eq A] := Mk (discrete_category A)
context
instance discrete_category

9
library/data/int/basic.lean
View file

@ -127,6 +127,8 @@ calc
sub_nat_nat m n = nat.cases_on 0 (of_nat (m - n)) _ : H1 ▸ rfl
... = of_nat (m - n) : rfl
context
reducible sub_nat_nat
theorem sub_nat_nat_of_lt {m n : ℕ} (H : m < n) :
sub_nat_nat m n = neg_succ_of_nat (pred (n - m)) :=
have H1 : n - m = succ (pred (n - m)), from (succ_pred_of_pos (sub_pos_of_gt H))⁻¹,
@ -134,6 +136,7 @@ calc
sub_nat_nat m n = nat.cases_on (succ (pred (n - m))) (of_nat (m - n))
(take k, neg_succ_of_nat k) : H1 ▸ rfl
... = neg_succ_of_nat (pred (n - m)) : rfl
end
definition nat_abs (a : ℤ) : ℕ := cases_on a (take n, n) (take n', succ n')
@ -278,6 +281,8 @@ calc
... = abstr (repr b) : abstr_eq H
... = b : abstr_repr
context
reducible abstr dist
theorem nat_abs_abstr (p : ℕ × ℕ) : nat_abs (abstr p) = dist (pr1 p) (pr2 p) :=
let m := pr1 p, n := pr2 p in
or.elim (@le_or_gt n m)
@ -291,6 +296,7 @@ or.elim (@le_or_gt n m)
... = succ (pred (n - m)) : rfl
... = n - m : succ_pred_of_pos (sub_pos_of_gt H)
... = dist m n : dist_le (le_of_lt H))
end
theorem cases_of_nat (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat n) :=
cases_on a
@ -455,6 +461,8 @@ have H2 : nat_abs b = pabs (repr b), from !nat_abs_eq_pabs_repr,
have H3 : pabs (padd (repr a) (repr b)) ≤ pabs (repr a) + pabs (repr b), from !dist_add_le_add_dist,
H⁻¹ ▸ H1⁻¹ ▸ H2⁻¹ ▸ H3
context
reducible nat_abs
theorem mul_nat_abs (a b : ℤ) : nat_abs (a * b) = #nat (nat_abs a) * (nat_abs b) :=
cases_on a
(take m,
@ -465,6 +473,7 @@ cases_on a
cases_on b
(take n, !nat_abs_neg ▸ rfl)
(take n', rfl))
end
/- multiplication -/

30
library/data/list/basic.lean
View file

@ -40,11 +40,12 @@ append_nil_right (a :: l) := calc
(a :: l) ++ nil = a :: (l ++ nil) : rfl
... = a :: l : append_nil_right l
theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u),
append.assoc nil t u := rfl,
append.assoc (a :: l) t u := calc
(a :: l) ++ t ++ u = a :: (l ++ t ++ u) : rfl
... = a :: (l ++ (t ++ u)) : append.assoc l t u
... = a :: (l ++ (t ++ u)) : append.assoc
... = (a :: l) ++ (t ++ u) : rfl
/- length -/
@ -63,7 +64,7 @@ length_append nil t := calc
... = length nil + length t : zero_add,
length_append (a :: s) t := calc
length (a :: s ++ t) = length (s ++ t) + 1 : rfl
... = length s + length t + 1 : length_append s t
... = length s + length t + 1 : length_append
... = (length s + 1) + length t : add.succ_left
... = length (a :: s) + length t : rfl
@ -83,7 +84,7 @@ theorem concat_eq_append (a : T) : ∀ (l : list T), concat a l = l ++ [a],
concat_eq_append nil := rfl,
concat_eq_append (b :: l) := calc
concat a (b :: l) = b :: (concat a l) : rfl
... = b :: (l ++ [a]) : concat_eq_append l
... = b :: (l ++ [a]) : concat_eq_append
... = (b :: l) ++ [a] : rfl
-- add_rewrite append_nil append_cons
@ -103,28 +104,28 @@ theorem reverse_singleton (x : T) : reverse [x] = [x]
theorem reverse_append : ∀ (s t : list T), reverse (s ++ t) = (reverse t) ++ (reverse s),
reverse_append nil t2 := calc
reverse (nil ++ t2) = reverse t2 : rfl
... = (reverse t2) ++ nil : (append_nil_right (reverse t2))⁻¹
... = (reverse t2) ++ nil : append_nil_right
... = (reverse t2) ++ (reverse nil) : {reverse_nil⁻¹},
reverse_append (a2 :: s2) t2 := calc
reverse ((a2 :: s2) ++ t2) = concat a2 (reverse (s2 ++ t2)) : rfl
... = concat a2 (reverse t2 ++ reverse s2) : {reverse_append s2 t2}
... = concat a2 (reverse t2 ++ reverse s2) : reverse_append
... = (reverse t2 ++ reverse s2) ++ [a2] : concat_eq_append
... = reverse t2 ++ (reverse s2 ++ [a2]) : append.assoc
... = reverse t2 ++ concat a2 (reverse s2) : {concat_eq_append a2 (reverse s2)⁻¹}
... = reverse t2 ++ concat a2 (reverse s2) : concat_eq_append
... = reverse t2 ++ reverse (a2 :: s2) : rfl
theorem reverse_reverse : ∀ (l : list T), reverse (reverse l) = l,
reverse_reverse nil := rfl,
reverse_reverse (a :: l) := calc
reverse (reverse (a :: l)) = reverse (concat a (reverse l)) : rfl
... = reverse (reverse l ++ [a]) : {concat_eq_append a (reverse l)}
... = reverse [a] ++ reverse (reverse l) : {reverse_append (reverse l) [a]}
... = reverse [a] ++ l : {reverse_reverse l}
... = reverse (reverse l ++ [a]) : concat_eq_append
... = reverse [a] ++ reverse (reverse l) : reverse_append
... = reverse [a] ++ l : reverse_reverse
... = a :: l : rfl
theorem concat_eq_reverse_cons (x : T) (l : list T) : concat x l = reverse (x :: reverse l) :=
calc
concat x l = concat x (reverse (reverse l)) : {(reverse_reverse l)⁻¹}
concat x l = concat x (reverse (reverse l)) : reverse_reverse
... = reverse (x :: reverse l) : rfl
/- head and tail -/
@ -138,11 +139,11 @@ theorem head_cons [h : inhabited T] (a : T) (l : list T) : head (a::l) = a
theorem head_concat [h : inhabited T] {s : list T} (t : list T) : s ≠ nil → head (s ++ t) = head s :=
cases_on s
(take H : nil ≠ nil, absurd rfl H)
(take x s, take H : x::s ≠ nil,
(take (x : T) (s : list T), take H : x::s ≠ nil,
calc
head (x::s ++ t) = head (x::(s ++ t)) : {!append_cons}
... = x : !head_cons
... = head (x::s) : !head_cons⁻¹)
head ((x::s) ++ t) = head (x::(s ++ t)) : rfl
... = x : head_cons
... = head (x::s) : rfl)
definition tail : list T → list T,
tail nil := nil,
@ -196,6 +197,7 @@ induction_on s
theorem mem_concat (x : T) (s t : list T) : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t :=
iff.intro mem_concat_imp_or mem_or_imp_concat
reducible mem append
theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) :=
induction_on l
(take H : x ∈ nil, false.elim (iff.elim_left !mem_nil H))

2
library/data/nat/sub.lean
View file

@ -348,7 +348,7 @@ sub_split
-- This section is still incomplete
definition dist (n m : ℕ) := (n - m) + (m - n)
definition dist [reducible] (n m : ℕ) := (n - m) + (m - n)
theorem dist_comm (n m : ℕ) : dist n m = dist m n :=
!add.comm

8
library/data/set.lean
View file

@ -12,7 +12,7 @@ open eq.ops bool
namespace set
definition set (T : Type) :=
T → bool
definition mem {T : Type} (x : T) (s : set T) :=
definition mem [reducible] {T : Type} (x : T) (s : set T) :=
(s x) = tt
notation e ∈ s := mem e s
@ -29,7 +29,7 @@ take x, iff.symm (H x)
theorem eqv_trans {T : Type} {A B C : set T} (H1 : A ∼ B) (H2 : B ∼ C) : A ∼ C :=
take x, iff.trans (H1 x) (H2 x)
definition empty {T : Type} : set T :=
definition empty [reducible] {T : Type} : set T :=
λx, ff
notation `∅` := empty
@ -42,7 +42,7 @@ definition univ {T : Type} : set T :=
theorem mem_univ {T : Type} (x : T) : x ∈ univ :=
rfl
definition inter {T : Type} (A B : set T) : set T :=
definition inter [reducible] {T : Type} (A B : set T) : set T :=
λx, A x && B x
notation a ∩ b := inter a b
@ -69,7 +69,7 @@ take x, band.comm (A x) (B x) ▸ iff.rfl
theorem inter_assoc {T : Type} (A B C : set T) : (A ∩ B) ∩ C ∼ A ∩ (B ∩ C) :=
take x, band.assoc (A x) (B x) (C x) ▸ iff.rfl
definition union {T : Type} (A B : set T) : set T :=
definition union [reducible] {T : Type} (A B : set T) : set T :=
λx, A x || B x
notation a ∪ b := union a b

10
library/data/sigma.lean
View file

@ -40,11 +40,11 @@ namespace sigma
definition dtrip (a : A) (b : B a) (c : C a b) := ⟨a, b, c⟩
definition dquad (a : A) (b : B a) (c : C a b) (d : D a b c) := ⟨a, b, c, d⟩
definition pr1' (x : Σ a, B a) := x.1
definition pr2' (x : Σ a b, C a b) := x.2.1
definition pr3 (x : Σ a b, C a b) := x.2.2
definition pr3' (x : Σ a b c, D a b c) := x.2.2.1
definition pr4 (x : Σ a b c, D a b c) := x.2.2.2
definition pr1' [reducible] (x : Σ a, B a) := x.1
definition pr2' [reducible] (x : Σ a b, C a b) := x.2.1
definition pr3 [reducible] (x : Σ a b, C a b) := x.2.2
definition pr3' [reducible] (x : Σ a b c, D a b c) := x.2.2.1
definition pr4 [reducible] (x : Σ a b c, D a b c) := x.2.2.2
theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
(H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : cast (dcongr_arg2 C H₁ H₂) c₁ = c₂) :

3
library/init/nat.lean
View file

@ -288,11 +288,14 @@ namespace nat
notation a * b := mul a b
section
reducible sub
definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
induction_on b
rfl
(λ b₁ (ih : succ a - succ b₁ = a - b₁),
eq.rec_on ih (eq.refl (pred (succ a - succ b₁))))
end
definition sub_eq_succ_sub_succ (a b : nat) : a - b = succ a - succ b :=
eq.rec_on (succ_sub_succ_eq_sub a b) rfl

4
library/logic/axioms/examples/diaconescu.lean
View file

@ -12,9 +12,9 @@ context
hypothesis propext {a b : Prop} : (a → b) → (b → a) → a = b
parameter p : Prop
private definition u := epsilon (λx, x = true ∨ p)
private definition u [reducible] := epsilon (λx, x = true ∨ p)
private definition v := epsilon (λx, x = false ∨ p)
private definition v [reducible] := epsilon (λx, x = false ∨ p)
private lemma u_def : u = true ∨ p :=
epsilon_spec (exists.intro true (or.inl rfl))

14
src/library/reducible.cpp
View file

@ -116,17 +116,13 @@ bool is_reducible_off(environment const & env, name const & n) {
}
std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
bool relax_main_opaque, bool only_main_reducible,
bool relax_main_opaque, reducible_behavior rb,
bool memoize) {
reducible_state const & s = reducible_ext::get_state(env);
if (only_main_reducible) {
if (rb == OpaqueIfNotReducibleOn) {
name_set reducible_on = s.m_reducible_on;
name_set reducible_off = s.m_reducible_off;
extra_opaque_pred pred([=](name const & n) {
return
(!module::is_definition(env, n) || reducible_off.contains(n)) &&
(!reducible_on.contains(n));
});
extra_opaque_pred pred([=](name const & n) { return !reducible_on.contains(n); });
return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, relax_main_opaque,
memoize, pred)));
} else {
@ -137,8 +133,8 @@ std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_gene
}
}
std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible) {
return mk_type_checker(env, name_generator(*g_tmp_prefix), relax_main_opaque, only_main_reducible);
std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque, reducible_behavior rb) {
return mk_type_checker(env, name_generator(*g_tmp_prefix), relax_main_opaque, rb);
}
std::unique_ptr<type_checker> mk_opaque_type_checker(environment const & env, name_generator const & ngen) {

7
src/library/reducible.h
View file

@ -33,11 +33,14 @@ bool is_reducible_on(environment const & env, name const & n);
*/
bool is_reducible_off(environment const & env, name const & n);
enum reducible_behavior { OpaqueIfNotReducibleOn, OpaqueIfReducibleOff };
/** \brief Create a type checker that takes the "reducibility" hints into account. */
std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
bool relax_main_opaque = true, bool only_main_reducible = false,
bool relax_main_opaque = true, reducible_behavior r = OpaqueIfReducibleOff,
bool memoize = true);
std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible = false);
std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque,
reducible_behavior r = OpaqueIfReducibleOff);
/** \brief Create a type checker that treats all definitions as opaque. */
std::unique_ptr<type_checker> mk_opaque_type_checker(environment const & env, name_generator const & ngen);

17
src/library/unifier.cpp
View file

@ -305,8 +305,8 @@ struct unifier_fn {
expr_map m_type_map; // auxiliary map for storing the type of the expr in choice constraints
unifier_plugin m_plugin;
type_checker_ptr m_tc[2];
type_checker_ptr m_flex_rigid_tc[2]; // type checker used when solving flex rigid constraints. By default,
// only the definitions from the main module are treated as transparent.
type_checker_ptr m_flex_rigid_tc; // type checker used when solving flex rigid constraints. By default,
// only the definitions from the main module are treated as transparent.
unifier_config m_config;
unsigned m_num_steps;
bool m_pattern; //!< If true, then only higher-order (pattern) matching is used
@ -417,16 +417,13 @@ struct unifier_fn {
if (m_config.m_cheap) {
m_tc[0] = mk_opaque_type_checker(env, m_ngen.mk_child());
m_tc[1] = m_tc[0];
m_flex_rigid_tc[0] = m_tc[0];
m_flex_rigid_tc[1] = m_tc[0];
m_flex_rigid_tc = m_tc[0];
m_config.m_computation = false;
} else {
m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false);
m_tc[1] = mk_type_checker(env, m_ngen.mk_child(), true);
if (!cfg.m_computation) {
m_flex_rigid_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false, true);
m_flex_rigid_tc[1] = mk_type_checker(env, m_ngen.mk_child(), true, true);
}
if (!cfg.m_computation)
m_flex_rigid_tc = mk_type_checker(env, m_ngen.mk_child(), false, OpaqueIfNotReducibleOn);
}
m_next_assumption_idx = 0;
m_next_cidx = 0;
@ -600,7 +597,7 @@ struct unifier_fn {
return whnf(e, j, relax, cs);
} else {
constraint_seq _cs;
expr r = m_flex_rigid_tc[relax]->whnf(e, _cs);
expr r = m_flex_rigid_tc->whnf(e, _cs);
to_buffer(_cs, j, cs);
return r;
}
@ -1399,7 +1396,7 @@ struct unifier_fn {
if (u.m_config.m_computation)
return *u.m_tc[relax];
else
return *u.m_flex_rigid_tc[relax];
return *u.m_flex_rigid_tc;
}
/** \brief Return true if margs contains an expression \c e s.t. is_meta(e) */

1
tests/lean/run/impbug1.lean
View file

@ -11,6 +11,7 @@ mk : Π (id : Π (A : ob), mor A A),
definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat
reducible id
theorem id_left (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) (A : ob) (f : mor A A) :
@eq (mor A A) (id ob mor Cat A) f :=
@category.rec ob mor (λ (C : category ob mor), @eq (mor A A) (id ob mor C A) f)

1
tests/lean/run/impbug2.lean
View file

@ -14,6 +14,7 @@ constant ob : Type.{1}
constant mor : ob → ob → Type.{1}
constant Cat : category ob mor
reducible id
theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id ob mor Cat A) f :=
@category.rec ob mor (λ (C : category ob mor), @eq (mor A A) (id ob mor C A) f)
(λ (id : Π (T : ob), mor T T)

1
tests/lean/run/impbug3.lean
View file

@ -15,6 +15,7 @@ mk : Π (id : Π (A : ob), mor A A),
definition id (Cat : category) := category.rec (λ id idl, id) Cat
constant Cat : category
reducible id
theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id Cat A) f :=
@category.rec (λ (C : category), @eq (mor A A) (id C A) f)
(λ (id : Π (T : ob), mor T T)

1
tests/lean/run/list_elab1.lean
View file

@ -23,6 +23,7 @@ list.rec Hnil Hind l
definition concat {T : Type} (s t : list T) : list T :=
list.rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
reducible concat
theorem concat_nil {T : Type} (t : list T) : concat t nil = t :=
list_induction_on t (eq.refl (concat nil nil))
(take (x : T) (l : list T) (H : concat l nil = l),

1
tests/lean/slow/list_elab2.lean
View file

@ -61,6 +61,7 @@ list_induction_on t (refl _)
(take (x : T) (l : list T) (H : concat l nil = l),
H ▸ (refl (cons x (concat l nil))))
reducible concat
theorem concat_nil2 (t : list T) : t ++ nil = t :=
list_induction_on t (refl _)
(take (x : T) (l : list T) (H : concat l nil = l),