From bcf057f4f327de487e1c05da325d32d6d9e6bad5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Jul 2015 18:49:50 -0700 Subject: [PATCH] feat(frontends/lean): display '[congr]' attribute when printing theorems --- src/frontends/lean/builtin_cmds.cpp | 2 ++ src/library/simplifier/simp_rule_set.cpp | 12 +++++++++--- src/library/simplifier/simp_rule_set.h | 2 ++ tests/lean/congr_print.lean | 5 +++++ tests/lean/congr_print.lean.expected.out | 20 ++++++++++++++++++++ 5 files changed, 38 insertions(+), 3 deletions(-) create mode 100644 tests/lean/congr_print.lean create mode 100644 tests/lean/congr_print.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 6fdcbe2e7..fdfb768b4 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -192,6 +192,8 @@ void print_attributes(parser & p, name const & n) { out << " [instance]"; if (is_simp_rule(env, n)) out << " [simp]"; + if (is_congr_rule(env, n)) + out << " [congr]"; switch (get_reducible_status(env, n)) { case reducible_status::Reducible: out << " [reducible]"; break; case reducible_status::Irreducible: out << " [irreducible]"; break; diff --git a/src/library/simplifier/simp_rule_set.cpp b/src/library/simplifier/simp_rule_set.cpp index 85e8ab25b..14c39f7d6 100644 --- a/src/library/simplifier/simp_rule_set.cpp +++ b/src/library/simplifier/simp_rule_set.cpp @@ -382,16 +382,18 @@ void add_congr_core(environment const & env, simp_rule_sets & s, name const & n) struct rrs_state { simp_rule_sets m_sets; - name_set m_snames; + name_set m_simp_names; + name_set m_congr_names; void add_simp(environment const & env, name const & cname) { type_checker tc(env); m_sets = add_core(tc, m_sets, cname); - m_snames.insert(cname); + m_simp_names.insert(cname); } void add_congr(environment const & env, name const & n) { add_congr_core(env, m_sets, n); + m_congr_names.insert(n); } }; @@ -433,7 +435,11 @@ environment add_congr_rule(environment const & env, name const & n, bool persist } bool is_simp_rule(environment const & env, name const & n) { - return rrs_ext::get_state(env).m_snames.contains(n); + return rrs_ext::get_state(env).m_simp_names.contains(n); +} + +bool is_congr_rule(environment const & env, name const & n) { + return rrs_ext::get_state(env).m_congr_names.contains(n); } simp_rule_sets get_simp_rule_sets(environment const & env) { diff --git a/src/library/simplifier/simp_rule_set.h b/src/library/simplifier/simp_rule_set.h index 07d39d628..37dba7c8b 100644 --- a/src/library/simplifier/simp_rule_set.h +++ b/src/library/simplifier/simp_rule_set.h @@ -106,6 +106,8 @@ environment add_congr_rule(environment const & env, name const & n, bool persist /** \brief Return true if \c n is an active simplification rule in \c env */ bool is_simp_rule(environment const & env, name const & n); +/** \brief Return true if \c n is an active congruence rule in \c env */ +bool is_congr_rule(environment const & env, name const & n); /** \brief Get current simplification rule sets */ simp_rule_sets get_simp_rule_sets(environment const & env); /** \brief Get simplification rule sets in the given namespace. */ diff --git a/tests/lean/congr_print.lean b/tests/lean/congr_print.lean new file mode 100644 index 000000000..1ce78d87f --- /dev/null +++ b/tests/lean/congr_print.lean @@ -0,0 +1,5 @@ +import data.list +open list perm + +set_option pp.max_depth 10 +print perm_erase_dup_of_perm diff --git a/tests/lean/congr_print.lean.expected.out b/tests/lean/congr_print.lean.expected.out new file mode 100644 index 000000000..06597dbd9 --- /dev/null +++ b/tests/lean/congr_print.lean.expected.out @@ -0,0 +1,20 @@ +theorem perm.perm_erase_dup_of_perm [congr] : ∀ {A : Type} [H : decidable_eq A] {l₁ l₂ : list A}, l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ := +λ (A : Type) (H : decidable_eq A) (l₁ l₂ : list A) (p : l₁ ~ l₂), + perm_induction_on p nil + (λ (x : A) (t₁ t₂ : list A) (p : t₁ ~ t₂) (r : erase_dup t₁ ~ erase_dup t₂), + decidable.by_cases + (λ (xint₁ : x ∈ t₁), assert xint₂ : x ∈ t₂, from mem_of_mem_erase_dup …, … …) + (λ (nxint₁ : x ∉ t₁), + assert nxint₂ : x ∉ t₂, from λ (xint₂ : x ∈ t₂), … nxint₁, + eq.rec … (eq.symm …))) + (λ (y x : A) (t₁ t₂ : list A) (p : t₁ ~ t₂) (r : erase_dup t₁ ~ erase_dup t₂), + decidable.by_cases + (λ (xinyt₁ : x ∈ y :: t₁), + decidable.by_cases (λ (yint₁ : …), …) + (λ (nyint₁ : y ∉ t₁), assert nyint₂ : …, from …, …)) + (λ (nxinyt₁ : x ∉ y :: t₁), + have xney : x ≠ y, from ne_of_not_mem_cons nxinyt₁, + have nxint₁ : x ∉ t₁, from not_mem_of_not_mem_cons nxinyt₁, + assert nxint₂ : x ∉ t₂, from λ (xint₂ : …), …, + … …)) + (λ (t₁ t₂ t₃ : list A) (p₁ : t₁ ~ t₂) (p₂ : t₂ ~ t₃), trans)