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

Add add_theorem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-06 12:24:20 -07:00
parent 9d6b421be9
commit ab915fb3f0
3 changed files with 30 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/kernel/builtin.cpp
View file

@ -204,15 +204,15 @@ void add_basic_theory(environment & env) {
// symm : Pi (A : Type u) (a b : A) (H : a = b), b = a :=
// Subst A (Fun x : A => x = a) a b (Refl A a) H
env.add_definition(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)}},
Subst(A, Fun({x, A}, Eq(x,a)), a, b, Refl(A, a), H)));
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)}},
Subst(A, Fun({x, A}, Eq(x,a)), a, b, Refl(A, a), H)));
// trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c :=
// Subst A (Fun x : A => a = x) b c H1 H2
env.add_definition(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a,b)}, {H2, Eq(b,c)}},
Subst(A, Fun({x, A}, Eq(a, x)), b, c, H1, H2)));
env.add_theorem(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a,b)}, {H2, Eq(b,c)}},
Subst(A, Fun({x, A}, Eq(a, x)), b, c, H1, H2)));
// congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b
expr piABx = Pi({x, A}, B(x));
@ -221,17 +221,17 @@ void add_basic_theory(environment & env) {
// eq_mp : Pi (a b: Bool) (H1 : a = b) (H2 : a), b :=
// Subst Bool (Fun x : Bool => x) a b H2 H1
env.add_definition(eq_mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, b),
Fun({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}},
Subst(Bool, Fun({x, Bool}, x), a, b, H2, H1)));
env.add_theorem(eq_mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, b),
Fun({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}},
Subst(Bool, Fun({x, Bool}, x), a, b, H2, H1)));
// truth : True := Refl Bool True
env.add_definition(truth_name, True, Refl(Bool, True));
env.add_theorem(truth_name, True, Refl(Bool, True));
// eqt_elim : Pi (a : Bool) (H : a = True), a := EqMP(True, a, Symm(Bool, a, True, H), Truth)
env.add_definition(eqt_elim_fn_name, Pi({{a, Bool}, {H, Eq(a, True)}}, a),
Fun({{a, Bool}, {H, Eq(a, True)}},
EqMP(True, a, Symm(Bool, a, True, H), Truth)));
env.add_theorem(eqt_elim_fn_name, Pi({{a, Bool}, {H, Eq(a, True)}}, a),
Fun({{a, Bool}, {H, Eq(a, True)}},
EqMP(True, a, Symm(Bool, a, True, H), Truth)));
// ext : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (H : Pi x : A, (f x) = (g x)), f = g
env.add_axiom(ext_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi({x, A}, Eq(f(x), g(x)))}}, Eq(f, g)));

17
src/kernel/environment.cpp
View file

@ -322,9 +322,7 @@ level environment::get_uvar(name const & n) const {
return m_imp->get_uvar(n);
}
void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
m_imp->check_no_children();
m_imp->check_name(n);
void environment::check_type(name const & n, expr const & t, expr const & v) {
infer_universe(t, *this);
expr v_t = infer_type(v, *this);
if (!is_convertible(t, v_t, *this)) {
@ -334,9 +332,22 @@ void environment::add_definition(name const & n, expr const & t, expr const & v,
<< "given type:\n" << v_t;
throw exception(buffer.str());
}
}
void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
m_imp->check_no_children();
m_imp->check_name(n);
check_type(n, t, v);
m_imp->add_definition(n, t, v, opaque);
}
void environment::add_theorem(name const & n, expr const & t, expr const & v) {
m_imp->check_no_children();
m_imp->check_name(n);
check_type(n, t, v);
m_imp->add_theorem(n, t, v);
}
void environment::add_definition(name const & n, expr const & v, bool opaque) {
m_imp->check_add(n);
expr v_t = infer_type(v, *this);

3
src/kernel/environment.h
View file

@ -18,6 +18,7 @@ namespace lean {
class environment {
struct imp;
std::shared_ptr<imp> m_imp;
void check_type(name const & n, expr const & t, expr const & v);
explicit environment(std::shared_ptr<imp> const & ptr);
explicit environment(imp * new_ptr);
public:
@ -154,6 +155,8 @@ public:
*/
void add_definition(name const & n, expr const & t, expr const & v, bool opaque = false);
void add_definition(char const * n, expr const & t, expr const & v, bool opaque = false) { add_definition(name(n), t, v, opaque); }
void add_theorem(name const & n, expr const & t, expr const & v);
void add_theorem(char const * n, expr const & t, expr const & v) { add_theorem(name(n), t, v); }
/**
\brief Add a new definition n : infer_type(v) := v.