michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/simplifier): check if the given types are convertible to ceq expected types

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-29 15:15:55 -08:00
parent 0bb8fe75b3
commit 4f3127d3d5
5 changed files with 131 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/simplifier/rewrite_rule_set.cpp
View file

@ -16,8 +16,9 @@ Author: Leonardo de Moura
namespace lean {
rewrite_rule::rewrite_rule(name const & id, expr const & lhs, expr const & rhs, expr const & ceq, expr const & proof,
unsigned num_args, bool is_permutation):
m_id(id), m_lhs(lhs), m_rhs(rhs), m_ceq(ceq), m_proof(proof), m_num_args(num_args), m_is_permutation(is_permutation) {
unsigned num_args, bool is_permutation, bool must_check):
m_id(id), m_lhs(lhs), m_rhs(rhs), m_ceq(ceq), m_proof(proof), m_num_args(num_args),
m_is_permutation(is_permutation), m_must_check_types(must_check) {
}
rewrite_rule_set::rewrite_rule_set(ro_environment const & env):m_env(env.to_weak_ref()) {}
@ -38,8 +39,9 @@ void rewrite_rule_set::insert(name const & id, expr const & th, expr const & pro
num++;
}
lean_assert(is_equality(eq));
bool must_check = true; // TODO(Leo): call procedure to test whether we must check types or not.
m_rule_set = cons(rewrite_rule(id, arg(eq, num_args(eq) - 2), arg(eq, num_args(eq) - 1),
ceq, proof, num, is_perm),
ceq, proof, num, is_perm, must_check),
m_rule_set);
}
}

4
src/library/simplifier/rewrite_rule_set.h
View file

