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

Add castlib as an independent library

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-06 23:40:47 -07:00
parent 7a9d53d0d7
commit c674bb3790
9 changed files with 191 additions and 135 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/CMakeLists.txt
View file

@ -84,6 +84,7 @@ include_directories(${LEAN_SOURCE_DIR}/interval)
include_directories(${LEAN_SOURCE_DIR}/kernel)
include_directories(${LEAN_SOURCE_DIR}/library)
include_directories(${LEAN_SOURCE_DIR}/library/arith)
include_directories(${LEAN_SOURCE_DIR}/library/cast)
include_directories(${LEAN_SOURCE_DIR}/library/import_all)
include_directories(${LEAN_SOURCE_DIR}/parsers)
include_directories(${LEAN_SOURCE_DIR}/frontends/lean)
@ -102,6 +103,8 @@ add_subdirectory(library)
set(LEAN_LIBS ${LEAN_LIBS} library)
add_subdirectory(library/arith)
set(LEAN_LIBS ${LEAN_LIBS} arithlib)
add_subdirectory(library/cast)
set(LEAN_LIBS ${LEAN_LIBS} castlib)
add_subdirectory(library/import_all)
set(LEAN_LIBS ${LEAN_LIBS} import_all)
add_subdirectory(frontends/lean)

1
src/frontends/lean/lean_notation.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "basic_thms.h"
#include "lean_frontend.h"
#include "arithlibs.h"
#include "castlib.h"
namespace lean {
/**

112
src/kernel/builtin.cpp
View file

@ -141,99 +141,6 @@ public:
MK_BUILTIN(if_fn, if_fn_value);
// =======================================
// =======================================
// cast builtin operator
static name g_cast_name("Cast");
static format g_cast_fmt(g_cast_name);
expr mk_Cast_fn();
class cast_fn_value : public value {
expr m_type;
public:
cast_fn_value() {
expr A = Const("A");
expr B = Const("B");
// Cast: Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B
m_type = Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B));
}
virtual ~cast_fn_value() {}
virtual expr get_type() const { return m_type; }
virtual name get_name() const { return g_cast_name; }
virtual bool normalize(unsigned num_as, expr const * as, expr & r) const {
if (num_as > 4 && as[1] == as[2]) {
// Cast T T H a == a
if (num_as == 5)
r = as[4];
else
r = mk_app(num_as - 4, as + 4);
return true;
} else if (is_app(as[4]) &&
arg(as[4], 0) == mk_Cast_fn() &&
num_args(as[4]) == 5 &&
as[1] == arg(as[4], 2)) {
// Cast T1 T2 H1 (Cast T3 T1 H2 a) == Cast T3 T2 (Trans H1 H2) a
expr const & nested = as[4];
expr const & T1 = as[1];
expr const & T2 = as[2];
expr const & T3 = arg(nested, 1);
expr const & H1 = as[3];
expr const & H2 = arg(nested, 3);
expr const & a = arg(nested, 4);
expr c = Cast(T3, T2, Trans(TypeU, T3, T1, T2, H1, H2), a);
if (num_as == 5) {
r = c;
} else {
buffer<expr> new_as;
new_as.push_back(c);
new_as.append(num_as - 5, as + 5);
r = mk_app(new_as.size(), new_as.data());
}
return true;
} else if (num_as > 5 && is_pi(as[1]) && is_pi(as[2])) {
// cast T1 T2 H f a_1 ... a_k
// Propagate application over cast.
// Remark: we check if T1 is a Pi to prevent non-termination
// For example, H can be a bogus hypothesis that shows
// that A == A -> A
// Since T1 and T2 are Pi's, we decompose them
expr const & T1 = as[1]; // Pi x : A1, B1
expr const & T2 = as[2]; // Pi x : A2, B2
expr const & H = as[3];
expr const & f = as[4];
expr const & a_1 = as[5]; // has type A2
expr const & A1 = abst_domain(T1);
expr const & B1 = abst_body(T1);
expr const & A2 = abst_domain(T2);
expr const & B2 = abst_body(T2);
expr B1f = mk_lambda(abst_name(T1), A1, B1);
expr B2f = mk_lambda(abst_name(T2), A2, B2);
expr A1_eq_A2 = DomInj(A1, A2, B1f, B2f, H);
name t("t");
expr A2_eq_A1 = Symm(TypeU, A1, A2, A1_eq_A2);
expr a_1p = Cast(A2, A1, A2_eq_A1, a_1);
expr fa_1 = f(a_1p);
// Cast fa_1 back to B2 since the type of cast T1 T2 H f a_1
// is in B2 a_1p
expr B1_eq_B2_at_a_1p = RanInj(A1, A2, B1f, B2f, H, a_1p);
expr fa_1_B2 = Cast(B1, B2, B1_eq_B2_at_a_1p, fa_1);
if (num_as == 6) {
r = fa_1_B2;
} else {
buffer<expr> new_as;
new_as.push_back(fa_1_B2);
new_as.append(num_as - 6, as + 6);
r = mk_app(new_as.size(), new_as.data());
}
return true;
} else {
return false;
}
}
};
MK_BUILTIN(Cast_fn, cast_fn_value);
// =======================================
MK_CONSTANT(implies_fn, name("implies"));
MK_CONSTANT(iff_fn, name("iff"));
MK_CONSTANT(and_fn, name("and"));
@ -242,7 +149,6 @@ MK_CONSTANT(not_fn, name("not"));
MK_CONSTANT(forall_fn, name("forall"));
MK_CONSTANT(exists_fn, name("exists"));
MK_CONSTANT(homo_eq_fn, name("heq"));
MK_CONSTANT(cast_fn, name("cast"));
// Axioms
MK_CONSTANT(mp_fn, name("MP"));
@ -252,8 +158,6 @@ MK_CONSTANT(case_fn, name("Case"));
MK_CONSTANT(subst_fn, name("Subst"));
MK_CONSTANT(eta_fn, name("Eta"));
MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
MK_CONSTANT(dom_inj_fn, name("DomInj"));
MK_CONSTANT(ran_inj_fn, name("RanInj"));
// Basic theorems
MK_CONSTANT(symm_fn, name("Symm"));
@ -273,13 +177,10 @@ void add_basic_theory(environment & env) {
expr x = Const("x");
expr y = Const("y");
expr A = Const("A");
expr Ap = Const("A'");
expr A_pred = A >> Bool;
expr B = Const("B");
expr Bp = Const("B'");
expr q_type = Pi({A, TypeU}, A_pred >> Bool);
expr piABx = Pi({x, A}, B(x));
expr piApBpx = Pi({x, Ap}, Bp(x));
expr A_arrow_u = A >> TypeU;
expr P = Const("P");
expr H = Const("H");
@ -290,7 +191,6 @@ void add_basic_theory(environment & env) {
env.add_builtin(mk_bool_value(true));
env.add_builtin(mk_bool_value(false));
env.add_builtin(mk_if_fn());
env.add_builtin(mk_Cast_fn());
// implies(x, y) := if x y True
env.add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
@ -315,10 +215,6 @@ void add_basic_theory(environment & env) {
// homogeneous equality
env.add_definition(homo_eq_fn_name, Pi({{A,TypeU},{x,A},{y,A}}, Bool), Fun({{A,TypeU}, {x,A}, {y,A}}, Eq(x, y)));
// Alias for Cast operator. We create the alias to be able to mark
// implicit arguments.
env.add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B)), mk_Cast_fn());
// MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
env.add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));
@ -340,14 +236,6 @@ void add_basic_theory(environment & env) {
// ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b
env.add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b)));
// DomInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
env.add_axiom(dom_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}}, Eq(A, Ap)));
// RanInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
// B a = B' (cast A A' (DomInj A A' B B' H) a)
env.add_axiom(ran_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}, {a, A}},
Eq(B(a), Bp(Cast(A, Ap, DomInj(A, Ap, B, Bp, H), a)))));
// Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a
env.add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)),
Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}},

20
src/kernel/builtin.h
View file

@ -113,12 +113,6 @@ expr mk_homo_eq_fn();
inline expr mk_homo_eq(expr const & A, expr const & l, expr const & r) { return mk_app(mk_homo_eq_fn(), A, l, r); }
inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_homo_eq(A, l, r); }
/** \brief Type Cast. It has type <tt>Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B</tt> */
expr mk_cast_fn();
/** \brief Return the term (cast A B H a) */
inline expr mk_cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_app(mk_cast_fn(), A, B, H, a); }
inline expr Cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_cast(A, B, H, a); }
/** \brief Modus Ponens axiom */
expr mk_mp_fn();
/** \brief (Axiom) {a : Bool}, {b : Bool}, H1 : a => b, H2 : a |- MP(a, b, H1, H2) : b */
@ -154,20 +148,6 @@ expr mk_imp_antisym_fn();
/** \brief (Axiom) {a : Bool}, {b : Bool}, H1 : a => b, H2 : b => a |- ImpAntisym(a, b, H1, H2) : a = b */
inline expr ImpAntisym(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_imp_antisym_fn(), a, b, H1, H2); }
/** \brief Domain Injectivity. It has type <tt>Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A' </tt> */
expr mk_dom_inj_fn();
/** \brief Return the term (DomInj A A' B B' H) */
inline expr mk_dom_inj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H) { return mk_app({mk_dom_inj_fn(), A, Ap, B, Bp, H}); }
inline expr DomInj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H) { return mk_dom_inj(A, Ap, B, Bp, H); }
/** \brief Range Injectivity. It has type <tt>Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
B a = B' (cast A A' (DomInj A A' B B' H) a)</tt>
*/
expr mk_ran_inj_fn();
/** \brief Return the term (RanInj A A' B B' H) */
inline expr mk_ran_inj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) { return mk_app({mk_ran_inj_fn(), A, Ap, B, Bp, H, a}); }
inline expr RanInj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) { return mk_ran_inj(A, Ap, B, Bp, H, a); }
expr mk_symm_fn();
/** \brief (Theorem) {A : Type u}, {a b : A}, H : a = b |- Symm(A, a, b, H) : b = a */
inline expr Symm(expr const & A, expr const & a, expr const & b, expr const & H) { return mk_app(mk_symm_fn(), A, a, b, H); }

