From 33d2dd2d8bda9147e31688dc8faf6ea188170a4f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 6 Aug 2013 02:03:22 -0700 Subject: [PATCH] Add subst proof rule. Define symm and trans using subst. Signed-off-by: Leonardo de Moura --- src/kernel/builtin.cpp | 19 +++++++++++++++---- src/kernel/builtin.h | 2 ++ src/kernel/environment.cpp | 12 +++++++++++- src/kernel/environment.h | 10 +++++++++- src/kernel/expr.h | 6 ++++++ 5 files changed, 43 insertions(+), 6 deletions(-) diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index e5e999825d..ab29578c1f 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -148,6 +148,7 @@ MK_CONSTANT(forall_fn, name("forall")); MK_CONSTANT(exists_fn, name("exists")); MK_CONSTANT(refl_fn, name("refl")); +MK_CONSTANT(subst_fn, name("subst")); MK_CONSTANT(symm_fn, name("symm")); MK_CONSTANT(trans_fn, name("trans")); MK_CONSTANT(congr_fn, name("congr")); @@ -157,6 +158,8 @@ MK_CONSTANT(foralli_fn, name("foralli")); MK_CONSTANT(domain_inj_fn, name("domain_inj")); MK_CONSTANT(range_inj_fn, name("range_inj")); + + void add_basic_theory(environment & env) { env.define_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION); env.define_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION); @@ -195,10 +198,18 @@ void add_basic_theory(environment & env) { // refl : Pi (A : Type u) (a : A), a = a env.add_axiom(refl_fn_name, Fun(A, u_type(), Fun(a, A, eq(a, a)))); - // symm : Pi (A : Type u) (a b : A) (H : a = b), b = a - env.add_axiom(symm_fn_name, Fun(A, u_type(), Fun(a, A, Fun(b, A, Fun(H, eq(a, b), eq(b, a)))))); - // trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c - env.add_axiom(trans_fn_name, Fun(A, u_type(), Fun(a, A, Fun(b, A, Fun(c, A, Fun(H1, eq(a, b), Fun(H2, eq(b, c), eq(a, c)))))))); + // subst : Pi (A : Type u) (P : A -> bool) (a b : A) (H1 : P a) (H2 : a = b), P b + env.add_axiom(subst_fn_name, Fun(A, u_type(), Fun(P, A_pred, Fun(a, A, Fun(b, A, Fun(H1, P(a), Fun(H2, eq(a, b), P(b)))))))); + // 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, Fun(A, u_type(), Fun(a, A, Fun(b, A, Fun(H, eq(a, b), eq(b, a))))), + fun(A, u_type(), fun(a, A, fun(b, A, fun(H, eq(a, b), app(subst_fn(), A, fun(x, A, eq(x,a)), a, b, app(refl_fn(), 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, Fun(A, u_type(), Fun(a, A, Fun(b, A, Fun(c, A, Fun(H1, eq(a, b), Fun(H2, eq(b, c), eq(a, c))))))), + fun(A, u_type(), fun(a, A, fun(b, A, fun(c, A, fun(H1, eq(a, b), fun(H2, eq(b, c), app(subst_fn(), 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 = Fun(x, A, B(x)); expr A_arrow_u = arrow(A, u_type()); diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index cd6ac37e2a..ba123032e5 100644 --- a/src/kernel/builtin.h +++ b/src/kernel/builtin.h @@ -92,6 +92,8 @@ inline expr mk_exists(expr const & A, expr const & P) { return app(exists_fn(), expr refl_fn(); bool is_refl_fn(expr const & e); +expr subst_fn(); +bool is_subst_fn(expr const & e); expr symm_fn(); bool is_symm_fn(expr const & e); expr trans_fn(); diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 54ebdf8540..c0d547cc80 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -28,8 +28,13 @@ environment::definition::definition(name const & n, expr const & t, expr const & environment::definition::~definition() { } +void environment::definition::display_header(std::ostream & out) const { + out << "Definition"; +} + void environment::definition::display(std::ostream & out) const { - out << "Definition " << m_name << " : " << m_type << " := " << m_value << "\n"; + display_header(out); + out << " " << m_name << " : " << m_type << " := " << m_value << "\n"; } environment::fact::fact(name const & n, expr const & t): @@ -199,6 +204,11 @@ struct environment::imp { m_object_dictionary.insert(std::make_pair(n, m_objects.back())); } + void add_theorem(name const & n, expr const & t, expr const & v) { + m_objects.push_back(new theorem(n, t, v)); + m_object_dictionary.insert(std::make_pair(n, m_objects.back())); + } + void add_axiom(name const & n, expr const & t) { m_objects.push_back(new axiom(n, t)); m_object_dictionary.insert(std::make_pair(n, m_objects.back())); diff --git a/src/kernel/environment.h b/src/kernel/environment.h index cd6218a99d..c37366c002 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -69,7 +69,7 @@ public: */ environment parent() const; - enum class object_kind { Definition, Var, Axiom }; + enum class object_kind { Definition, Theorem, Var, Axiom }; /** \brief Base class for environment objects @@ -92,6 +92,7 @@ public: expr m_type; expr m_value; bool m_opaque; + virtual void display_header(std::ostream & out) const; public: definition(name const & n, expr const & t, expr const & v, bool opaque); virtual ~definition(); @@ -103,6 +104,13 @@ public: virtual void display(std::ostream & out) const; }; + class theorem : public definition { + virtual void display_header(std::ostream & out) const { out << "Theorem"; } + public: + theorem(name const & n, expr const & t, expr const & v):definition(n, t, v, true) {} + virtual object_kind kind() const { return object_kind::Theorem; } + }; + class fact : public object { protected: name m_name; diff --git a/src/kernel/expr.h b/src/kernel/expr.h index e5a7a38205..3ba482da73 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -260,6 +260,12 @@ inline expr app(expr const & e1, expr const & e2) { expr args[2] = {e1, e2}; ret inline expr app(expr const & e1, expr const & e2, expr const & e3) { expr args[3] = {e1, e2, e3}; return app(3, args); } inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { expr args[4] = {e1, e2, e3, e4}; return app(4, args); } inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { expr args[5] = {e1, e2, e3, e4, e5}; return app(5, args); } +inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { + expr args[6] = {e1, e2, e3, e4, e5, e6}; return app(6, args); +} +inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { + expr args[7] = {e1, e2, e3, e4, e5, e6, e7}; return app(7, args); +} inline expr eq(expr const & l, expr const & r) { return expr(new expr_eq(l, r)); } inline expr lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); } inline expr lambda(char const * n, expr const & t, expr const & e) { return lambda(name(n), t, e); }