From cebde17bec5abdbc2b95651fc5be10bcee229c62 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Jan 2018 18:18:56 -0800 Subject: [PATCH] feat(library/tactic/simplify): `simp` reduces `c a_1 ... a_n = c b_1 ... b_n` into `a_1 = b_1 /\ ... /\ a_n = b_n` --- doc/changes.md | 3 ++ library/data/rbmap/default.lean | 2 +- library/data/rbtree/find.lean | 4 +- library/data/rbtree/min_max.lean | 8 +-- library/data/stream.lean | 2 +- library/init/data/nat/lemmas.lean | 6 +-- library/init/meta/interactive.lean | 3 +- library/init/native/result.lean | 2 +- src/library/inductive_compiler/nested.cpp | 1 + src/library/tactic/simplify.cpp | 63 +++++++++++++++++------ src/library/tactic/simplify.h | 6 ++- tests/lean/run/simp_constructor.lean | 20 ++++++- 12 files changed, 88 insertions(+), 32 deletions(-) diff --git a/doc/changes.md b/doc/changes.md index f27583bf7e..1ff353bd76 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -97,6 +97,9 @@ master branch (aka work in progress branch) * `simp` now reduces equalities `c_1 ... = c_2 ...` to `false` if `c_1` and `c_2` are distinct constructors. This feature can be disabled using `simp {constructor_eq := ff}`. +* `simp` now reduces equalities `c a_1 ... a_n = c b_1 ... b_n` to `a_1 = b_1 /\ ... /\ a_n = b_n` if `c` is a constructor. + This feature can be disabled using `simp {constructor_eq := ff}`. + * `subst` and `subst_vars` now support heterogeneous equalities that are actually homogeneous (i.e., `@heq α a β b` where `α` and `β` are definitionally equal). diff --git a/library/data/rbmap/default.lean b/library/data/rbmap/default.lean index f934ce33ad..16466cc25b 100644 --- a/library/data/rbmap/default.lean +++ b/library/data/rbmap/default.lean @@ -60,7 +60,7 @@ end lemma eq_some_of_to_value_eq_some {e : option (α × β)} {v : β} : to_value e = some v → ∃ k, e = some (k, v) := begin cases e with val; simp [to_value], - { cases val, simp, intro h, injection h, subst v, constructor, refl } + { cases val, simp, intro h, subst v, constructor, refl } end lemma eq_none_of_to_value_eq_none {e : option (α × β)} : to_value e = none → e = none := diff --git a/library/data/rbtree/find.lean b/library/data/rbtree/find.lean index a6074b166f..c4b9ec6dfd 100644 --- a/library/data/rbtree/find.lean +++ b/library/data/rbtree/find.lean @@ -114,7 +114,7 @@ begin { have hyx : lift lt (some y) (some x) := (range hs_hs₂ (mem_of_mem_exact hm)).1, simp [lift] at hyx, exact absurd hyx h.2 } }, - { intro hm, injection hm, simp [*] } }, + { intro hm, simp [*] } }, { cases hs, apply iff.intro, @@ -137,7 +137,7 @@ begin apply find.induction lt t x; intros; simp only [mem, find, *] at *, iterate 2 { { cases hs, exact ih hs_hs₁ rfl }, - { injection he, subst y, simp at h, exact h }, + { subst y, simp at h, exact h }, { cases hs, exact ih hs_hs₂ rfl } } end diff --git a/library/data/rbtree/min_max.lean b/library/data/rbtree/min_max.lean index 8aaf533c40..9077bbadee 100644 --- a/library/data/rbtree/min_max.lean +++ b/library/data/rbtree/min_max.lean @@ -15,7 +15,7 @@ begin { intros, contradiction }, all_goals { cases t_lchild; simp [rbnode.min]; intro h, - { injection h, subst t_val, simp [mem, irrefl_of lt a] }, + { subst t_val, simp [mem, irrefl_of lt a] }, all_goals { rw [mem], simp [t_ih_lchild h] } } end @@ -25,7 +25,7 @@ begin { intros, contradiction }, all_goals { cases t_rchild; simp [rbnode.max]; intro h, - { injection h, subst t_val, simp [mem, irrefl_of lt a] }, + { subst t_val, simp [mem, irrefl_of lt a] }, all_goals { rw [mem], simp [t_ih_rchild h] } } end @@ -55,7 +55,7 @@ begin { simp [strict_weak_order.equiv], intros _ _ hs hmin b, contradiction }, all_goals { cases t_lchild; intros lo hi hs hmin b hmem, - { simp [rbnode.min] at hmin, injection hmin, subst t_val, + { simp [rbnode.min] at hmin, subst t_val, simp [mem] at hmem, cases hmem with heqv hmem, { left, exact heqv.swap }, { have := lt_of_mem_right hs (by constructor) hmem, @@ -80,7 +80,7 @@ begin { simp [strict_weak_order.equiv], intros _ _ hs hmax b, contradiction }, all_goals { cases t_rchild; intros lo hi hs hmax b hmem, - { simp [rbnode.max] at hmax, injection hmax, subst t_val, + { simp [rbnode.max] at hmax, subst t_val, simp [mem] at hmem, cases hmem with hmem heqv, { have := lt_of_mem_left hs (by constructor) hmem, right, assumption }, diff --git a/library/data/stream.lean b/library/data/stream.lean index 102a6d493b..783a243a60 100644 --- a/library/data/stream.lean +++ b/library/data/stream.lean @@ -464,7 +464,7 @@ theorem take_theorem (s₁ s₂ : stream α) : (∀ (n : nat), approx n s₁ = a begin intro h, apply stream.ext, intro n, induction n with n ih, - { have aux := h 1, unfold approx at aux, injection aux }, + { have aux := h 1, simp [approx] at aux, exact aux }, { have h₁ : some (nth (succ n) s₁) = some (nth (succ n) s₂), { rw [← nth_approx, ← nth_approx, h (succ (succ n))] }, injection h₁ } diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index 49e985c25f..6ce04f9696 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -47,7 +47,7 @@ left_comm nat.add nat.add_comm nat.add_assoc protected lemma add_left_cancel : ∀ {n m k : ℕ}, n + m = n + k → m = k | 0 m k := by simp [nat.zero_add] {contextual := tt} | (succ n) m k := λ h, - have n+m = n+k, by simp [succ_add] at h; injection h, + have n+m = n+k, by { simp [succ_add] at h, assumption }, add_left_cancel this protected lemma add_right_cancel {n m k : ℕ} (h : n + m = k + m) : n = k := @@ -427,14 +427,14 @@ protected lemma bit0_inj : ∀ {n m : ℕ}, bit0 n = bit0 m → n = m | (n+1) 0 h := by contradiction | (n+1) (m+1) h := have succ (succ (n + n)) = succ (succ (m + m)), - begin unfold bit0 at h, simp [add_one, add_succ, succ_add] at h, exact h end, + begin unfold bit0 at h, simp [add_one, add_succ, succ_add] at h, rw h end, have n + n = m + m, by iterate { injection this with this }, have n = m, from bit0_inj this, by rw this protected lemma bit1_inj : ∀ {n m : ℕ}, bit1 n = bit1 m → n = m := λ n m h, -have succ (bit0 n) = succ (bit0 m), begin simp [nat.bit1_eq_succ_bit0] at h, assumption end, +have succ (bit0 n) = succ (bit0 m), begin simp [nat.bit1_eq_succ_bit0] at h, rw h end, have bit0 n = bit0 m, by injection this, nat.bit0_inj this diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index b1d2b828d9..9f9bba8fcb 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -1390,6 +1390,7 @@ structure unfold_config extends simp_config := (proj := ff) (eta := ff) (canonize_instances := ff) +(constructor_eq := ff) namespace interactive open interactive interactive.types expr @@ -1630,7 +1631,7 @@ by tactic.mk_inj_eq lemma psigma.mk.inj_eq {α : Sort u} {β : α → Sort v} (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) : (psigma.mk a₁ b₁ = psigma.mk a₂ b₂) = (a₁ = a₂ ∧ b₁ == b₂) := by tactic.mk_inj_eq -lemma subtype.mk.inj_eq {α : Type u} {p : α → Prop} (a₁ : α) (h₁ : p a₁) (a₂ : α) (h₂ : p a₂) : (subtype.mk a₁ h₁ = subtype.mk a₂ h₂) = (a₁ = a₂) := +lemma subtype.mk.inj_eq {α : Sort u} {p : α → Prop} (a₁ : α) (h₁ : p a₁) (a₂ : α) (h₂ : p a₂) : (subtype.mk a₁ h₁ = subtype.mk a₂ h₂) = (a₁ = a₂) := by tactic.mk_inj_eq lemma option.some.inj_eq {α : Type u} (a₁ a₂ : α) : (some a₁ = some a₂) = (a₁ = a₂) := diff --git a/library/init/native/result.lean b/library/init/native/result.lean index 21028a70d2..dd3088fd26 100644 --- a/library/init/native/result.lean +++ b/library/init/native/result.lean @@ -67,7 +67,7 @@ section resultT bind_assoc := begin intros, cases x, simp, - apply congr_arg, rw [monad.bind_assoc], + rw [monad.bind_assoc], apply congr_arg, funext, cases x with e a; simp, { cases f a, refl }, diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 45c7e70848..7970557b83 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -1554,6 +1554,7 @@ class add_nested_inductive_decl_fn { cfg.m_canonize_proofs = false; cfg.m_use_axioms = false; cfg.m_zeta = false; + cfg.m_constructor_eq = false; return cfg; } diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 1f2da37e21..03a6b9c200 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -34,6 +34,7 @@ Author: Daniel Selsam, Leonardo de Moura #include "library/congr_lemma.h" #include "library/fun_info.h" #include "library/constructions/constructor.h" +#include "library/constructions/injective.h" #include "library/inductive_compiler/ginductive.h" #include "library/vm/vm_expr.h" #include "library/vm/vm_option.h" @@ -671,10 +672,10 @@ simp_result simplify_core_fn::visit(expr const & e, optional const & paren break; } - if (m_cfg.m_constructor_eq) - new_result = simplify_constructor_eq_constructor(new_result); - - if (auto r2 = post(new_result.get_new(), parent)) { + if (m_cfg.m_constructor_eq && simplify_constructor_eq_constructor(new_result)) { + curr_result = new_result; + /* continue simplifying */ + } else if (auto r2 = post(new_result.get_new(), parent)) { if (!r2->second) { curr_result = join(new_result, r2->first); break; @@ -770,28 +771,60 @@ simp_result simplify_core_fn::visit_app(expr const & _e) { return simp_result(e); } -simp_result simplify_core_fn::simplify_constructor_eq_constructor(simp_result const & r) { +bool simplify_core_fn::simplify_constructor_eq_constructor(simp_result & r) { if (m_rel != get_eq_name()) - return r; /* TODO(Leo): we can add support for <-> */ - expr lhs, rhs; - if (!is_eq(r.get_new(), lhs, rhs)) - return r; + return false; /* TODO(Leo): we can add support for <-> */ + expr A, lhs, rhs; + if (!is_eq(r.get_new(), A, lhs, rhs)) + return false; optional c1 = is_gintro_rule_app(m_ctx.env(), lhs); - if (!c1) return r; + if (!c1) return false; optional c2 = is_gintro_rule_app(m_ctx.env(), rhs); - if (!c2) return r; + if (!c2) return false; if (*c1 != *c2) { if (optional not_eq_prf = mk_constructor_ne_constructor_proof(m_ctx, lhs, rhs)) { expr eq_false_prf = mk_app(m_ctx, get_eq_false_intro_name(), *not_eq_prf); simp_result new_r(mk_false(), eq_false_prf); - return join_eq(m_ctx, r, new_r); + r = join_eq(m_ctx, r, new_r); + return true; } else { - return r; + return false; } } else { - /* TODO(Leo) */ - return r; + A = whnf_ginductive(m_ctx, A); + expr const & A_fn = get_app_fn(A); + if (!is_constant(A_fn) || !is_ginductive(m_ctx.env(), const_name(A_fn))) + return false; + unsigned A_nparams = get_ginductive_num_params(m_ctx.env(), const_name(A_fn)); + if (get_app_num_args(lhs) <= A_nparams) + return false; + name inj_eq_name = mk_injective_eq_name(*c1); + optional inj_eq_decl = m_ctx.env().find(inj_eq_name); + if (!inj_eq_decl) + return false; + /* We use the `*.inj` lemma for computing the arguments for `*.inj_eq` lemma. */ + try { + name inj_name = mk_injective_name(*c1); + optional inj_decl = m_ctx.env().find(inj_name); + if (!inj_decl) + return false; + unsigned inj_arity = get_arity(inj_decl->get_type()); + type_context::tmp_locals locals(m_ctx); + expr H = locals.push_local("_h", r.get_new()); + expr inj = mk_app(m_ctx, inj_name, inj_arity, H); + buffer inj_args; + expr const & inj_fn = get_app_args(inj, inj_args); + expr inj_eq_pr = mk_app(mk_constant(inj_eq_name, const_levels(inj_fn)), inj_args.size() - 1, inj_args.data()); + expr inj_eq = m_ctx.infer(inj_eq_pr); + expr new_lhs, new_rhs; + lean_verify(is_eq(inj_eq, new_lhs, new_rhs)); + simp_result new_r(new_rhs, inj_eq_pr); + r = join_eq(m_ctx, r, new_r); + return true; + } catch (exception &) { + return false; + } } } diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h index 4013759d0c..7a9811c186 100644 --- a/src/library/tactic/simplify.h +++ b/src/library/tactic/simplify.h @@ -121,8 +121,10 @@ protected: simp_result propext_rewrite(expr const & e); /* Simplify equalities of the form (c ... = c' ...) where `c` and `c'` are - constructors. */ - simp_result simplify_constructor_eq_constructor(simp_result const & r); + constructors. + + Return true if `r` was simplified. */ + bool simplify_constructor_eq_constructor(simp_result & r); /* Visitors */ virtual optional> pre(expr const & e, optional const & parent); diff --git a/tests/lean/run/simp_constructor.lean b/tests/lean/run/simp_constructor.lean index 748a89d7dd..281d6ff35c 100644 --- a/tests/lean/run/simp_constructor.lean +++ b/tests/lean/run/simp_constructor.lean @@ -11,8 +11,6 @@ end example : ¬ term.var "a" = term.app "f" [] := by simp -#check @term.app.inj_eq - universes u inductive vec (α : Type u) : nat → Type u @@ -35,3 +33,21 @@ with Expr_list : Type | cons : Expr → Expr_list → Expr_list #check @Expr.app.inj_eq + +example {α : Type u} (n : nat) (a₁ a₂ : α) (t : vec α n) (h : vec.cons a₁ t = vec.cons a₂ t) : a₁ = a₂ := +begin + simp at h, + exact h +end + +example (a₁ a₂ : nat) (h₁ : a₁ > 0) (h₂ : a₂ > 0) (h : a₁ = a₂) : subtype.mk a₁ h₁ = subtype.mk a₂ h₂ := +begin + simp, + exact h +end + +example (a₁ a₂ : nat) (h₁ : a₁ > 0) (h₂ : a₂ > 0) (h : subtype.mk a₁ h₁ = subtype.mk a₂ h₂) : a₁ = a₂ := +begin + simp at h, + exact h +end