2
src/library/cast/CMakeLists.txt Normal file
View file

@ -0,0 +1,2 @@
add_library(castlib castlib.cpp)
target_link_libraries(castlib ${LEAN_LIBS})

134
src/library/cast/castlib.cpp Normal file
View file

@ -0,0 +1,134 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "castlib.h"
#include "environment.h"
#include "abstract.h"
#include "builtin.h"
namespace lean {
// Cast builtin operator
static name g_cast_name("Cast");
static format g_cast_fmt(g_cast_name);
expr mk_Cast_fn();
class cast_fn_value : public value {
expr m_type;
public:
cast_fn_value() {
expr A = Const("A");
expr B = Const("B");
// Cast: Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B
m_type = Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B));
}
virtual ~cast_fn_value() {}
virtual expr get_type() const { return m_type; }
virtual name get_name() const { return g_cast_name; }
virtual bool normalize(unsigned num_as, expr const * as, expr & r) const {
if (num_as > 4 && as[1] == as[2]) {
// Cast T T H a == a
if (num_as == 5)
r = as[4];
else
r = mk_app(num_as - 4, as + 4);
return true;
} else if (is_app(as[4]) &&
arg(as[4], 0) == mk_Cast_fn() &&
num_args(as[4]) == 5 &&
as[1] == arg(as[4], 2)) {
// Cast T1 T2 H1 (Cast T3 T1 H2 a) == Cast T3 T2 (Trans H1 H2) a
expr const & nested = as[4];
expr const & T1 = as[1];
expr const & T2 = as[2];
expr const & T3 = arg(nested, 1);
expr const & H1 = as[3];
expr const & H2 = arg(nested, 3);
expr const & a = arg(nested, 4);
expr c = Cast(T3, T2, Trans(TypeU, T3, T1, T2, H1, H2), a);
if (num_as == 5) {
r = c;
} else {
buffer<expr> new_as;
new_as.push_back(c);
new_as.append(num_as - 5, as + 5);
r = mk_app(new_as.size(), new_as.data());
}
return true;
} else if (num_as > 5 && is_pi(as[1]) && is_pi(as[2])) {
// cast T1 T2 H f a_1 ... a_k
// Propagate application over cast.
// Remark: we check if T1 is a Pi to prevent non-termination
// For example, H can be a bogus hypothesis that shows
// that A == A -> A
// Since T1 and T2 are Pi's, we decompose them
expr const & T1 = as[1]; // Pi x : A1, B1
expr const & T2 = as[2]; // Pi x : A2, B2
expr const & H = as[3];
expr const & f = as[4];
expr const & a_1 = as[5]; // has type A2
expr const & A1 = abst_domain(T1);
expr const & B1 = abst_body(T1);
expr const & A2 = abst_domain(T2);
expr const & B2 = abst_body(T2);
expr B1f = mk_lambda(abst_name(T1), A1, B1);
expr B2f = mk_lambda(abst_name(T2), A2, B2);
expr A1_eq_A2 = DomInj(A1, A2, B1f, B2f, H);
name t("t");
expr A2_eq_A1 = Symm(TypeU, A1, A2, A1_eq_A2);
expr a_1p = Cast(A2, A1, A2_eq_A1, a_1);
expr fa_1 = f(a_1p);
// Cast fa_1 back to B2 since the type of cast T1 T2 H f a_1
// is in B2 a_1p
expr B1_eq_B2_at_a_1p = RanInj(A1, A2, B1f, B2f, H, a_1p);
expr fa_1_B2 = Cast(B1, B2, B1_eq_B2_at_a_1p, fa_1);
if (num_as == 6) {
r = fa_1_B2;
} else {
buffer<expr> new_as;
new_as.push_back(fa_1_B2);
new_as.append(num_as - 6, as + 6);
r = mk_app(new_as.size(), new_as.data());
}
return true;
} else {
return false;
}
}
};
MK_BUILTIN(Cast_fn, cast_fn_value);
MK_CONSTANT(cast_fn, name("cast"));
MK_CONSTANT(dom_inj_fn, name("DomInj"));
MK_CONSTANT(ran_inj_fn, name("RanInj"));
void import_castlib(environment & env) {
if (env.find_object(to_value(mk_Cast_fn()).get_name()))
return;
expr x = Const("x");
expr A = Const("A");
expr Ap = Const("A'");
expr B = Const("B");
expr Bp = Const("B'");
expr piABx = Pi({x, A}, B(x));
expr piApBpx = Pi({x, Ap}, Bp(x));
expr H = Const("H");
expr a = Const("a");
expr b = Const("b");
env.add_builtin(mk_Cast_fn());
// Alias for Cast operator. We create the alias to be able to mark
// implicit arguments.
env.add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B)), mk_Cast_fn());
// DomInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
env.add_axiom(dom_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}}, Eq(A, Ap)));
// RanInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
// B a = B' (cast A A' (DomInj A A' B B' H) a)
env.add_axiom(ran_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}, {a, A}},
Eq(B(a), Bp(Cast(A, Ap, DomInj(A, Ap, B, Bp, H), a)))));
}
}

