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

fix(tests/library/rewriter): app_rewriter1_tst

Browse source 
There was a bug in the app_rewriter1_tst. If we apply the ADD_COMM RW to
f(0), then the result should be f(0) since there is nothing to do for
ADD_COMM.

    f(0) = f(0)

The proof for this equality should be Refl(Nat, f(0)). But it was

    Refl(Nat -> Nat, f)

which is wrong. Somehow, the previous kernel didn't detect this type
mismatch and recent changes of the kernel found the problem.

I fixed the bug and re-enable the test as it was.
This commit is contained in:
Soonho Kong 2013-11-30 02:16:33 -05:00
parent f5f7380fbe
commit aed8b1fc73
1 changed files with 4 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/tests/library/rewriter/rewriter.cpp
View file

@ -15,6 +15,7 @@ Author: Soonho Kong
#include "library/arith/nat.h"
#include "library/rewriter/fo_match.h"
#include "library/rewriter/rewriter.h"
#include "library/rewriter/apply_rewriter_fn.h"
#include "library/basic_thms.h"
using namespace lean;
@ -395,8 +396,6 @@ static void try_rewriter2_tst() {
env.add_theorem("try2", concl, proof);
}
#if 0
// TODO(Leo): fix
static void app_rewriter1_tst() {
cout << "=== app_rewriter1_tst() ===" << std::endl;
// Theorem: Pi(x y : N), x + y = y + x := ADD_COMM x y
@ -440,9 +439,8 @@ static void app_rewriter1_tst() {
cout << "Concl = " << concl << std::endl
<< "Proof = " << proof << std::endl;
lean_assert_eq(concl, mk_eq(v, f1(nVal(0))));
lean_assert_eq(proof, Const("Refl")(Nat >> Nat, f1));
lean_assert_eq(proof, Refl(Nat, f1(nVal(0))));
env.add_theorem("app_rewriter1", concl, proof);
// ==========================================================
cout << "====================================================" << std::endl;
v = f1(a_plus_b);
result = app_try_comm_rewriter(env, ctx, v);
@ -454,7 +452,6 @@ static void app_rewriter1_tst() {
lean_assert_eq(proof,
Const("Congr2")(Nat, Fun(name("_"), Nat, Nat), a_plus_b, b_plus_a, f1, Const("ADD_COMM")(a, b)));
env.add_theorem("app_rewriter2", concl, proof);
// ==========================================================
cout << "====================================================" << std::endl;
v = f4(nVal(0), a_plus_b, nVal(0), b_plus_a);
result = app_try_comm_rewriter(env, ctx, v);
@ -463,7 +460,7 @@ static void app_rewriter1_tst() {
cout << "Concl = " << concl << std::endl
<< "Proof = " << proof << std::endl;
lean_assert_eq(concl, mk_eq(v, f4(nVal(0), b_plus_a, nVal(0), a_plus_b)));
// Congr Nat (fun _ : Nat, Nat) (f4 0 (Nat::add a b) 0) (f4 0 (Nat::add b a) 0) (Nat::add b a) (Nat::add a b) (Congr1 Nat (fun _ : Nat, (Nat -> Nat)) (f4 0 (Nat::add a b)) (f4 0 (Nat::add b a)) 0 (Congr2 Nat (fun _ : Nat, (Nat -> Nat -> Nat)) (Nat::add a b) (Nat::add b a) (f4 0) (ADD_COMM a b))) (ADD_COMM b a)
// Congr Nat (fun _ : Nat, Nat) (f4 0 (Nat::add a b) 0) (f4 0 (Nat::add b a) 0) (Nat::add b a) (Nat::add a b) (Congr1 Nat (fun _ : Nat, (Nat -> Nat)) (f4 0 (Nat::add a b)) (f4 0 (Nat::add b a)) 0 (Congr2 Nat (fun _ : Nat, (Nat -> Nat -> Nat)) (Nat::add a b) (Nat::add b a) (f4 0) (ADD_COMM a b))) (ADD_COMM b a)
lean_assert_eq(proof,
Const("Congr")(Nat, Fun(name("_"), Nat, Nat), f4(zero, a_plus_b, zero), f4(zero, b_plus_a, zero),
@ -476,7 +473,6 @@ static void app_rewriter1_tst() {
Const("ADD_COMM")(b, a)));
env.add_theorem("app_rewriter3", concl, proof);
}
#endif
static void repeat_rewriter1_tst() {
cout << "=== repeat_rewriter1_tst() ===" << std::endl;
@ -604,10 +600,7 @@ int main() {
orelse_rewriter2_tst();
try_rewriter1_tst();
try_rewriter2_tst();
// TODO(Leo): discuss with Soonho about this failure.
// The failure is probably due to a change in the normalizer.
// Now, The expression t == t does not normalize to True.
// app_rewriter1_tst();
app_rewriter1_tst();
repeat_rewriter1_tst();
repeat_rewriter2_tst();
return has_violations() ? 1 : 0;