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

feat(kernel): add abstraction (aka function extensionality) axiom

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-01 13:56:38 -08:00
parent 09f98ecddc
commit 1ec8f9d536
5 changed files with 24 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/notation.cpp
View file

@ -92,6 +92,7 @@ void init_builtin_notation(frontend & f) {
f.mark_implicit_arguments("SubstP", {true, true, true, false, false, false});
f.mark_implicit_arguments(mk_trans_ext_fn(), {true, true, true, true, true, true, false, false});
f.mark_implicit_arguments(mk_eta_fn(), {true, true, false});
f.mark_implicit_arguments(mk_abst_fn(), {true, true, true, true, false});
f.mark_implicit_arguments(mk_imp_antisym_fn(), {true, true, false, false});
f.mark_implicit_arguments(mk_dom_inj_fn(), {true, true, true, true, false});
f.mark_implicit_arguments(mk_ran_inj_fn(), {true, true, true, true, false, false});

5
src/kernel/builtin.cpp
View file

@ -203,6 +203,7 @@ MK_CONSTANT(trans_ext_fn, name("TransExt"));
MK_CONSTANT(subst_fn, name("Subst"));
MK_CONSTANT(eta_fn, name("Eta"));
MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
MK_CONSTANT(abst_fn, name("Abst"));
void import_basic(environment & env) {
if (!env.mark_builtin_imported("basic"))
@ -213,6 +214,7 @@ void import_basic(environment & env) {
expr p1 = Bool >> Bool;
expr p2 = Bool >> p1;
expr f = Const("f");
expr g = Const("g");
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
@ -281,5 +283,8 @@ void import_basic(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)));
// Abst : 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(abst_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)));
}
}

5
src/kernel/builtin.h
View file

@ -181,6 +181,11 @@ 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); }
/** \brief Abstraction axiom */
expr mk_abst_fn();
/** \brief (Axiom) {A : Type u} {B : A -> Type u}, f g : {Pi x : A, B x}, H : (Pi x : A, (f x) = (g x)) |- Abst(A, B, f, g, H) : f = g */
inline expr Abst(expr const & A, expr const & B, expr const & f, expr const & g, expr const & H) { return mk_app({mk_abst_fn(), A, B, f, g, H}); }
class environment;
/** \brief Initialize the environment with basic builtin declarations and axioms */
void import_basic(environment & env);

5
tests/lean/abst.lean Normal file
View file

@ -0,0 +1,5 @@
Axiom PlusComm(a b : Int) : a + b == b + a.
Variable a : Int.
Check (Abst (fun x : Int, (PlusComm a x))).
Set pp::implicit true.
Check (Abst (fun x : Int, (PlusComm a x))).

8
tests/lean/abst.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
Set: pp::colors
Set: pp::unicode
Assumed: PlusComm
Assumed: a
Abst (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a)
Set: lean::pp::implicit
Abst::explicit ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) :
(λ x : ℤ, a + x) == (λ x : ℤ, x + a)