From dc6411b90385344b69f16512a28ce190a01e722b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 May 2015 14:41:12 -0700 Subject: [PATCH] feat(library/inductive_unifier_plugin): restrict rule that was generating non-terminating behavior see issue #632 --- hott/init/trunc.hlean | 10 ++--- hott/types/int/basic.hlean | 8 +++- hott/types/int/hott.hlean | 4 +- library/data/int/basic.lean | 8 +++- library/data/nat/order.lean | 2 +- src/library/inductive_unifier_plugin.cpp | 3 ++ tests/lean/run/is_nil.lean | 24 ----------- tests/lean/run/tactic23.lean | 4 +- tests/lean/run/uni.lean | 49 ----------------------- tests/lean/run/uni2.lean | 51 ------------------------ 10 files changed, 27 insertions(+), 136 deletions(-) delete mode 100644 tests/lean/run/uni.lean delete mode 100644 tests/lean/run/uni2.lean diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 7b91504ea..91f93def3 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -87,7 +87,7 @@ namespace is_trunc definition is_trunc_eq [instance] [priority 1200] (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x = y) := - is_trunc.mk (!is_trunc.to_internal x y) + is_trunc.mk (@is_trunc.to_internal (n .+1) A H x y) /- contractibility -/ @@ -95,7 +95,7 @@ namespace is_trunc is_trunc.mk (contr_internal.mk center center_eq) definition center (A : Type) [H : is_contr A] : A := - @contr_internal.center A !is_trunc.to_internal + @contr_internal.center A (@is_trunc.to_internal -2 A H) definition center_eq [H : is_contr A] (a : A) : !center = a := @contr_internal.center_eq A !is_trunc.to_internal a @@ -144,11 +144,11 @@ namespace is_trunc definition is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A] : is_trunc (n.+1) A := - is_trunc_of_leq A star + @is_trunc_of_leq A (-2.+1) _ star _ - definition is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A] + definition is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A] : is_trunc (n.+2) A := - is_trunc_of_leq A star + @is_trunc_of_leq A (-2.+1.+1) _ star _ /- hprops -/ diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean index d4907c04c..7b84dde36 100644 --- a/hott/types/int/basic.hlean +++ b/hott/types/int/basic.hlean @@ -799,7 +799,13 @@ definition succ_neg_nat_succ (n : ℕ) : succ (-nat.succ n) = -n := !succ_neg_su definition rec_nat_on [unfold-c 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) (Hpred : Π⦃n : ℕ⦄, P (-n) → P (-nat.succ n)) : P z := -int.rec_on z (λn, nat.rec_on n H0 Hsucc) (λn, nat.rec_on n (Hpred H0) (λm H, Hpred H)) +begin + induction z with n n, + {exact nat.rec_on n H0 Hsucc}, + {induction n with m ih, + exact Hpred H0, + exact Hpred ih} +end --the only computation rule of rec_nat_on which is not definitional definition rec_nat_on_neg {P : ℤ → Type} (n : nat) (H0 : P zero) diff --git a/hott/types/int/hott.hlean b/hott/types/int/hott.hlean index cd02efc2f..c79d5fa96 100644 --- a/hott/types/int/hott.hlean +++ b/hott/types/int/hott.hlean @@ -98,8 +98,8 @@ namespace eq rec_nat_on b idp (λn IH, calc - power p (succ n) ⬝ p⁻¹ = power p n : con_inv_cancel_right - ... = power p (pred (succ n)) : by rewrite pred_nat_succ) + power p (succ n) ⬝ p⁻¹ = power p n : by apply con_inv_cancel_right + ... = power p (pred (succ n)) : by rewrite pred_nat_succ) (λn IH, calc power p (-succ n) ⬝ p⁻¹ = power p (-succ (succ n)) : by rewrite [↑power,-rec_nat_on_neg] ... = power p (pred (-succ n)) : by rewrite -neg_succ) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 1ff98569b..3d603a310 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -660,7 +660,13 @@ theorem succ_neg_nat_succ (n : ℕ) : succ (-nat.succ n) = -n := !succ_neg_succ definition rec_nat_on [unfold-c 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) (Hpred : Π⦃n : ℕ⦄, P (-n) → P (-nat.succ n)) : P z := -int.rec_on z (λn, nat.rec_on n H0 Hsucc) (λn, nat.rec_on n (Hpred H0) (λm H, Hpred H)) +begin + induction z with n n, + {exact nat.rec_on n H0 Hsucc}, + {induction n with m ih, + exact Hpred H0, + exact Hpred ih} +end --the only computation rule of rec_nat_on which is not definitional theorem rec_nat_on_neg {P : ℤ → Type} (n : nat) (H0 : P zero) diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index ac386ff1a..299f56db3 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -237,7 +237,7 @@ theorem succ_le_succ {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := !add_one ▸ !add_one ▸ add_le_add_right H 1 theorem le_of_succ_le_succ {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m := -le_of_add_le_add_right H +le_of_add_le_add_right (by rewrite -add_one at H; assumption) theorem self_le_succ (n : ℕ) : n ≤ succ n := le.intro !add_one diff --git a/src/library/inductive_unifier_plugin.cpp b/src/library/inductive_unifier_plugin.cpp index 1aa92eb65..755554b58 100644 --- a/src/library/inductive_unifier_plugin.cpp +++ b/src/library/inductive_unifier_plugin.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" #include "library/unifier_plugin.h" #include "library/unifier.h" +#include "library/util.h" namespace lean { class inductive_unifier_plugin_cell : public unifier_plugin_cell { @@ -98,6 +99,8 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell { expr const & elim = get_app_args(lhs, args); environment const & env = tc.env(); auto it_name = *inductive::is_elim_rule(env, const_name(elim)); + if (is_recursive_datatype(env, it_name)) + return lazy_list(); auto decls = *inductive::is_inductive_decl(env, it_name); for (auto const & d : std::get<2>(decls)) { if (inductive::inductive_decl_name(d) == it_name) diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean index 3e049c2cb..7459b9693 100644 --- a/tests/lean/run/is_nil.lean +++ b/tests/lean/run/is_nil.lean @@ -23,27 +23,3 @@ theorem cons_ne_nil {A : Type} (a : A) (l : list A) : ¬ cons a l = nil theorem T : is_nil (@nil Prop) := by apply is_nil_nil - -(* -local list = Const("list", {1})(Prop) -local isNil = Const("is_nil", {1})(Prop) -local Nil = Const({"list", "nil"}, {1})(Prop) -local m = mk_metavar("m", list) -print(isNil(Nil)) -print(isNil(m)) - - -function test_unify(env, m, lhs, rhs, num_s) - print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s)) - local ss = unify(env, lhs, rhs, name_generator(), substitution()) - local n = 0 - for s in ss do - print("solution: " .. tostring(s:instantiate(m))) - n = n + 1 - end - if num_s ~= n then print("n: " .. n) end - assert(num_s == n) -end -print("=====================") -test_unify(get_env(), m, isNil(Nil), isNil(m), 2) -*) diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean index 6573e206c..2bbf670c5 100644 --- a/tests/lean/run/tactic23.lean +++ b/tests/lean/run/tactic23.lean @@ -31,8 +31,8 @@ theorem T1 {p : nat → Prop} {a : nat } (H : p (a+2)) : ∃ x, p (succ x) definition is_zero (n : nat) := nat.rec true (λ n r, false) n -theorem T2 : ∃ a, (is_zero a) = true -:= by apply exists.intro; apply eq.refl +theorem T2 : ∃ a, (is_zero a) = true := +by existsi zero; apply eq.refl end nat end experiment diff --git a/tests/lean/run/uni.lean b/tests/lean/run/uni.lean deleted file mode 100644 index 311e866eb..000000000 --- a/tests/lean/run/uni.lean +++ /dev/null @@ -1,49 +0,0 @@ -import logic -namespace experiment -inductive nat : Type := -| zero : nat -| succ : nat → nat - -check @nat.rec - -(* -local env = get_env() -local nat_rec = Const({"nat", "rec"}, {1}) -local nat = Const("nat") -local n = Local("n", nat) -local C = Fun(n, Prop) -local p = Local("p", Prop) -local ff = Const("false") -local tt = Const("true") -local t = nat_rec(C, ff, Fun(n, p, tt)) -local zero = Const("zero") -local succ = Const("succ") -local one = succ(zero) -local tc = type_checker(env) -print(env:whnf(t(one))) -print(env:whnf(t(zero))) -local m = mk_metavar("m", nat) -print(env:whnf(t(m))) - -function test_unify(env, lhs, rhs, num_s) - print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s)) - local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options()) - local n = 0 - for s in ss do - print("solution: ") - s:for_each_expr(function(n, v, j) - print(" " .. tostring(n) .. " := " .. tostring(v)) - end) - s:for_each_level(function(n, v, j) - print(" " .. tostring(n) .. " := " .. tostring(v)) - end) - n = n + 1 - end - if num_s ~= n then print("n: " .. n) end - assert(num_s == n) -end - -test_unify(env, t(m), tt, 1) -test_unify(env, t(m), ff, 1) -*) -end experiment diff --git a/tests/lean/run/uni2.lean b/tests/lean/run/uni2.lean deleted file mode 100644 index 86d61f014..000000000 --- a/tests/lean/run/uni2.lean +++ /dev/null @@ -1,51 +0,0 @@ -import logic -namespace experiment -inductive nat : Type := -| zero : nat -| succ : nat → nat - -constant f : nat → nat - -check @nat.rec - -(* -local env = get_env() -local nat_rec = Const({"nat", "rec"}, {1}) -local nat = Const("nat") -local f = Const("f") -local n = Local("n", nat) -local C = Fun(n, Prop) -local p = Local("p", Prop) -local ff = Const("false") -local tt = Const("true") -local t = nat_rec(C, ff, Fun(n, p, tt)) -local zero = Const("zero") -local succ = Const("succ") -local one = succ(zero) -local tc = type_checker(env) -print(env:whnf(t(one))) -print(env:whnf(t(zero))) -local m = mk_metavar("m", nat) -print(env:whnf(t(m))) - -function test_unify(env, lhs, rhs, num_s) - print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s)) - local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options()) - local n = 0 - for s in ss do - print("solution: ") - s:for_each_expr(function(n, v, j) - print(" " .. tostring(n) .. " := " .. tostring(v)) - end) - s:for_each_level(function(n, v, j) - print(" " .. tostring(n) .. " := " .. tostring(v)) - end) - n = n + 1 - end - if num_s ~= n then print("n: " .. n) end - assert(num_s == n) -end - -test_unify(env, f(t(m)), f(tt), 1) -*) -exit