From 58fef282c3dff353ee02fa5b4b4cea5fdc65e135 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Aug 2013 01:16:37 -0700 Subject: [PATCH] Refactor theorems. Add new theorems. Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 2 +- src/kernel/basic_thms.cpp | 209 ++++++++++++++++++++++++++++++++++++++ src/kernel/basic_thms.h | 100 ++++++++++++++++++ src/kernel/builtin.cpp | 200 +++++------------------------------- src/kernel/builtin.h | 95 ++++------------- src/kernel/toplevel.cpp | 2 + 6 files changed, 357 insertions(+), 251 deletions(-) create mode 100644 src/kernel/basic_thms.cpp create mode 100644 src/kernel/basic_thms.h diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 4c1488be3..91b9c164c 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,4 +1,4 @@ add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp - type_check.cpp context.cpp builtin.cpp toplevel.cpp) + type_check.cpp context.cpp builtin.cpp basic_thms.cpp toplevel.cpp) target_link_libraries(kernel ${EXTRA_LIBS}) diff --git a/src/kernel/basic_thms.cpp b/src/kernel/basic_thms.cpp new file mode 100644 index 000000000..7e46972a1 --- /dev/null +++ b/src/kernel/basic_thms.cpp @@ -0,0 +1,209 @@ +/* +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 "basic_thms.h" +#include "environment.h" +#include "abstract.h" +#include "type_check.h" + +namespace lean { + +MK_CONSTANT(true_neq_false, name("TrueNeFalse")); +MK_CONSTANT(truth, name("Truth")); +MK_CONSTANT(false_elim_fn, name("FalseElim")); +MK_CONSTANT(absurd_fn, name("Absurd")); +MK_CONSTANT(em_fn, name("EM")); +MK_CONSTANT(double_neg_fn, name("DoubleNeg")); +MK_CONSTANT(mt_fn, name("MT")); +MK_CONSTANT(contrapos_fn, name("Contrapos")); +MK_CONSTANT(conj_fn, name("Conj")); +MK_CONSTANT(symm_fn, name("Symm")); +MK_CONSTANT(trans_fn, name("Trans")); +MK_CONSTANT(xtrans_fn, name("xTrans")); +MK_CONSTANT(congr1_fn, name("Congr1")); +MK_CONSTANT(congr2_fn, name("Congr2")); +MK_CONSTANT(congr_fn, name("Congr")); +MK_CONSTANT(eq_mp_fn, name("EqMP")); +MK_CONSTANT(eqt_elim_fn, name("EqTElim")); +MK_CONSTANT(forall_elim_fn, name("ForallElim")); + +#if 0 +MK_CONSTANT(ext_fn, name("ext")); +MK_CONSTANT(foralli_fn, name("foralli")); +MK_CONSTANT(domain_inj_fn, name("domain_inj")); +MK_CONSTANT(range_inj_fn, name("range_inj")); +#endif + +void add_basic_thms(environment & env) { + expr A = Const("A"); + expr a = Const("a"); + expr b = Const("b"); + expr c = Const("c"); + expr H = Const("H"); + expr H1 = Const("H1"); + expr H2 = Const("H2"); + expr B = Const("B"); + expr f = Const("f"); + expr g = Const("g"); + expr h = Const("h"); + expr x = Const("x"); + expr y = Const("y"); + expr z = Const("z"); + expr P = Const("P"); + expr A1 = Const("A1"); + expr B1 = Const("B1"); + expr a1 = Const("a1"); + + expr A_pred = A >> Bool; + expr q_type = Pi({A, TypeU}, A_pred >> Bool); + expr piABx = Pi({x, A}, B(x)); + expr A_arrow_u = A >> TypeU; + + // True_neq_False : Not(True = False) + env.add_theorem(true_neq_false_name, Not(Eq(True, False)), Trivial); + + // Truth : True := Trivial + env.add_theorem(truth_name, True, Trivial); + + // FalseElim : Pi (a : Bool) (H : False), a + env.add_theorem(false_elim_fn_name, Pi({{a, Bool}, {H, False}}, a), + Fun({{a, Bool}, {H, False}}, Case(Fun({x, Bool}, x), Truth, H, a))); + + // Absurd : Pi (a : Bool) (H1 : a) (H2 : Not a), False + env.add_theorem(absurd_fn_name, Pi({{a, Bool}, {H1, a}, {H2, Not(a)}}, False), + Fun({{a, Bool}, {H1, a}, {H2, Not(a)}}, + MP(a, False, H2, H1))); + + // DoubleNeg : Pi (a : Bool), Eq(Not(Not(a)), a) + env.add_theorem(double_neg_fn_name, Pi({a, Bool}, Eq(Not(Not(a)), a)), + Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Not(Not(x)), x)), Trivial, Trivial, a))); + + // ModusTollens : Pi (a b : Bool) (H1 : a => b) (H2 : Not(b)), Not(a) + env.add_theorem(mt_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, Not(a)), + Fun({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, + Discharge(a, False, Fun({H, a}, + Absurd(b, MP(a, b, H1, H), H2))))); + + // Contrapositive : Pi (a b : Bool) (H : a => b), (Not(b) => Not(a)) + env.add_theorem(contrapos_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, Implies(Not(b), Not(a))), + Fun({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, + Discharge(Not(b), Not(a), Fun({H1, Not(b)}, MT(a, b, H, H1))))); + + // Conj : Pi (a b : Bool) (H1 : a) (H2 : b), And(a, b) + env.add_theorem(conj_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, And(a, b)), + Fun({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, + Discharge(Implies(a, Not(b)), False, Fun({H, Implies(a, Not(b))}, + Absurd(b, H2, MP(a, Not(b), H, H1)))))); + + // Iff : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = 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_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_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))); + + // xTrans: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c := + // Subst B (Fun x : B => a = x) b c H1 H2 + env.add_theorem(xtrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)), + Fun({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, + Subst(B, Fun({x, B}, Eq(a, x)), b, c, H1, H2))); + + // OrIntro1 : Pi (a b : Bool) (H : a), Or(a, b) + env.add_theorem(name("OrIntro1"), Pi({{a, Bool}, {b, Bool}, {H, a}}, Or(a, b)), + Fun({{a, Bool}, {b, Bool}, {H, a}}, + Discharge(Not(a), b, Fun({H1, Not(a)}, + FalseElim(b, Absurd(a, H, H1)))))); + + // EM : Pi (a : Bool), Or(a, Not(a)) + env.add_theorem(em_fn_name, Pi({a, Bool}, Or(a, Not(a))), + Fun({a, Bool}, Case(Fun({x, Bool}, Or(x, Not(x))), Trivial, Trivial, a))); + + env.add_theorem(name("OrIdempotent"), Pi({a, Bool}, Eq(Or(a, a), a)), + Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Or(x, x), x)), Trivial, Trivial, a))); + + env.add_theorem(name("OrComm"), Pi({{a, Bool}, {b, Bool}}, Eq(Or(a, b), Or(b, a))), + Fun({{a, Bool}, {b, Bool}}, + Case(Fun({x, Bool}, Eq(Or(x, b), Or(b, x))), + Case(Fun({y, Bool}, Eq(Or(True, y), Or(y, True))), Trivial, Trivial, b), + Case(Fun({y, Bool}, Eq(Or(False, y), Or(y, False))), Trivial, Trivial, b), + a))); + + env.add_theorem(name("OrAssoc"), Pi({{a, Bool}, {b, Bool}, {c, Bool}}, Eq(Or(Or(a, b), c), Or(a, Or(b, c)))), + Fun({{a, Bool}, {b, Bool}, {c, Bool}}, + Case(Fun({x, Bool}, Eq(Or(Or(x, b), c), Or(x, Or(b, c)))), + Case(Fun({y, Bool}, Eq(Or(Or(True, y), c), Or(True, Or(y, c)))), + Case(Fun({z, Bool}, Eq(Or(Or(True, True), z), Or(True, Or(True, z)))), Trivial, Trivial, c), + Case(Fun({z, Bool}, Eq(Or(Or(True, False), z), Or(True, Or(False, z)))), Trivial, Trivial, c), b), + Case(Fun({y, Bool}, Eq(Or(Or(False, y), c), Or(False, Or(y, c)))), + Case(Fun({z, Bool}, Eq(Or(Or(False, True), z), Or(False, Or(True, z)))), Trivial, Trivial, c), + Case(Fun({z, Bool}, Eq(Or(Or(False, False), z), Or(False, Or(False, z)))), Trivial, Trivial, c), b), a))); + + + // Congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi (x : A) B x) (a : A) (H : f = g), f a = g a := + // Subst piABx (Fun h : piABx => f a = h a) f g (Refl piABx f) H + env.add_theorem(congr1_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, Eq(f(a), g(a))), + Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, + Subst(piABx, Fun({h, piABx}, Eq(f(a), h(a))), f, g, Refl(piABx, f), H))); + + // Congr2 : Pi (A : Type u) (B : A -> Type u) (f : Pi (x : A) B x) (a b : A) (H : a = b), f a = f b := + // Subst A (Fun x : A => f a = f x) a b (Refl A a) H + env.add_theorem(congr2_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(f(a), f(b))), + Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {a, A}, {b, A}, {H, Eq(a, b)}}, + Subst(A, Fun({x, A}, Eq(f(a), f(x))), a, b, Refl(A, a), H))); + + // 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 := + // xTrans (B a) (B b) (f a) (f b) (g b) (congr2 A B f g b H1) (congr1 A B f a b H2) + env.add_theorem(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))), + Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, + xTrans(B(a), B(b), f(a), f(b), g(b), + Congr2(A, B, f, a, b, H2), Congr1(A, B, f, g, b, H1)))); + + // EqMP : Pi (a b: Bool) (H1 : a = b) (H2 : a), b := + // 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))); + + // EqTElim : Pi (a : Bool) (H : a = True), a := 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))); + + // EqTIntro : Pi (a : Bool) (H : a), a = True + // env.add_theorem(eqt_intro_fn_name, Pi({{a, Bool}, {H, a}}, Eq(a, True)), + // Fun({{a, Bool}, {H, a}} + + // ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a + env.add_theorem(forall_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)), + Fun({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, + EqTElim(P(a), Congr1(A, Fun({x, A}, Bool), P, Fun({x, A}, True), a, H)))); + +#if 0 + // STOPPED HERE + + // foralli : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P) + env.add_axiom(foralli_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P))); + + // 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))); + + + // domain_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), A = A1 + expr piA1B1x = Pi({x, A1}, B1(x)); + expr A1_arrow_u = A1 >> TypeU; + env.add_axiom(domain_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {H, Eq(piABx, piA1B1x)}}, Eq(A, A1))); + // range_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (a : A) (a1 : A1) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), (B a) = (B1 a1) + env.add_axiom(range_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {a, A}, {a1, A1}, {H, Eq(piABx, piA1B1x)}}, Eq(B(a), B1(a1)))); +#endif +} +} diff --git a/src/kernel/basic_thms.h b/src/kernel/basic_thms.h new file mode 100644 index 000000000..7ad991537 --- /dev/null +++ b/src/kernel/basic_thms.h @@ -0,0 +1,100 @@ +/* +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 "builtin.h" + +namespace lean { + +expr mk_absurd_fn(); +bool is_absurd_fn(expr const & e); +/** \brief (Theorem) a : Bool, H1 : a, H2 : Not(a) |- Absurd(a, H1, H2) : False */ +inline expr Absurd(expr const & a, expr const & H1, expr const & H2) { return mk_app(mk_absurd_fn(), a, H1, H2); } + +expr mk_false_elim_fn(); +bool is_false_elim_fn(expr const & e); +/** \brief (Theorem) a : Bool, H : False |- FalseElim(a, H) : a */ +inline expr FalseElim(expr const & a, expr const & H) { return mk_app(mk_false_elim_fn(), a, H); } + +expr mk_double_neg_fn(); +bool is_double_neg_fn(expr const & e); +/** \brief (Theorem) a : Bool |- DoubleNeg(a) : Neg(Neg(a)) = a */ +inline expr DoubleNeg(expr const & a) { return mk_app(mk_double_neg_fn(), a); } + +expr mk_mt_fn(); +bool is_mt_fn(expr const & e); +/** \brief (Theorem) a b : Bool, H1 : a => b, H2 : Not(b) |- MT(a, b, H1, H2) : Not(a) */ +inline expr MT(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_mt_fn(), a, b, H1, H2); } + +expr mk_contrapos_fn(); +bool is_contrapos_fn(expr const & e); +/** \brief (Theorem) a b : Bool, H : a => b |- Contrapos(a, b, H): Neg(b) => Neg(a) */ +inline expr Contrapos(expr const & a, expr const & b, expr const & H) { return mk_app(mk_contrapos_fn(), a, b, H); } + +expr mk_symm_fn(); +bool is_symm_fn(expr const & e); +/** \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); } + +expr mk_trans_fn(); +bool is_trans_fn(expr const & e); +/** \brief (Theorem) A : Type u, a b c : A, H1 : a = b, H2 : b = c |- Trans(A, a, b, c, H1, H2) : a = c */ +inline expr Trans(expr const & A, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_fn(), A, a, b, c, H1, H2}); } + +expr mk_xtrans_fn(); +bool is_xtrans_fn(expr const & e); +/** \brief (Theorem) A : Type u, B : Type u, a : A, b c : B, H1 : a = b, H2 : b = c |- xTrans(A, B, a, b, c, H1, H2) : a = c */ +inline expr xTrans(expr const & A, expr const & B, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_xtrans_fn(), A, B, a, b, c, H1, H2}); } + +expr mk_congr1_fn(); +bool is_congr1_fn(expr const & e); +/** \brief (Theorem) A : Type u, B : A -> Type u, f g : (Pi x : A, B x), a : A, H : f = g |- Congr2(A, B, f, g, a, H) : f a = g a */ +inline expr Congr1(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & H) { return mk_app({mk_congr1_fn(), A, B, f, g, a, H}); } + +expr mk_congr2_fn(); +bool is_congr2_fn(expr const & e); +/** \brief (Theorem) A : Type u, B : A -> Type u, f : (Pi x : A, B x), a b : A, H : a = b |- Congr1(A, B, f, a, b, H) : f a = f b */ +inline expr Congr2(expr const & A, expr const & B, expr const & f, expr const & a, expr const & b, expr const & H) { return mk_app({mk_congr2_fn(), A, B, f, a, b, H}); } + +expr mk_congr_fn(); +bool is_congr_fn(expr const & e); +/** \brief (Theorem) A : Type u, B : A -> Type u, f g : (Pi x : A, B x), a b : A, H1 : f = g, H2 : a = b |- Congr(A, B, f, g, a, b, H1, H2) : f a = g b */ +inline expr Congr(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app({mk_congr_fn(), A, B, f, g, a, b, H1, H2}); } + +expr mk_eq_mp_fn(); +bool is_eq_mp_fn(expr const & e); +/** \brief (Theorem) a : Bool, b : Bool, H1 : a = b, H2 : a |- EqMP(a, b, H1, H2) : b */ +inline expr EqMP(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_eq_mp_fn(), a, b, H1, H2); } + +expr mk_truth(); +bool is_truth(expr const & e); +/** \brief (Theorem) Truth : True */ +#define Truth mk_truth() + +expr mk_eqt_elim_fn(); +bool is_eqt_elim(expr const & e); +// \brief (Theorem) a : Bool, H : a = True |- EqT(a, H) : a +inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); } + +expr mk_forall_elim_fn(); +bool is_forall_elim_fn(expr const & e); +// \brief (Theorem) A : Type u, P : A -> Bool, H : (Forall A P), a : A |- Forallelim(A, P, H, a) : P a +inline expr ForallElim(expr const & A, expr const & P, expr const & H, expr const & a) { return mk_app(mk_forall_elim_fn(), A, P, H, a); } + +/** \brief Add basic theorems to Environment */ +void add_basic_thms(environment & env); + +#if 0 +expr mk_ext_fn(); +bool is_ext_fn(expr const & e); +expr mk_foralli_fn(); +bool is_foralli_fn(expr const & e); +expr mk_domain_inj_fn(); +bool is_domain_inj_fn(expr const & e); +expr mk_range_inj_fn(); +bool is_range_inj_fn(expr const & e); +#endif +} diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index f57e5947f..9bb024d0f 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -171,72 +171,40 @@ public: char const * implies_fn_value::g_kind = "implies"; MK_BUILTIN(implies_fn, implies_fn_value); - -MK_CONSTANT(mp_fn, name("mp")); -MK_CONSTANT(discharge_fn, name("discharge")); - -MK_CONSTANT(and_fn, name("and")); -MK_CONSTANT(or_fn, name("or")); -MK_CONSTANT(not_fn, name("not")); - +MK_CONSTANT(and_fn, name("and")); +MK_CONSTANT(or_fn, name("or")); +MK_CONSTANT(not_fn, name("not")); MK_CONSTANT(forall_fn, name("forall")); MK_CONSTANT(exists_fn, name("exists")); -MK_CONSTANT(true_neq_false, name("true_neq_false")); -MK_CONSTANT(refl_fn, name("refl")); -MK_CONSTANT(case_fn, name("case")); -MK_CONSTANT(false_elim_fn, name("false_elim")); -MK_CONSTANT(em_fn, name("em")); -MK_CONSTANT(double_neg_fn, name("double_neg")); -MK_CONSTANT(subst_fn, name("subst")); -MK_CONSTANT(eta_fn, name("eta")); -MK_CONSTANT(absurd_fn, name("absurd")); -MK_CONSTANT(symm_fn, name("symm")); -MK_CONSTANT(trans_fn, name("trans")); -MK_CONSTANT(xtrans_fn, name("xtrans")); -MK_CONSTANT(congr1_fn, name("congr1")); -MK_CONSTANT(congr2_fn, name("congr2")); -MK_CONSTANT(congr_fn, name("congr")); -MK_CONSTANT(eq_mp_fn, name("eq_mp")); -MK_CONSTANT(truth, name("truth")); -MK_CONSTANT(eqt_elim_fn, name("eqt_elim")); -MK_CONSTANT(ext_fn, name("ext")); -MK_CONSTANT(forall_elim_fn, name("forall_elim")); -MK_CONSTANT(foralli_fn, name("foralli")); -MK_CONSTANT(domain_inj_fn, name("domain_inj")); -MK_CONSTANT(range_inj_fn, name("range_inj")); +MK_CONSTANT(mp_fn, name("MP")); +MK_CONSTANT(discharge_fn, name("Discharge")); +MK_CONSTANT(refl_fn, name("Refl")); +MK_CONSTANT(case_fn, name("Case")); +MK_CONSTANT(subst_fn, name("Subst")); +MK_CONSTANT(eta_fn, name("Eta")); -expr Case(expr const & P, expr const & H1, expr const & H2, expr const & a) { return mk_app(mk_case_fn(), P, H1, H2, a); } 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); - expr p1 = Bool >> Bool; - expr p2 = Bool >> p1; - - expr A = Const("A"); - expr a = Const("a"); - expr b = Const("b"); - expr c = Const("c"); - expr H = Const("H"); - expr H1 = Const("H1"); - expr H2 = Const("H2"); - expr B = Const("B"); - expr f = Const("f"); - expr g = Const("g"); - expr h = Const("h"); - expr x = Const("x"); - expr y = Const("y"); - expr z = Const("z"); - expr P = Const("P"); - expr A1 = Const("A1"); - expr B1 = Const("B1"); - expr a1 = Const("a1"); - - expr A_pred = A >> Bool; - expr q_type = Pi({A, TypeU}, A_pred >> Bool); - expr piABx = Pi({x, A}, B(x)); + expr p1 = Bool >> Bool; + expr p2 = Bool >> p1; + expr f = Const("f"); + expr a = Const("a"); + expr b = Const("b"); + expr x = Const("x"); + expr y = Const("y"); + expr A = Const("A"); + expr A_pred = A >> Bool; + expr B = Const("B"); + expr q_type = Pi({A, TypeU}, A_pred >> Bool); + expr piABx = Pi({x, A}, B(x)); expr A_arrow_u = A >> TypeU; + expr P = Const("P"); + expr H = Const("H"); + expr H1 = Const("H1"); + expr H2 = Const("H2"); // not(x) = (x => False) env.add_definition(not_fn_name, p1, Fun({x, Bool}, Implies(x, False))); @@ -269,123 +237,5 @@ void add_basic_theory(environment & env) { // Eta : Pi (A : Type u) (B : A -> Type u), f : (Pi x : A, B x), (Fun x : A => f x) = f env.add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f))); - - // True_neq_False : Not(True = False) - env.add_theorem(true_neq_false_name, Not(Eq(True, False)), Trivial); - - // Truth : True := Trivial - env.add_theorem(truth_name, True, Trivial); - - // False_elim : Pi (a : Bool) (H : False), a - env.add_theorem(false_elim_fn_name, Pi({{a, Bool}, {H, False}}, a), - Fun({{a, Bool}, {H, False}}, Case(Fun({x, Bool}, x), Truth, H, a))); - - // Absurd : Pi (a : Bool) (H1 : a) (H2 : Not a), False - env.add_theorem(absurd_fn_name, Pi({{a, Bool}, {H1, a}, {H2, Not(a)}}, False), - Fun({{a, Bool}, {H1, a}, {H2, Not(a)}}, - MP(a, False, H2, H1))); - - // OrIntro : Pi (a b : Bool) (H : a), Or(a, b) - env.add_theorem(name("or_intro1"), Pi({{a, Bool}, {b, Bool}, {H, a}}, Or(a, b)), - Fun({{a, Bool}, {b, Bool}, {H, a}}, - Discharge(Not(a), b, Fun({H1, Not(a)}, - FalseElim(b, Absurd(a, H, H1)))))); - - // EM : Pi (a : Bool), Or(a, Not(a)) - env.add_theorem(em_fn_name, Pi({a, Bool}, Or(a, Not(a))), - Fun({a, Bool}, Case(Fun({x, Bool}, Or(x, Not(x))), Trivial, Trivial, a))); - - // DoubleNeg : Pi (a : Bool), Eq(Not(Not(a)), a) - env.add_theorem(double_neg_fn_name, Pi({a, Bool}, Eq(Not(Not(a)), a)), - Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Not(Not(x)), x)), Trivial, Trivial, a))); - - env.add_theorem(name("or_idempotent"), Pi({a, Bool}, Eq(Or(a, a), a)), - Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Or(x, x), x)), Trivial, Trivial, a))); - - env.add_theorem(name("or_comm"), Pi({{a, Bool}, {b, Bool}}, Eq(Or(a, b), Or(b, a))), - Fun({{a, Bool}, {b, Bool}}, - Case(Fun({x, Bool}, Eq(Or(x, b), Or(b, x))), - Case(Fun({y, Bool}, Eq(Or(True, y), Or(y, True))), Trivial, Trivial, b), - Case(Fun({y, Bool}, Eq(Or(False, y), Or(y, False))), Trivial, Trivial, b), - a))); - - env.add_theorem(name("or_assoc"), Pi({{a, Bool}, {b, Bool}, {c, Bool}}, Eq(Or(Or(a, b), c), Or(a, Or(b, c)))), - Fun({{a, Bool}, {b, Bool}, {c, Bool}}, - Case(Fun({x, Bool}, Eq(Or(Or(x, b), c), Or(x, Or(b, c)))), - Case(Fun({y, Bool}, Eq(Or(Or(True, y), c), Or(True, Or(y, c)))), - Case(Fun({z, Bool}, Eq(Or(Or(True, True), z), Or(True, Or(True, z)))), Trivial, Trivial, c), - Case(Fun({z, Bool}, Eq(Or(Or(True, False), z), Or(True, Or(False, z)))), Trivial, Trivial, c), b), - Case(Fun({y, Bool}, Eq(Or(Or(False, y), c), Or(False, Or(y, c)))), - Case(Fun({z, Bool}, Eq(Or(Or(False, True), z), Or(False, Or(True, z)))), Trivial, Trivial, c), - Case(Fun({z, Bool}, Eq(Or(Or(False, False), z), Or(False, Or(False, z)))), Trivial, Trivial, c), b), a))); - - // 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_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_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))); - - // xTrans: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c := - // Subst B (Fun x : B => a = x) b c H1 H2 - env.add_theorem(xtrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)), - Fun({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, - Subst(B, Fun({x, B}, Eq(a, x)), b, c, H1, H2))); - - // Congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi (x : A) B x) (a : A) (H : f = g), f a = g a := - // Subst piABx (Fun h : piABx => f a = h a) f g (Refl piABx f) H - env.add_theorem(congr1_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, Eq(f(a), g(a))), - Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, - Subst(piABx, Fun({h, piABx}, Eq(f(a), h(a))), f, g, Refl(piABx, f), H))); - - // Congr2 : Pi (A : Type u) (B : A -> Type u) (f : Pi (x : A) B x) (a b : A) (H : a = b), f a = f b := - // Subst A (Fun x : A => f a = f x) a b (Refl A a) H - env.add_theorem(congr2_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(f(a), f(b))), - Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {a, A}, {b, A}, {H, Eq(a, b)}}, - Subst(A, Fun({x, A}, Eq(f(a), f(x))), a, b, Refl(A, a), H))); - - // 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 := - // xTrans (B a) (B b) (f a) (f b) (g b) (congr2 A B f g b H1) (congr1 A B f a b H2) - env.add_theorem(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))), - Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, - xTrans(B(a), B(b), f(a), f(b), g(b), - Congr2(A, B, f, a, b, H2), Congr1(A, B, f, g, b, H1)))); - - // EqMP : Pi (a b: Bool) (H1 : a = b) (H2 : a), b := - // 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))); - - // EqTElim : Pi (a : Bool) (H : a = True), a := 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))); - - // ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a - env.add_theorem(forall_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)), - Fun({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, - EqTElim(P(a), Congr1(A, Fun({x, A}, Bool), P, Fun({x, A}, True), a, H)))); - - // STOPPED HERE - - // foralli : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P) - env.add_axiom(foralli_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P))); - - // 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))); - - - // domain_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), A = A1 - expr piA1B1x = Pi({x, A1}, B1(x)); - expr A1_arrow_u = A1 >> TypeU; - env.add_axiom(domain_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {H, Eq(piABx, piA1B1x)}}, Eq(A, A1))); - // range_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (a : A) (a1 : A1) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), (B a) = (B1 a1) - env.add_axiom(range_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {a, A}, {a1, A1}, {H, Eq(piABx, piA1B1x)}}, Eq(B(a), B1(a1)))); } } diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index 6aec38052..7507f4245 100644 --- a/src/kernel/builtin.h +++ b/src/kernel/builtin.h @@ -57,27 +57,30 @@ inline expr If(expr const & A, expr const & c, expr const & t, expr const & e) { inline expr mk_bool_if(expr const & c, expr const & t, expr const & e) { return mk_if(mk_bool_type(), c, t, e); } inline expr bIf(expr const & c, expr const & t, expr const & e) { return mk_bool_if(c, t, e); } +/** \brief Return the Lean Implies operator */ expr mk_implies_fn(); +/** \brief Return true iff \c e is the Lean implies operator */ bool is_implies_fn(expr const & e); +/** \brief Return the term (e1 => e2) */ inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app(mk_implies_fn(), e1, e2); } inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); } -/** \brief Return the Lean and operator */ +/** \brief Return the Lean And operator */ expr mk_and_fn(); /** \brief Return true iff \c e is the Lean and operator. */ bool is_and_fn(expr const & e); -/** \brief Return (and e1 e2) */ +/** \brief Return (e1 and e2) */ inline expr mk_and(expr const & e1, expr const & e2) { return mk_app(mk_and_fn(), e1, e2); } inline expr mk_and(unsigned num_args, expr const * args) { return mk_bin_op(mk_and_fn(), True, num_args, args); } inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); } inline expr And(std::initializer_list const & l) { return mk_and(l.size(), l.begin()); } -/** \brief Return the Lean or operator */ +/** \brief Return the Lean Or operator */ expr mk_or_fn(); bool is_or_fn(expr const & e); -/** \brief Return (or e1 e2) */ +/** \brief Return (e1 Or e2) */ inline expr mk_or(expr const & e1, expr const & e2) { return mk_app(mk_or_fn(), e1, e2); } inline expr mk_or(unsigned num_args, expr const * args) { return mk_bin_op(mk_or_fn(), False, num_args, args); } inline expr Or(expr const & e1, expr const & e2) { return mk_or(e1, e2); } @@ -87,7 +90,7 @@ inline expr Or(std::initializer_list const & l) { return mk_or(l.size(), l expr mk_not_fn(); bool is_not_fn(expr const & e); -/** \brief Return (not e) */ +/** \brief Return (Not e) */ inline expr mk_not(expr const & e) { return mk_app(mk_not_fn(), e); } inline expr Not(expr const & e) { return mk_not(e); } @@ -95,7 +98,7 @@ inline expr Not(expr const & e) { return mk_not(e); } expr mk_forall_fn(); /** \brief Return true iff \c e is the Lean forall operator */ bool is_forall_fn(expr const & e); -/** \brief Return the term (forall A P), where A is a type and P : A -> bool */ +/** \brief Return the term (Forall A P), where A is a type and P : A -> bool */ inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); } inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); } @@ -107,101 +110,43 @@ bool is_exists_fn(expr const & e); inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); } inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); } +/** \brief Modus Ponens axiom */ expr mk_mp_fn(); bool is_mp_fn(const expr & e); /** \brief (Axiom) a : Bool, b : Bool, H1 : a => b, H2 : a |- MP(a, b, H1, H2) : b */ inline expr MP(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_mp_fn(), a, b, H1, H2); } +/** \brief Discharge axiom */ expr mk_discharge_fn(); bool is_discharge_fn(const expr & e); /** \brief (Axiom) a : Bool, b : Bool, H : a -> b |- Discharge(a, b, H) : a => b */ inline expr Discharge(expr const & a, expr const & b, expr const & H) { return mk_app(mk_discharge_fn(), a, b, H); } +/** \brief Reflexivity axiom */ expr mk_refl_fn(); bool is_refl_fn(expr const & e); /** \brief (Axiom) A : Type u, a : A |- Refl(A, a) : a = a */ inline expr Refl(expr const & A, expr const & a) { return mk_app(mk_refl_fn(), A, a); } #define Trivial Refl(Bool, True) +/** \brief Case analysis axiom */ +expr mk_case_fn(); +bool is_case_fn(expr const & e); +/** \brief (Axiom) P : Bool -> Bool, H1 : P True, H2 : P False, a : Bool |- Case(P, H1, H2, a) : P a */ +inline expr Case(expr const & P, expr const & H1, expr const & H2, expr const & a) { return mk_app(mk_case_fn(), P, H1, H2, a); } + +/** \brief Substitution axiom */ expr mk_subst_fn(); bool is_subst_fn(expr const & e); /** \brief (Axiom) A : Type u, P : A -> Bool, a b : A, H1 : P a, H2 : a = b |- Subst(A, P, a, b, H1, H2) : P b */ inline expr Subst(expr const & A, expr const & P, expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app({mk_subst_fn(), A, P, a, b, H1, H2}); } +/** \brief Eta conversion axiom */ expr mk_eta_fn(); bool is_eta_fn(expr const & e); /** \brief (Axiom) A : Type u, B : A -> Type u, f : (Pi x : A, B x) |- Eta(A, B, f) : ((Fun x : A => f x) = f) */ inline expr Eta(expr const & A, expr const & B, expr const & f) { return mk_app(mk_eta_fn(), A, B, f); } -expr mk_absurd_fn(); -bool is_absurd_fn(expr const & e); -/** \brief (Theorem) a : Bool, H1 : a, H2 : Not(a) |- Absurd(a, H1, H2) : False */ -inline expr Absurd(expr const & a, expr const & H1, expr const & H2) { return mk_app(mk_absurd_fn(), a, H1, H2); } - -expr mk_false_elim_fn(); -bool is_false_elim_fn(expr const & e); -/** \brief (Theorem) a : Bool, H : False |- FalseElim(a, H) : a */ -inline expr FalseElim(expr const & a, expr const & H) { return mk_app(mk_false_elim_fn(), a, H); } - -expr mk_symm_fn(); -bool is_symm_fn(expr const & e); -/** \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); } - -expr mk_trans_fn(); -bool is_trans_fn(expr const & e); -/** \brief (Theorem) A : Type u, a b c : A, H1 : a = b, H2 : b = c |- Trans(A, a, b, c, H1, H2) : a = c */ -inline expr Trans(expr const & A, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_fn(), A, a, b, c, H1, H2}); } - -expr mk_xtrans_fn(); -bool is_xtrans_fn(expr const & e); -/** \brief (Theorem) A : Type u, B : Type u, a : A, b c : B, H1 : a = b, H2 : b = c |- xTrans(A, B, a, b, c, H1, H2) : a = c */ -inline expr xTrans(expr const & A, expr const & B, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_xtrans_fn(), A, B, a, b, c, H1, H2}); } - -expr mk_congr1_fn(); -bool is_congr1_fn(expr const & e); -/** \brief (Theorem) A : Type u, B : A -> Type u, f g : (Pi x : A, B x), a : A, H : f = g |- Congr2(A, B, f, g, a, H) : f a = g a */ -inline expr Congr1(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & H) { return mk_app({mk_congr1_fn(), A, B, f, g, a, H}); } - -expr mk_congr2_fn(); -bool is_congr2_fn(expr const & e); -/** \brief (Theorem) A : Type u, B : A -> Type u, f : (Pi x : A, B x), a b : A, H : a = b |- Congr1(A, B, f, a, b, H) : f a = f b */ -inline expr Congr2(expr const & A, expr const & B, expr const & f, expr const & a, expr const & b, expr const & H) { return mk_app({mk_congr2_fn(), A, B, f, a, b, H}); } - -expr mk_congr_fn(); -bool is_congr_fn(expr const & e); -/** \brief (Theorem) A : Type u, B : A -> Type u, f g : (Pi x : A, B x), a b : A, H1 : f = g, H2 : a = b |- Congr(A, B, f, g, a, b, H1, H2) : f a = g b */ -inline expr Congr(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app({mk_congr_fn(), A, B, f, g, a, b, H1, H2}); } - -expr mk_eq_mp_fn(); -bool is_eq_mp_fn(expr const & e); -/** \brief (Theorem) a : Bool, b : Bool, H1 : a = b, H2 : a |- EqMP(a, b, H1, H2) : b */ -inline expr EqMP(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_eq_mp_fn(), a, b, H1, H2); } - -expr mk_truth(); -bool is_truth(expr const & e); -/** \brief (Theorem) Truth : True */ -#define Truth mk_truth() - -expr mk_eqt_elim_fn(); -bool is_eqt_elim(expr const & e); -// \brief (Theorem) a : Bool, H : a = True |- EqT(a, H) : a -inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); } - -expr mk_forall_elim_fn(); -bool is_forall_elim_fn(expr const & e); -// \brief (Theorem) A : Type u, P : A -> Bool, H : (Forall A P), a : A |- Forallelim(A, P, H, a) : P a -inline expr ForallElim(expr const & A, expr const & P, expr const & H, expr const & a) { return mk_app(mk_forall_elim_fn(), A, P, H, a); } - -expr mk_ext_fn(); -bool is_ext_fn(expr const & e); -expr mk_foralli_fn(); -bool is_foralli_fn(expr const & e); -expr mk_domain_inj_fn(); -bool is_domain_inj_fn(expr const & e); -expr mk_range_inj_fn(); -bool is_range_inj_fn(expr const & e); - class environment; /** \brief Initialize the environment with basic builtin declarations and axioms */ void add_basic_theory(environment & env); diff --git a/src/kernel/toplevel.cpp b/src/kernel/toplevel.cpp index d4ea73c28..653b259e3 100644 --- a/src/kernel/toplevel.cpp +++ b/src/kernel/toplevel.cpp @@ -6,12 +6,14 @@ Author: Leonardo de Moura */ #include "toplevel.h" #include "builtin.h" +#include "basic_thms.h" #include "arith.h" namespace lean { environment mk_toplevel() { environment r; add_basic_theory(r); + add_basic_thms(r); add_int_theory(r); return r; }