From 3fbc50627157db577ddeac75e5b6d8a89e523205 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 7 Aug 2013 21:16:04 -0700
Subject: [PATCH] Rename Truth to Trivial, and delete Trivial macro

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/basic_thms.cpp | 14 +++++++-------
 src/kernel/basic_thms.h   |  7 +++----
 src/kernel/builtin.h      |  1 -
 3 files changed, 10 insertions(+), 12 deletions(-)

diff --git a/src/kernel/basic_thms.cpp b/src/kernel/basic_thms.cpp
index 7179e2dd95..eae61cc741 100644
--- a/src/kernel/basic_thms.cpp
+++ b/src/kernel/basic_thms.cpp
@@ -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)))));
 
 
diff --git a/src/kernel/basic_thms.h b/src/kernel/basic_thms.h
index df67741d1e..ee2d327710 100644
--- a/src/kernel/basic_thms.h
+++ b/src/kernel/basic_thms.h
@@ -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); }
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 82c5fd0c3d..2820514bf4 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -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();