45
src/library/cast/castlib.h Normal file
View file

@ -0,0 +1,45 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "expr.h"
namespace lean {
/** \brief Type Cast. It has type <tt>Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B</tt> */
expr mk_cast_fn();
/** \brief Return the term (cast A B H a) */
inline expr mk_cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_app(mk_cast_fn(), A, B, H, a); }
inline expr Cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_cast(A, B, H, a); }
/** \brief Domain Injectivity.
It has type <tt>Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A' </tt>
*/
expr mk_dom_inj_fn();
/** \brief Return the term (DomInj A A' B B' H) */
inline expr mk_dom_inj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H) {
return mk_app({mk_dom_inj_fn(), A, Ap, B, Bp, H});
}
inline expr DomInj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H) {
return mk_dom_inj(A, Ap, B, Bp, H);
}
/** \brief Range Injectivity.
It has type <tt>Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
B a = B' (cast A A' (DomInj A A' B B' H) a)</tt>
*/
expr mk_ran_inj_fn();
/** \brief Return the term (RanInj A A' B B' H) */
inline expr mk_ran_inj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) {
return mk_app({mk_ran_inj_fn(), A, Ap, B, Bp, H, a});
}
inline expr RanInj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) {
return mk_ran_inj(A, Ap, B, Bp, H, a);
}
class environment;
/** \brief Import type "casting" library */
void import_castlib(environment & env);
}

