Refactor theorems. Add new theorems.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
345894d4ed
commit
58fef282c3
6 changed files with 357 additions and 251 deletions
|
|
@ -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})
|
||||
|
|
|
|||
209
src/kernel/basic_thms.cpp
Normal file
209
src/kernel/basic_thms.cpp
Normal file
|
|
@ -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
|
||||
}
|
||||
}
|
||||
100
src/kernel/basic_thms.h
Normal file
100
src/kernel/basic_thms.h
Normal file
|
|
@ -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
|
||||
}
|
||||
|
|
@ -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))));
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<expr> 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<expr> 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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue