From 415ca2b93f9ccedd02ff4975089e8e72dc982dd7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 May 2015 12:58:46 -0700 Subject: [PATCH] feat(library/tactic): add 'congruence' tactic It is the f_equal described at issue #500. --- hott/init/tactic.hlean | 3 +- library/init/tactic.lean | 1 + src/emacs/lean-syntax.el | 2 +- src/library/constants.cpp | 4 + src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/tactic/CMakeLists.txt | 3 +- src/library/tactic/congruence_tactic.cpp | 123 +++++++++++++++++++++++ src/library/tactic/congruence_tactic.h | 11 ++ src/library/tactic/init_module.cpp | 3 + tests/lean/hott/congr_tac.hlean | 46 +++++++++ tests/lean/run/congr_tac.lean | 34 +++++++ 12 files changed, 229 insertions(+), 3 deletions(-) create mode 100644 src/library/tactic/congruence_tactic.cpp create mode 100644 src/library/tactic/congruence_tactic.h create mode 100644 tests/lean/hott/congr_tac.hlean create mode 100644 tests/lean/run/congr_tac.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 32e82b76e..1317ef586 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -43,7 +43,8 @@ opaque definition beta : tactic := builtin opaque definition info : tactic := builtin opaque definition whnf : tactic := builtin opaque definition contradiction : tactic := builtin -opaque definition exfalso : tactic := builtin +opaque definition exfalso : tactic := builtin +opaque definition congruence : tactic := builtin opaque definition rotate_left (k : num) := builtin opaque definition rotate_right (k : num) := builtin definition rotate (k : num) := rotate_left k diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 96a585f2b..cbbd88c96 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -44,6 +44,7 @@ opaque definition info : tactic := builtin opaque definition whnf : tactic := builtin opaque definition contradiction : tactic := builtin opaque definition exfalso : tactic := builtin +opaque definition congruence : tactic := builtin opaque definition rotate_left (k : num) := builtin opaque definition rotate_right (k : num) := builtin definition rotate (k : num) := rotate_left k diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 3733535d4..d2236ef1e 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -136,7 +136,7 @@ "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact" "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp" "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "left" "right" - "injection")) + "injection" "congruence")) word-end) (1 'font-lock-constant-face)) ;; Types diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 73d7c45f7..cda7dfce3 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -13,6 +13,7 @@ name const * g_bool_ff = nullptr; name const * g_bool_tt = nullptr; name const * g_char = nullptr; name const * g_char_mk = nullptr; +name const * g_congr = nullptr; name const * g_dite = nullptr; name const * g_empty = nullptr; name const * g_empty_rec = nullptr; @@ -139,6 +140,7 @@ void initialize_constants() { g_bool_tt = new name{"bool", "tt"}; g_char = new name{"char"}; g_char_mk = new name{"char", "mk"}; + g_congr = new name{"congr"}; g_dite = new name{"dite"}; g_empty = new name{"empty"}; g_empty_rec = new name{"empty", "rec"}; @@ -266,6 +268,7 @@ void finalize_constants() { delete g_bool_tt; delete g_char; delete g_char_mk; + delete g_congr; delete g_dite; delete g_empty; delete g_empty_rec; @@ -392,6 +395,7 @@ name const & get_bool_ff_name() { return *g_bool_ff; } name const & get_bool_tt_name() { return *g_bool_tt; } name const & get_char_name() { return *g_char; } name const & get_char_mk_name() { return *g_char_mk; } +name const & get_congr_name() { return *g_congr; } name const & get_dite_name() { return *g_dite; } name const & get_empty_name() { return *g_empty; } name const & get_empty_rec_name() { return *g_empty_rec; } diff --git a/src/library/constants.h b/src/library/constants.h index 15e3ff4f0..33ed64101 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -15,6 +15,7 @@ name const & get_bool_ff_name(); name const & get_bool_tt_name(); name const & get_char_name(); name const & get_char_mk_name(); +name const & get_congr_name(); name const & get_dite_name(); name const & get_empty_name(); name const & get_empty_rec_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 26959c81d..ca951ad6e 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -8,6 +8,7 @@ bool.ff bool.tt char char.mk +congr dite empty empty.rec diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index afa0e24a6..c3058ae21 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -5,6 +5,7 @@ inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp contradiction_tactic.cpp -exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp) +exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp +congruence_tactic.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/congruence_tactic.cpp b/src/library/tactic/congruence_tactic.cpp new file mode 100644 index 000000000..ee262cb53 --- /dev/null +++ b/src/library/tactic/congruence_tactic.cpp @@ -0,0 +1,123 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/util.h" +#include "library/constants.h" +#include "library/reducible.h" +#include "library/tactic/util.h" +#include "library/tactic/intros_tactic.h" +#include "library/tactic/expr_to_tactic.h" + +namespace lean { +tactic congruence_tactic() { + auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) -> optional { + goals const & gs = s.get_goals(); + if (empty(gs)) { + throw_no_goal_if_enabled(s); + return none_proof_state(); + } + goal const & g = head(gs); + expr t = g.get_type(); + substitution subst = s.get_subst(); + name_generator ngen = s.get_ngen(); + auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque()); + constraint_seq cs; + t = tc->whnf(t, cs); + expr lhs, rhs; + if (!is_eq(t, lhs, rhs)) { + throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, goal is not an equality"); + return none_proof_state(); + } + + buffer new_goals; + + auto mk_eq_goal = [&](expr const & lhs, expr const & rhs) { + expr new_type = mk_eq(*tc, lhs, rhs); + expr new_meta = g.mk_meta(ngen.next(), new_type); + new_goals.push_back(goal(new_meta, new_type)); + return some_expr(new_meta); + }; + + std::function(expr const &, expr const &, bool)> process = + [&](expr const & lhs, expr const & rhs, bool first) { + if (tc->is_def_eq(lhs, rhs, justification(), cs)) { + return some_expr(mk_refl(*tc, lhs)); + } + if (!is_app(lhs) || !is_app(rhs)) { + if (first) { + throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, left (and right) hand side of equation must be a function application"); + return none_expr(); + } + return mk_eq_goal(lhs, rhs); + } + expr lhs_fn = app_fn(lhs); + expr rhs_fn = app_fn(rhs); + expr lhs_fn_type = tc->whnf(tc->infer(lhs_fn, cs), cs); + expr rhs_fn_type = tc->whnf(tc->infer(rhs_fn, cs), cs); + if (!tc->is_def_eq(lhs_fn_type, rhs_fn_type, justification(), cs)) { + if (first) { + throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, functions do not have the same type"); + return none_expr(); + } + return mk_eq_goal(lhs, rhs); + } + expr fn_type; + if (is_pi(lhs_fn_type)) { + fn_type = lhs_fn_type; + } else if (is_pi(rhs_fn_type)) { + fn_type = rhs_fn_type; + } else if (first) { + throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, failed to compute function type"); + return none_expr(); + } else { + return mk_eq_goal(lhs, rhs); + } + + if (!closed(binding_body(fn_type))) { + if (first) { + throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, cannot be applied to dependent functions"); + return none_expr(); + } + return mk_eq_goal(lhs, rhs); + } + + expr lhs_arg = app_arg(lhs); + expr rhs_arg = app_arg(rhs); + expr arg_pr; + if (tc->is_def_eq(lhs_arg, rhs_arg, justification(), cs)) { + arg_pr = mk_refl(*tc, lhs_arg); + } else { + arg_pr = *mk_eq_goal(lhs_arg, rhs_arg); + } + + optional opt_fn_pr = process(lhs_fn, rhs_fn, false); + if (!opt_fn_pr) + return none_expr(); + expr fn_pr = *opt_fn_pr; + + expr A = binding_domain(fn_type); + expr B = binding_body(fn_type); + level l1 = sort_level(tc->ensure_type(A, cs)); + level l2 = sort_level(tc->ensure_type(B, cs)); + + return some_expr(mk_app({mk_constant(get_congr_name(), {l1, l2}), + A, B, lhs_fn, rhs_fn, lhs_arg, rhs_arg, fn_pr, arg_pr})); + }; + + if (optional pr = process(lhs, rhs, true)) { + std::reverse(new_goals.begin(), new_goals.end()); + assign(subst, g, *pr); + proof_state new_ps(s, to_list(new_goals.begin(), new_goals.end(), tail(gs)), subst, ngen); + if (solve_constraints(env, ios, new_ps, cs)) + return some_proof_state(new_ps); + } + return none_proof_state(); + }; + return tactic01(fn); +} +void initialize_congruence_tactic() { register_simple_tac(name{"tactic", "congruence"}, congruence_tactic); } +void finalize_congruence_tactic() {} +} diff --git a/src/library/tactic/congruence_tactic.h b/src/library/tactic/congruence_tactic.h new file mode 100644 index 000000000..e08914a17 --- /dev/null +++ b/src/library/tactic/congruence_tactic.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +namespace lean { +void initialize_congruence_tactic(); +void finalize_congruence_tactic(); +} diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index a2f2788a1..a289a3c66 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -27,6 +27,7 @@ Author: Leonardo de Moura #include "library/tactic/exfalso_tactic.h" #include "library/tactic/constructor_tactic.h" #include "library/tactic/injection_tactic.h" +#include "library/tactic/congruence_tactic.h" namespace lean { void initialize_tactic_module() { @@ -53,9 +54,11 @@ void initialize_tactic_module() { initialize_exfalso_tactic(); initialize_constructor_tactic(); initialize_injection_tactic(); + initialize_congruence_tactic(); } void finalize_tactic_module() { + finalize_congruence_tactic(); finalize_injection_tactic(); finalize_constructor_tactic(); finalize_exfalso_tactic(); diff --git a/tests/lean/hott/congr_tac.hlean b/tests/lean/hott/congr_tac.hlean new file mode 100644 index 000000000..77714eb8e --- /dev/null +++ b/tests/lean/hott/congr_tac.hlean @@ -0,0 +1,46 @@ +example (f : nat → nat → nat) (a b c : nat) : b = c → f a b = f a c := +begin + intro bc, + congruence, + assumption +end + +example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c := +begin + intro fg bc, + congruence, + exact fg, + exact bc +end + +example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c := +by intros; congruence; assumption + +inductive list (A : Type) := +| nil {} : list A +| cons : A → list A → list A + +namespace list +notation `[` a `]` := list.cons a list.nil +notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l +notation h :: t := cons h t +variable {T : Type} +definition append : list T → list T → list T +| [] l := l +| (h :: s) t := h :: (append s t) +notation l₁ ++ l₂ := append l₁ l₂ +end list +open list + +example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] := +begin + intro ab, + congruence, + {congruence, + exact ab}, + {congruence, + exact (eq.symm ab)} +end + +example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] := +by intros; repeat (congruence | assumption | apply eq.symm) diff --git a/tests/lean/run/congr_tac.lean b/tests/lean/run/congr_tac.lean new file mode 100644 index 000000000..a08f419dc --- /dev/null +++ b/tests/lean/run/congr_tac.lean @@ -0,0 +1,34 @@ +import data.list + +example (f : nat → nat → nat) (a b c : nat) : b = c → f a b = f a c := +begin + intro bc, + congruence, + assumption +end + +example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c := +begin + intro fg bc, + congruence, + exact fg, + exact bc +end + +example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c := +by intros; congruence; assumption + +open list + +example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] := +begin + intro ab, + congruence, + {congruence, + exact ab}, + {congruence, + exact (eq.symm ab)} +end + +example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] := +by intros; repeat (congruence | assumption | apply eq.symm)