@ -28,8 +28,9 @@ class rewrite_rule {
expr m_proof;
unsigned m_num_args;
bool m_is_permutation;
bool m_must_check_types; // if true, then we must check if the given types are convertible to the expected types
rewrite_rule(name const & id, expr const & lhs, expr const & rhs, expr const & ceq, expr const & proof,
unsigned num_args, bool is_permutation);
unsigned num_args, bool is_permutation, bool must_check);
public:
name const & get_id() const { return m_id; }
expr const & get_lhs() const { return m_lhs; }
@ -38,6 +39,7 @@ public:
expr const & get_proof() const { return m_proof; }
unsigned get_num_args() const { return m_num_args; }
bool is_permutation() const { return m_is_permutation; }
bool must_check_types() const { return m_must_check_types; }
};
/**

38
src/library/simplifier/simplifier.cpp
View file

@ -881,6 +881,37 @@ class simplifier_cell::imp {
new_rhs = instantiate(rhs, num, new_args.data() + 1);
if (rule.is_permutation() && !is_lt(new_rhs, target, false))
return false;
if (rule.must_check_types()) {
// This check is needed because of universe cumulativity.
// Consider the following example:
//
// universe U >= 2
// variable f (A : (Type 1)) : (Type 1)
// axiom Ax1 (a : Type) : f a = a
// rewrite_set S
// add_rewrite Ax1 eq_id : S
// theorem T1 (A : (Type 1)) : f A = A
// := by simp S
//
// The axiom Ax1 is only for arguments convertible to Type (i.e., Type 0), but
// argument A in T1 lives in (Type 1)
//
// In many cases, we can statically determine that this check is not needed.
// By statically, we mean the time we are inserting ceqs into rewrite rule sets.
expr ceq = rule.get_ceq();
unsigned i = 0;
while (is_pi(ceq)) {
expr arg = new_args[i+1];
if (!is_convertible(infer_type(arg), abst_domain(ceq))) {
if (m_monitor)
m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(),
i, simplifier_monitor::failure_kind::TypeMismatch);
return false;
}
ceq = instantiate(abst_body(ceq), arg);
i = i + 1;
}
}
if (m_proofs_enabled) {
if (num > 0) {
new_args[0] = rule.get_proof();
@ -904,6 +935,13 @@ class simplifier_cell::imp {
for (unsigned i = 0; i < num; i++) {
lean_assert(is_pi(ceq));
if (subst[i]) {
if (rule.must_check_types() && !is_convertible(infer_type(*subst[i]), abst_domain(ceq))) {
// See before the previous is_convertible
if (m_monitor)
m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(),
i, simplifier_monitor::failure_kind::TypeMismatch);
return false;
}
ceq = instantiate(abst_body(ceq), *subst[i]);
if (m_proofs_enabled)
proof_args.push_back(*subst[i]);

53
tests/lean/bad_simp2.lean Normal file
View file

@ -0,0 +1,53 @@
import tactic
universe U >= 2
variable f (A : (Type 1)) : (Type 1)
axiom Ax1 (a : Type) : f a = a
rewrite_set S
add_rewrite Ax1 eq_id : S
theorem T1a (A : Type) : f A = A
:= by simp S
-- The following theorem should not be provable.
-- The axiom Ax1 is only for arguments convertible to Type (i.e., Type 0)
-- The argument A in the following theorem lives in (Type 1)
theorem T1b (A : (Type 1)) : f A = A
:= by simp S
variable g (A : Type → (Type 1)) : (Type 1)
axiom Ax2 (a : Type → Type) : g a = a Bool
add_rewrite Ax2 : S
theorem T2a (A : Type → Type) : g A = A Bool
:= by simp S
-- The following theorem should not be provable.
-- See T1b
theorem T2b (A : Type → (Type 1)) : g A = A Bool
:= by simp S
variable h (A : Type) (B : (Type 1)) : (Type 1)
axiom Ax3 (a : Type) : h a a = a
add_rewrite Ax3 : S
theorem T3a (A : Type) : h A A = A
:= by simp S
axiom Ax4 (a b : Type) : h a b = b
add_rewrite Ax4 : S
theorem T4a (A : Type) (B : Type) : h A B = B
:= by simp S
-- The following theorem should not be provable.
-- See T1b
theorem T4b (A : Type) (B : (Type 1)) : h A B = B
:= by simp S
variable h2 (A : Type) (B : (Type 1)) : Type
axiom Ax5 (a b : Type) : f a = a -> h2 a b = a
add_rewrite Ax5 : S
theorem T5a (A B : Type) : h2 A B = A
:= by simp S
-- The following theorem should not be provable.
-- See T1b
theorem T5b (A : Type) (B : (Type 1)) : h2 A B = A
:= by simp S
print environment 1

32
tests/lean/bad_simp2.lean.expected.out Normal file
View file

@ -0,0 +1,32 @@
Set: pp::colors
Set: pp::unicode
Imported 'tactic'
Assumed: f
Assumed: Ax1
Proved: T1a
bad_simp2.lean:14:3: error: invalid 'done' command, proof cannot be produced from this state
Proof state:
A : (Type 1) ⊢ f A = A
Assumed: g
Assumed: Ax2
Proved: T2a
bad_simp2.lean:24:3: error: invalid 'done' command, proof cannot be produced from this state
Proof state:
A : Type → (Type 1) ⊢ g A = A Bool
Assumed: h
Assumed: Ax3
Proved: T3a
Assumed: Ax4
Proved: T4a
bad_simp2.lean:40:3: error: invalid 'done' command, proof cannot be produced from this state
Proof state:
A : Type, B : (Type 1) ⊢ h A B = B
Assumed: h2
Assumed: Ax5
Proved: T5a
bad_simp2.lean:51:3: error: invalid 'done' command, proof cannot be produced from this state
Proof state:
A : Type, B : (Type 1) ⊢ h2 A B = A
theorem T5a (A B : Type) : h2 A B = A :=
eqt_elim (trans (congr1 A (congr2 eq (Ax5 A B (eqt_elim (trans (congr1 A (congr2 eq (Ax1 A))) (eq_id A))))))
(eq_id A))