2
src/library/import_all/import_all.cpp
View file

@ -8,12 +8,14 @@ Author: Leonardo de Moura
#include "builtin.h"
#include "basic_thms.h"
#include "arithlibs.h"
#include "castlib.h"
namespace lean {
void import_all(environment & env) {
add_basic_theory(env);
add_basic_thms(env);
import_arithlibs(env);
import_castlib(env);
}
environment mk_toplevel() {
environment r;

7
src/tests/kernel/threads.cpp
View file

@ -18,8 +18,7 @@ Author: Leonardo de Moura
#include "test.h"
using namespace lean;
expr normalize(expr const & e) {
environment env = mk_toplevel();
expr norm(expr const & e, environment & env) {
env.add_var("a", Int);
env.add_var("b", Int);
env.add_var("f", Int >> (Int >> Int));
@ -28,6 +27,7 @@ expr normalize(expr const & e) {
}
static void mk(expr const & a) {
environment env = mk_toplevel();
expr b = Const("b");
for (unsigned i = 0; i < 100; i++) {
expr h = Const("h");
@ -36,7 +36,8 @@ static void mk(expr const & a) {
h = mk_app(h, b);
h = max_sharing(h);
lean_assert(closed(h));
h = normalize(h);
environment env2 = env.mk_child();
h = norm(h, env2);
h = abstract(h, a);
lean_assert(!closed(h));
h = deep_copy(h);