Add => as a primitive. Define Not, And and Or using =>. Add MP and Discharge as axioms.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/builtin.cpp

@@ -124,10 +124,9 @@ public:
             else
                 r = args[4]; // if A false a b --> b
             return true;
-        // TODO: uncomment the following code.
+        } if (num_args == 5 && args[3] == args[4]) {
-        // } if (num_args == 5 && args[3] == args[4]) {
+            r = args[3];     // if A c a a --> a
-        //     r = args[3];     // if A c a a --> a
+            return true;
-        //     return true;
         } else {
             return false;
         }
@@ -135,12 +134,47 @@ public:
     virtual bool operator==(value const & other) const { return other.kind() == kind(); }
     virtual void display(std::ostream & out) const { out << "if"; }
     virtual format pp() const { return format("if"); }
-    virtual unsigned hash() const { return 23; }
+    virtual unsigned hash() const { return 27; }
 };
 char const * if_fn_value::g_kind = "if";
 
 MK_BUILTIN(if_fn, if_fn_value);
 
+class implies_fn_value : public value {
+    expr m_type;
+public:
+    static char const * g_kind;
+    implies_fn_value() {
+        m_type = Bool >> (Bool >> Bool);
+    }
+    virtual ~implies_fn_value() {}
+    char const * kind() const { return g_kind; }
+    virtual expr get_type() const { return m_type; }
+    virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
+        if (num_args == 3) {
+            if ((is_bool_value(args[1]) && is_false(args[1])) ||
+                (is_bool_value(args[2]) && is_true(args[2]))) {
+                r = True;
+                return true;
+            } else if (is_bool_value(args[1]) && is_bool_value(args[2]) && is_true(args[1]) && is_false(args[2])) {
+                r = False;
+                return true;
+            }
+        }
+        return false;
+    }
+    virtual bool operator==(value const & other) const { return other.kind() == kind(); }
+    virtual void display(std::ostream & out) const { out << "=>"; }
+    virtual format pp() const { return format("=>"); }
+    virtual unsigned hash() const { return 23; }
+};
+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"));
@@ -156,6 +190,7 @@ 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"));
@@ -203,27 +238,41 @@ void add_basic_theory(environment & env) {
     expr piABx = Pi({x, A}, B(x));
     expr A_arrow_u = A >> TypeU;
 
-    // not(x) = (x = False)
+    // not(x) = (x => False)
-    env.add_definition(not_fn_name, p1, Fun({x, Bool}, Eq(x, False)));
+    env.add_definition(not_fn_name, p1, Fun({x, Bool}, Implies(x, False)));
 
-    // and(x, y) = (if bool x y false)
+    // or(x, y) = Not(x) => y
-    env.add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, False)));
+    env.add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y)));
-    // or(x, y) = (if bool x true y)
+
-    env.add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, True, y)));
+    // and(x, y) = Not(x => Not(y))
+    env.add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y)))));
 
     // forall : Pi (A : Type u), (A -> Bool) -> Bool
     env.add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
+    // TODO: introduce epsilon
     env.add_definition(exists_fn_name, q_type, Fun({{A,TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
 
+    // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
+    env.add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));
+
+    // Discharge : Pi (a b : Bool) (H : a -> b), a => b
+    env.add_axiom(discharge_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a >> b}}, Implies(a, b)));
+
     // Refl : Pi (A : Type u) (a : A), a = a
     env.add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a)));
 
-    // True_neq_False : Not(True = False)
-    env.add_theorem(true_neq_false_name, Not(Eq(True, False)), Trivial);
-
     // Case : Pi (P : Bool -> Bool) (H1 : P True) (H2 : P False) (a : Bool), P a
     env.add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a)));
 
+    // 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)));
+
+    // 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);
 
@@ -231,6 +280,17 @@ void add_basic_theory(environment & env) {
     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)));
@@ -259,12 +319,6 @@ void add_basic_theory(environment & env) {
                                   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)));
 
-    // 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)),

src/kernel/builtin.h

@@ -57,6 +57,11 @@ 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); }
 
+expr mk_implies_fn();
+bool is_implies_fn(expr const & e);
+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 */
 expr mk_and_fn();
 /** \brief Return true iff \c e is the Lean and operator. */
@@ -102,6 +107,15 @@ 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); }
 
+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); }
+
+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); }
 
 expr mk_refl_fn();
 bool is_refl_fn(expr const & e);
@@ -119,6 +133,16 @@ 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 */