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

Rename Truth to Trivial, and delete Trivial macro

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-07 21:16:04 -07:00
parent bede62e2f7
commit 3fbc506271
3 changed files with 10 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/kernel/basic_thms.cpp
View file

@ -11,8 +11,8 @@ Author: Leonardo de Moura
namespace lean {
MK_CONSTANT(trivial, name("Trivial"));
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"));
@ -73,19 +73,19 @@ void add_basic_thms(environment & env) {
expr piABx = Pi({x, A}, B(x));
expr A_arrow_u = A >> TypeU;
// Trivial : True
env.add_theorem(trivial_name, True, Refl(Bool, True));
// True_neq_False : Not(True = False)
env.add_theorem(true_neq_false_name, Not(Eq(True, False)), Trivial);
// Truth : True
env.add_theorem(truth_name, True, Trivial);
// 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)));
// 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)));
Fun({{a, Bool}, {H, False}}, Case(Fun({x, Bool}, x), Trivial, 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),
@ -215,13 +215,13 @@ void add_basic_thms(environment & env) {
// 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)}},
EqMP(True, a, Symm(Bool, a, True, H), Truth)));
EqMP(True, a, Symm(Bool, a, True, H), Trivial)));
// 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}},
ImpAntisym(a, True,
Discharge(a, True, Fun({H1, a}, Truth)),
Discharge(a, True, Fun({H1, a}, Trivial)),
Discharge(True, a, Fun({H2, True}, H)))));

7
src/kernel/basic_thms.h
View file

@ -8,15 +8,14 @@ Author: Leonardo de Moura
#include "builtin.h"
namespace lean {
expr mk_trivial();
/** \brief (Theorem) Trivial : True */
#define Trivial mk_trivial()
expr mk_true_ne_false();
/** \brief (Theorem) TrueNeFalse : Not(True = False) */
#define TrueNeFalse mk_true_ne_false();
expr mk_truth();
/** \brief (Theorem) Truth : True */
#define Truth mk_truth()
expr mk_em_fn();
/** \brief (Theorem) a : Bool |- EM(a) : Or(a, Not(a)) */
inline expr EM(expr const & a) { return mk_app(mk_em_fn(), a); }

1
src/kernel/builtin.h
View file

@ -106,7 +106,6 @@ inline expr Discharge(expr const & a, expr const & b, expr const & H) { return m
expr mk_refl_fn();
/** \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();