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

Add ImpAntisym axiom

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-07 08:29:20 -07:00
parent 722e2b0ed4
commit 2d27573e0c
2 changed files with 17 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/kernel/builtin.cpp
View file

@ -177,13 +177,14 @@ MK_CONSTANT(not_fn, name("not"));
MK_CONSTANT(forall_fn, name("forall")); MK_CONSTANT(forall_fn, name("forall"));
MK_CONSTANT(exists_fn, name("exists")); MK_CONSTANT(exists_fn, name("exists"));
MK_CONSTANT(mp_fn, name("MP")); // Axioms
MK_CONSTANT(discharge_fn, name("Discharge")); MK_CONSTANT(mp_fn, name("MP"));
MK_CONSTANT(refl_fn, name("Refl")); MK_CONSTANT(discharge_fn, name("Discharge"));
MK_CONSTANT(case_fn, name("Case")); MK_CONSTANT(refl_fn, name("Refl"));
MK_CONSTANT(subst_fn, name("Subst")); MK_CONSTANT(case_fn, name("Case"));
MK_CONSTANT(eta_fn, name("Eta")); MK_CONSTANT(subst_fn, name("Subst"));
MK_CONSTANT(eta_fn, name("Eta"));
MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
void add_basic_theory(environment & env) { void add_basic_theory(environment & env) {
env.define_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION); env.define_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
@ -237,5 +238,8 @@ 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 // 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))); env.add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f)));
// 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)));
} }
} }

6
src/kernel/builtin.h
View file

@ -147,6 +147,12 @@ 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) */ /** \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); } inline expr Eta(expr const & A, expr const & B, expr const & f) { return mk_app(mk_eta_fn(), A, B, f); }
/** \brief Implies Anti-symmetry */
expr mk_imp_antisym_fn();
bool is_imp_antisym_fn(expr const & e);
/** \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); }
class environment; class environment;
/** \brief Initialize the environment with basic builtin declarations and axioms */ /** \brief Initialize the environment with basic builtin declarations and axioms */
void add_basic_theory(environment & env); void add_basic_theory(environment & env);