From 11b1f416f6f4c0e9ee6c5776d4f411c0e3ff52a8 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 4 Aug 2015 13:20:13 +0200 Subject: [PATCH] feat(nat): add unfold attributes to add, mul, sub and of_num in namespace nat_esimp in both libraries --- hott/init/nat.hlean | 6 ++++++ hott/init/num.hlean | 2 +- library/init/nat.lean | 6 ++++++ library/init/num.lean | 2 +- tests/lean/693.lean | 2 +- tests/lean/693.lean.expected.out | 4 ++-- 6 files changed, 17 insertions(+), 5 deletions(-) diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index 19953fb4f..9187f2788 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -290,3 +290,9 @@ namespace nat lemma sub_lt_succ (a b : ℕ) : a - b < succ a := lt_succ_of_le (sub_le a b) end nat + +namespace nat_esimp + open nat + attribute add mul sub [unfold 2] + attribute of_num [unfold 1] +end nat_esimp diff --git a/hott/init/num.hlean b/hott/init/num.hlean index 5e67d8aa7..a38e9dd93 100644 --- a/hott/init/num.hlean +++ b/hott/init/num.hlean @@ -130,4 +130,4 @@ namespace nat num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n end nat -attribute nat.of_num [reducible] [constructor] -- of_num is also reducible if namespace "nat" is not opened +attribute nat.of_num [reducible] -- of_num is also reducible if namespace "nat" is not opened diff --git a/library/init/nat.lean b/library/init/nat.lean index 6033c5fff..18e4f1dbc 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -247,3 +247,9 @@ namespace nat theorem sub_lt_succ_iff_true [simp] (a b : ℕ) : a - b < succ a ↔ true := iff_true_intro !sub_lt_succ end nat + +namespace nat_esimp + open nat + attribute add mul sub [unfold 2] + attribute of_num [unfold 1] +end nat_esimp diff --git a/library/init/num.lean b/library/init/num.lean index ca83897be..2884e7da2 100644 --- a/library/init/num.lean +++ b/library/init/num.lean @@ -127,4 +127,4 @@ namespace nat num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n end nat -attribute nat.of_num [reducible] [constructor] -- of_num is also reducible if namespace "nat" is not opened +attribute nat.of_num [reducible] -- of_num is also reducible if namespace "nat" is not opened diff --git a/tests/lean/693.lean b/tests/lean/693.lean index ef3008ecb..34f9c9064 100644 --- a/tests/lean/693.lean +++ b/tests/lean/693.lean @@ -1,4 +1,4 @@ -open nat +open nat nat_esimp definition foo [unfold 1 3] (a : nat) (b : nat) (c :nat) : nat := (a + c) * b diff --git a/tests/lean/693.lean.expected.out b/tests/lean/693.lean.expected.out index 1e7240e2f..b14394183 100644 --- a/tests/lean/693.lean.expected.out +++ b/tests/lean/693.lean.expected.out @@ -1,7 +1,7 @@ 693.lean:10:2: proof state c : ℕ, h : c = 1 -⊢ (1 + 0) * c = (1 + 0) * 1 +⊢ 1 * c = 1 693.lean:18:2: proof state b c : ℕ, h : c = 1 @@ -13,4 +13,4 @@ h : c = 1 693.lean:34:2: proof state b c : ℕ, h : c = 1 -⊢ (1 + 1) * c = foo c 1 1 +⊢ 2 * c = foo c 1 1