From 3ff3eb6444bd7309653973c93f006593746f518c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 6 Aug 2013 14:47:13 -0700 Subject: [PATCH] Add Eta axiom Signed-off-by: Leonardo de Moura --- src/kernel/builtin.cpp | 14 +++++++++----- src/kernel/builtin.h | 5 +++++ 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 6a116e8ba..8660a3737 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -149,6 +149,7 @@ MK_CONSTANT(exists_fn, name("exists")); MK_CONSTANT(refl_fn, name("refl")); MK_CONSTANT(subst_fn, name("subst")); +MK_CONSTANT(eta_fn, name("eta")); MK_CONSTANT(symm_fn, name("symm")); MK_CONSTANT(trans_fn, name("trans")); MK_CONSTANT(xtrans_fn, name("xtrans")); @@ -188,6 +189,11 @@ void add_basic_theory(environment & env) { 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; + // and(x, y) = (if bool x y false) env.add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True))); // or(x, y) = (if bool x true y) @@ -196,8 +202,6 @@ void add_basic_theory(environment & env) { env.add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True))); // forall : Pi (A : Type u), (A -> Bool) -> Bool - expr A_pred = A >> Bool; - expr q_type = Pi({A, TypeU}, A_pred >> Bool); env.add_var(forall_fn_name, q_type); env.add_definition(exists_fn_name, q_type, Fun({{A,TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x))))))); @@ -207,6 +211,9 @@ void add_basic_theory(environment & env) { // 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, Pi({{A, TypeU}, {P, A_pred}, {a, A}, {b, A}, {H1, P(a)}, {H2, Eq(a,b)}}, P(b))); + // 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))); + // 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)), @@ -219,15 +226,12 @@ void add_basic_theory(environment & env) { 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))); - expr piABx = Pi({x, A}, B(x)); - expr A_arrow_u = A >> TypeU; // 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))), diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index d706a82ca..b7e887c84 100644 --- a/src/kernel/builtin.h +++ b/src/kernel/builtin.h @@ -113,6 +113,11 @@ 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}); } +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_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 */