max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-06 10:26:58 -08:00
parent 31a0d7d520
commit db70c78704
14 changed files with 79 additions and 68 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/data/int/basic.lean
View file

@ -59,11 +59,11 @@ end
private lemma sub_nat_nat_of_sub_eq_zero {m n : ℕ} (h : n - m = 0) :
sub_nat_nat m n = of_nat (m - n) :=
begin unfold sub_nat_nat, rw [h, sub_nat_nat._match_1.equations.eqn_1] end
begin unfold sub_nat_nat, rw h, unfold sub_nat_nat._match_1, reflexivity end
private lemma sub_nat_nat_of_sub_eq_succ {m n k : ℕ} (h : n - m = succ k) :
sub_nat_nat m n = -[1+ k] :=
begin unfold sub_nat_nat, rw [h, sub_nat_nat._match_1.equations.eqn_2] end
begin unfold sub_nat_nat, rw h, unfold sub_nat_nat._match_1, reflexivity end
protected def neg : ℤ → ℤ
| (of_nat n) := neg_of_nat n
@ -276,7 +276,7 @@ protected lemma mul_comm : ∀ a b : ℤ, a * b = b * a
private lemma of_nat_mul_neg_of_nat (m : ℕ) :
∀ n, of_nat m * neg_of_nat n = neg_of_nat (m * n)
| 0 := rfl
| (succ n) := by simp [neg_of_nat.equations.eqn_2]
| (succ n) := begin unfold neg_of_nat, simp end
private lemma neg_of_nat_mul_of_nat (m n : ℕ) :
neg_of_nat m * of_nat n = neg_of_nat (m * n) :=
@ -285,7 +285,7 @@ begin rw int.mul_comm, simp [of_nat_mul_neg_of_nat] end
private lemma neg_succ_of_nat_mul_neg_of_nat (m : ℕ) :
∀ n, -[1+ m] * neg_of_nat n = of_nat (succ m * n)
| 0 := rfl
| (succ n) := by simp [neg_of_nat.equations.eqn_2]
| (succ n) := begin unfold neg_of_nat, simp end
private lemma neg_of_nat_mul_neg_succ_of_nat (m n : ℕ) :
neg_of_nat n * -[1+ m] = of_nat (n * succ m) :=

5
src/frontends/lean/definition_cmds.cpp
View file

