Add more theorems

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

src/kernel/builtin.cpp

@@ -124,9 +124,10 @@ public:
             else
                 r = args[4]; // if A false a b --> b
             return true;
-        } if (num_args == 5 && args[3] == args[4]) {
+        // TODO: uncomment the following code.
-            r = args[3];     // if A c a a --> a
+        // } if (num_args == 5 && args[3] == args[4]) {
-            return true;
+        //     r = args[3];     // if A c a a --> a
+        //     return true;
         } else {
             return false;
         }
@@ -147,7 +148,12 @@ 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(symm_fn, name("symm"));
@@ -160,11 +166,13 @@ 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(foralle_fn, name("foralle"));
+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"));
 
+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);
@@ -184,6 +192,7 @@ void add_basic_theory(environment & env) {
     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");
@@ -194,87 +203,129 @@ void add_basic_theory(environment & env) {
     expr piABx = Pi({x, A}, B(x));
     expr A_arrow_u = A >> TypeU;
 
+    // not(x) = (x = False)
+    env.add_definition(not_fn_name, p1, Fun({x, Bool}, Eq(x, False)));
+
     // and(x, y) = (if bool x y false)
-    env.add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
+    env.add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, False)));
     // or(x, y) = (if bool x true y)
-    env.add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, False, y)));
+    env.add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, True, y)));
-    // not(x) = (if bool x false true)
-    env.add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
 
     // 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))));
     env.add_definition(exists_fn_name, q_type, Fun({{A,TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
 
-    // refl : Pi (A : Type u) (a : A), a = a
+    // Refl : Pi (A : Type u) (a : A), a = a
     env.add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a)));
 
-    // subst : Pi (A : Type u) (P : A -> bool) (a b : A) (H1 : P a) (H2 : a = b), P b
+    // 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)));
+
+    // 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)));
+
+    // 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)));
+
+    // 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
+    // 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 :=
+    // 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 :=
+    // 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 :=
+    // 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 :=
+    // 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 :=
+    // 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 :=
+    // 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))));
 
-    // eq_mp : Pi (a b: Bool) (H1 : a = b) (H2 : a), b :=
+    // 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)));
 
-    // truth : True := Refl Bool True
+    // EqTElim : Pi (a : Bool) (H : a = True), a := EqMP(True, a, Symm(Bool, a, True, H), Truth)
-    env.add_theorem(truth_name, True, Refl(Bool, True));
-
-    // eqt_elim : 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)));
 
-    // foralle : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
+    // ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
-    env.add_theorem(foralle_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_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)));
 
-    // 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)));
 
     // 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));

src/kernel/builtin.h

@@ -107,6 +107,7 @@ 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)
 
 expr mk_subst_fn();
 bool is_subst_fn(expr const & e);
@@ -163,15 +164,13 @@ 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_foralle_fn();
+expr mk_forall_elim_fn();
-bool is_foralle_fn(expr const & e);
+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_foralle_fn(), A, P, H, 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_foralle_fn();
-bool is_foralle_fn(expr const & e);
 expr mk_foralli_fn();
 bool is_foralli_fn(expr const & e);
 expr mk_domain_inj_fn();