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

Move Symm and Trans back to basic_thms.cpp

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

23
src/kernel/builtin.cpp
View file

@ -159,12 +159,7 @@ MK_CONSTANT(subst_fn, name("Subst"));
MK_CONSTANT(eta_fn, name("Eta"));
MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
// Basic theorems
MK_CONSTANT(symm_fn, name("Symm"));
MK_CONSTANT(trans_fn, name("Trans"));
MK_CONSTANT(trans_ext_fn, name("TransExt"));
void add_basic_theory(environment & env) {
void import_basiclib(environment & env) {
env.add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
env.add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
@ -173,7 +168,6 @@ void add_basic_theory(environment & env) {
expr f = Const("f");
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
expr x = Const("x");
expr y = Const("y");
expr A = Const("A");
@ -235,20 +229,5 @@ 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)));
// 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)}},
Subst(A, a, b, Fun({x, A}, Eq(x,a)), Refl(A, a), H)));
// Trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c
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, b, c, Fun({x, A}, Eq(a, x)), H1, H2)));
// TransExt: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c
env.add_theorem(trans_ext_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, b, c, Fun({x, B}, Eq(a, x)), H1, H2)));
}
}

15
src/kernel/builtin.h
View file

@ -148,22 +148,9 @@ 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); }
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); }
expr mk_trans_fn();
/** \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_trans_ext_fn();
/** \brief (Theorem) {A : Type u}, {B : Type u}, {a : A}, {b c : B}, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
inline expr TransExt(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_trans_ext_fn(), A, B, a, b, c, H1, H2}); }
class environment;
/** \brief Initialize the environment with basic builtin declarations and axioms */
void add_basic_theory(environment & env);
void import_basiclib(environment & env);
/**
\brief Helper macro for defining constants such as bool_type, int_type, int_add, etc.

21
src/library/basic_thms.cpp
View file

@ -30,6 +30,9 @@ MK_CONSTANT(conjunct2_fn, name("Conjunct2"));
MK_CONSTANT(disj1_fn, name("Disj1"));
MK_CONSTANT(disj2_fn, name("Disj2"));
MK_CONSTANT(disj_cases_fn, name("DisjCases"));
MK_CONSTANT(symm_fn, name("Symm"));
MK_CONSTANT(trans_fn, name("Trans"));
MK_CONSTANT(trans_ext_fn, name("TransExt"));
MK_CONSTANT(congr1_fn, name("Congr1"));
MK_CONSTANT(congr2_fn, name("Congr2"));
MK_CONSTANT(congr_fn, name("Congr"));
@ -44,7 +47,7 @@ MK_CONSTANT(domain_inj_fn, name("domain_inj"));
MK_CONSTANT(range_inj_fn, name("range_inj"));
#endif
void add_basic_thms(environment & env) {
void import_basicthms(environment & env) {
expr A = Const("A");
expr a = Const("a");
expr b = Const("b");
@ -194,6 +197,21 @@ void add_basic_thms(environment & env) {
MT(a, c, Discharge(a, c, H2), H))),
H))))));
// 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)}},
Subst(A, a, b, Fun({x, A}, Eq(x,a)), Refl(A, a), H)));
// Trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c
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, b, c, Fun({x, A}, Eq(a, x)), H1, H2)));
// TransExt: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c
env.add_theorem(trans_ext_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, b, c, Fun({x, B}, Eq(a, x)), H1, H2)));
// EqTElim : Pi (a : Bool) (H : a = True), a
env.add_theorem(eqt_elim_fn_name, Pi({{a, Bool}, {H, Eq(a, True)}}, a),
Fun({{a, Bool}, {H, Eq(a, True)}},
@ -227,7 +245,6 @@ void add_basic_thms(environment & env) {
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
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)}},

14
src/library/basic_thms.h
View file

@ -84,6 +84,18 @@ expr mk_disj_cases_fn();
/** \brief (Theorem) {a b c : Bool}, H1 : Or(a,b), H2 : a -> c, H3 : b -> c |- DisjCases(a, b, c, H1, H2, H3) : c */
inline expr DisjCases(expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2, expr const & H3) { return mk_app({mk_disj_cases_fn(), a, b, c, H1, H2, H3}); }
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); }
expr mk_trans_fn();
/** \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_trans_ext_fn();
/** \brief (Theorem) {A : Type u}, {B : Type u}, {a : A}, {b c : B}, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
inline expr TransExt(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_trans_ext_fn(), A, B, a, b, c, H1, H2}); }
expr mk_eqt_elim_fn();
/** \brief (Theorem) {a : Bool}, H : a = True |- EqTElim(a, H) : a */
inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); }
@ -109,7 +121,7 @@ expr mk_forall_elim_fn();
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);
void import_basicthms(environment & env);
#if 0
expr mk_ext_fn();

1
src/library/cast/castlib.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include "castlib.h"
#include "environment.h"
#include "abstract.h"
#include "basic_thms.h"
#include "builtin.h"
namespace lean {

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

@ -12,10 +12,10 @@ Author: Leonardo de Moura
namespace lean {
void import_all(environment & env) {
add_basic_theory(env);
add_basic_thms(env);
import_arithlibs(env);
import_basiclib(env);
import_basicthms(env);
import_castlib(env);
import_arithlibs(env);
}
environment mk_toplevel() {
environment r;