@ -514,8 +514,7 @@ static environment copy_equation_lemmas(environment const & env, name const & d_
environment new_env = env;
unsigned i = 1;
while (true) {
name eqn_suffix = name({"equations", "eqn"}).append_after(i);
name eqn_name = const_name(fn) + eqn_suffix;
name eqn_name = mk_equation_name(const_name(fn), i);
optional<declaration> eqn_decl = env.find(eqn_name);
if (!eqn_decl) break;
unsigned num_eqn_levels = eqn_decl->get_num_univ_params();
@ -548,7 +547,7 @@ static environment copy_equation_lemmas(environment const & env, name const & d_
return none_expr();
});
new_eqn_type = locals.mk_pi(new_eqn_type);
name new_eqn_name = d_name + eqn_suffix;
name new_eqn_name = mk_equation_name(d_name, i);
expr new_eqn_value;
new_eqn_value = mk_app(mk_constant(eqn_name, eqn_levels), args);
new_eqn_value = locals.mk_lambda(new_eqn_value);

4
src/library/equations_compiler/util.cpp
View file

@ -532,8 +532,8 @@ static expr prove_eqn_lemma(type_context & ctx, buffer<expr> const & Hs, expr co
return ctx.mk_lambda(Hs, body);
}
static name mk_equation_name(name const & f_name, unsigned eqn_idx) {
return name(name(f_name, "equations"), "eqn").append_after(eqn_idx);
name mk_equation_name(name const & f_name, unsigned eqn_idx) {
return name(name(f_name, "equations"), "_eqn").append_after(eqn_idx);
}
environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,

2
src/library/equations_compiler/util.h
View file

@ -97,6 +97,8 @@ environment mk_equation_lemma(environment const & env, options const & opts, met
This function is used to make sure we have equations for all definitions. */
environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, unsigned arity);
name mk_equation_name(name const & f_name, unsigned eqn_idx);
void initialize_eqn_compiler_util();
void finalize_eqn_compiler_util();
}

18
src/library/tactic/eqn_lemmas.cpp
View file

@ -12,7 +12,11 @@ Author: Leonardo de Moura
#include "library/util.h"
#include "library/constants.h"
#include "library/module.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_list.h"
#include "library/equations_compiler/util.h"
#include "library/tactic/eqn_lemmas.h"
#include "library/tactic/tactic_state.h"
namespace lean {
struct eqn_lemmas_ext : public environment_extension {
@ -96,10 +100,9 @@ void get_eqn_lemmas_for(environment const & env, name const & cname, bool refl_o
}
void get_eqn_lemmas_for(environment const & env, name const & cname, buffer<name> & result) {
name base(name(cname, "equations"), "eqn");
unsigned idx = 1;
while (true) {
name eqn = base.append_after(idx);
name eqn = mk_equation_name(cname, idx);
if (env.find(eqn)) {
result.push_back(eqn);
idx++;
@ -128,6 +131,16 @@ void get_ext_eqn_lemmas_for(environment const & env, name const & cname, buffer<
}
}
vm_obj tactic_get_eqn_lemmas_for(vm_obj const & all, vm_obj const & n, vm_obj const & s) {
buffer<name> result;
if (to_bool(all)) {
get_ext_eqn_lemmas_for(to_tactic_state(s).env(), to_name(n), result);
} else {
get_eqn_lemmas_for(to_tactic_state(s).env(), to_name(n), result);
}
return mk_tactic_success(to_obj(result), to_tactic_state(s));
}
bool has_eqn_lemmas(environment const & env, name const & cname) {
eqn_lemmas_ext const & ext = get_extension(env);
return ext.m_lemmas.contains(cname);
@ -136,6 +149,7 @@ bool has_eqn_lemmas(environment const & env, name const & cname) {
void initialize_eqn_lemmas() {
g_ext = new eqn_lemmas_ext_reg();
eqn_lemmas_modification::init();
DECLARE_VM_BUILTIN(name({"tactic", "get_eqn_lemmas_for"}), tactic_get_eqn_lemmas_for);
}
void finalize_eqn_lemmas() {

2
tests/lean/def_inaccessible_issue.lean
View file

@ -14,4 +14,4 @@ definition map2 : ∀ {n}, bv n → bv n → bv n
| 0 nil nil := nil
| (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2)
check map2.equations.eqn_2
check map2.equations._eqn_2

2
tests/lean/def_inaccessible_issue.lean.expected.out
View file

@ -1,3 +1,3 @@
map2.equations.eqn_2 :
map2.equations._eqn_2 :
∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv n) (b2 : bool) (v2 : bv n),
map2 f (cons n b1 v1) (cons n b2 v2) = cons n (f b1 b2) (map2 f v1 v2)

13
tests/lean/run/def_complete_bug.lean
View file

@ -1,4 +1,3 @@
definition g : list nat → list nat → nat
| [] (y::ys) := y
| [] ys := 0
@ -6,9 +5,9 @@ definition g : list nat → list nat → nat
| (x::xs) (y::ys) := g xs ys + y
| (x::xs) [] := g xs []
print g._main.equations.eqn_1
print g._main.equations.eqn_2
print g._main.equations.eqn_3
print g._main.equations.eqn_4
print g._main.equations.eqn_5
print g._main.equations.eqn_6
print g._main.equations._eqn_1
print g._main.equations._eqn_2
print g._main.equations._eqn_3
print g._main.equations._eqn_4
print g._main.equations._eqn_5
print g._main.equations._eqn_6

9
tests/lean/run/def_ite_value.lean
View file

@ -1,4 +1,3 @@
inductive bv : nat → Type
| nil : bv 0
| cons : Π n, bool → bv n → bv (n+1)
@ -12,9 +11,9 @@ definition f : ∀ n : nat, bv n → nat → nat
set_option pp.binder_types true
check @f._main.equations.eqn_1
check @f._main.equations.eqn_2
check @f._main.equations.eqn_3
check @f._main.equations._eqn_1
check @f._main.equations._eqn_2
check @f._main.equations._eqn_3
example (n : nat) (b : bool) (v : bv n) (x : nat) : x ≠ 1000000 → f (n+1) (cons n b v) x = f n v (x + 1) :=
assume H, f._main.equations.eqn_3 n b v x H
assume H, f._main.equations._eqn_3 n b v x H

42
tests/lean/run/equation_with_values.lean
View file

@ -6,12 +6,12 @@ def f : char → nat
| #"e" := 4
| _ := 5
check f.equations.eqn_1
check f.equations.eqn_2
check f.equations.eqn_3
check f.equations.eqn_4
check f.equations.eqn_5
check f.equations.eqn_6
check f.equations._eqn_1
check f.equations._eqn_2
check f.equations._eqn_3
check f.equations._eqn_4
check f.equations._eqn_5
check f.equations._eqn_6
def g : nat → nat
| 100000 := 0
@ -20,11 +20,11 @@ def g : nat → nat
| 400000 := 3
| _ := 5
check g.equations.eqn_1
check g.equations.eqn_2
check g.equations.eqn_3
check g.equations.eqn_4
check g.equations.eqn_5
check g.equations._eqn_1
check g.equations._eqn_2
check g.equations._eqn_3
check g.equations._eqn_4
check g.equations._eqn_5
def h : string → nat
| "hello" := 0
@ -33,19 +33,19 @@ def h : string → nat
| "boo" := 3
| _ := 5
check h.equations.eqn_1
check h.equations.eqn_2
check h.equations.eqn_3
check h.equations.eqn_4
check h.equations.eqn_5
check h.equations._eqn_1
check h.equations._eqn_2
check h.equations._eqn_3
check h.equations._eqn_4
check h.equations._eqn_5
def r : string × string → nat
| ("hello", "world") := 0
| ("world", "hello") := 1
| _ := 2
check r.equations.eqn_1
check r.equations.eqn_2
check r.equations.eqn_3
check r.equations.eqn_4
check r.equations.eqn_5
check r.equations._eqn_1
check r.equations._eqn_2
check r.equations._eqn_3
check r.equations._eqn_4
check r.equations._eqn_5

7
tests/lean/run/lift_nested_rec.lean
View file

@ -1,4 +1,3 @@
definition f : nat → (nat × nat) → nat
| 0 m := m.1
| (n+1) m :=
@ -6,6 +5,6 @@ definition f : nat → (nat × nat) → nat
| (a, b) := (f n (b, a + 1)) + (f n (a, b))
end
check @f._main.equations.eqn_1
check @f._main.equations.eqn_2
check @f._match_1.equations.eqn_1
check @f._main.equations._eqn_1
check @f._main.equations._eqn_2
check @f._match_1.equations._eqn_1

13
tests/lean/run/pack_unpack1.lean
View file

@ -1,4 +1,3 @@
inductive tree_core (A : Type*) : bool → Type*
| leaf' : A → tree_core ff
| node' : tree_core tt → tree_core ff
@ -66,8 +65,8 @@ noncomputable definition bla {A : Type*} : ∀ n : tree A, P n
| (tree.leaf a) := mk1 a
| (tree.node l) := mk2 l
check bla._main.equations.eqn_1
check bla._main.equations.eqn_2
check bla._main.equations._eqn_1
check bla._main.equations._eqn_2
definition foo {A : Type*} : nat → tree A → nat
| 0 _ := 0
@ -75,7 +74,7 @@ definition foo {A : Type*} : nat → tree A → nat
| (n+1) (tree.node []) := foo n (tree.node [])
| (n+1) (tree.node (x::xs)) := foo n x
check @foo._main.equations.eqn_1
check @foo._main.equations.eqn_2
check @foo._main.equations.eqn_3
check @foo._main.equations.eqn_4
check @foo._main.equations._eqn_1
check @foo._main.equations._eqn_2
check @foo._main.equations._eqn_3
check @foo._main.equations._eqn_4

12
tests/lean/run/pack_unpack2.lean
View file

@ -16,8 +16,8 @@ noncomputable definition bla {A : Type*} : ∀ n : tree A, P n
| (tree.leaf a) := mk1 a
| (tree.node l) := mk2 l
check bla._main.equations.eqn_1
check bla._main.equations.eqn_2
check bla._main.equations._eqn_1
check bla._main.equations._eqn_2
noncomputable definition foo {A : Type*} : nat → tree A → nat
| 0 _ := sorry
@ -25,7 +25,7 @@ noncomputable definition foo {A : Type*} : nat → tree A → nat
| (n+1) (tree.node []) := foo n (tree.node [])
| (n+1) (tree.node (x::xs)) := foo n x
check @foo._main.equations.eqn_1
check @foo._main.equations.eqn_2
check @foo._main.equations.eqn_3
check @foo._main.equations.eqn_4
check @foo._main.equations._eqn_1
check @foo._main.equations._eqn_2
check @foo._main.equations._eqn_3
check @foo._main.equations._eqn_4

10
tests/lean/run/pack_unpack3.lean
View file

@ -16,14 +16,14 @@ noncomputable definition bla {A : Type*} : ∀ n : tree A, P n
| (tree.leaf a) := mk1 a
| (tree.node n xs) := mk2 n xs
check bla._main.equations.eqn_1
check bla._main.equations.eqn_2
check bla._main.equations._eqn_1
check bla._main.equations._eqn_2
noncomputable definition foo {A : Type*} : nat → tree A → nat
| 0 _ := sorry
| (n+1) (tree.leaf a) := 0
| (n+1) (tree.node m xs) := foo n (tree.node m xs)
check @foo._main.equations.eqn_1
check @foo._main.equations.eqn_2
check @foo._main.equations.eqn_3
check @foo._main.equations._eqn_1
check @foo._main.equations._eqn_2
check @foo._main.equations._eqn_3