From dd21cdcc95061c2c9879d785836f32e4c79961b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Aug 2013 11:23:04 -0700 Subject: [PATCH] Add more theorems. Signed-off-by: Leonardo de Moura --- src/kernel/basic_thms.cpp | 202 ++++++++++++++++++++++++++------------ src/kernel/basic_thms.h | 94 +++++++++++++----- 2 files changed, 208 insertions(+), 88 deletions(-) diff --git a/src/kernel/basic_thms.cpp b/src/kernel/basic_thms.cpp index 7e46972a1..454ce275f 100644 --- a/src/kernel/basic_thms.cpp +++ b/src/kernel/basic_thms.cpp @@ -11,24 +11,34 @@ Author: Leonardo de Moura 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")); +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(double_neg_elim_fn, name("DoubleNegElim")); +MK_CONSTANT(mt_fn, name("MT")); +MK_CONSTANT(contrapos_fn, name("Contrapos")); +MK_CONSTANT(false_imp_any_fn, name("FalseImpAny")); +MK_CONSTANT(eq_mp_fn, name("EqMP")); +MK_CONSTANT(not_imp1_fn, name("NotImp1")); +MK_CONSTANT(not_imp2_fn, name("NotImp2")); +MK_CONSTANT(conj_fn, name("Conj")); +MK_CONSTANT(conjunct1_fn, name("Conjunct1")); +MK_CONSTANT(conjunct2_fn, name("Conjunct2")); +MK_CONSTANT(disj1_fn, name("Disj1")); +MK_CONSTANT(disj2_fn, name("Disj2")); +MK_CONSTANT(disj_cases_fn, name("DisjCases")); +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(eqt_elim_fn, name("EqTElim")); +MK_CONSTANT(eqt_intro_fn, name("EqTIntro")); +MK_CONSTANT(forall_elim_fn, name("ForallElim")); #if 0 MK_CONSTANT(ext_fn, name("ext")); @@ -45,6 +55,7 @@ void add_basic_thms(environment & env) { expr H = Const("H"); expr H1 = Const("H1"); expr H2 = Const("H2"); + expr H3 = Const("H3"); expr B = Const("B"); expr f = Const("f"); expr g = Const("g"); @@ -65,9 +76,13 @@ void add_basic_thms(environment & env) { // True_neq_False : Not(True = False) env.add_theorem(true_neq_false_name, Not(Eq(True, False)), Trivial); - // Truth : True := 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))); @@ -81,6 +96,11 @@ void add_basic_thms(environment & env) { 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))); + // DoubleNegElim : Pi (a : Bool) (P : Bool -> Bool) (H : P (Not (Not a))), (P a) + env.add_theorem(double_neg_elim_fn_name, Pi({{a, Bool}, {P, Bool >> Bool}, {H, P(Not(Not(a)))}}, P(a)), + Fun({{a, Bool}, {P, Bool >> Bool}, {H, P(Not(Not(a)))}}, + Subst(Bool, P, Not(Not(a)), a, H, DoubleNeg(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)}}, @@ -92,41 +112,118 @@ void add_basic_thms(environment & env) { Fun({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, Discharge(Not(b), Not(a), Fun({H1, Not(b)}, MT(a, b, H, H1))))); + // FalseImpliesAny : Pi (a : Bool), False => a + env.add_theorem(false_imp_any_fn_name, Pi({a, Bool}, Implies(False, a)), + Fun({a, Bool}, Case(Fun({x, Bool}, Implies(False, x)), Trivial, Trivial, a))); + + // EqMP : Pi (a b: Bool) (H1 : a = b) (H2 : a), b + 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))); + + // NotImp1 : Pi (a b : Bool) (H : Not(Implies(a, b))), a + env.add_theorem(not_imp1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, a), + Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, + EqMP(Not(Not(a)), a, + DoubleNeg(a), + Discharge(Not(a), False, + Fun({H1, Not(a)}, + Absurd(Implies(a, b), + Discharge(a, b, + Fun({H2, a}, + FalseElim(b, Absurd(a, H2, H1)))), + H)))))); + + // NotImp2 : Pi (a b : Bool) (H : Not(Implies(a, b))), Not(b) + env.add_theorem(not_imp2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, Not(b)), + Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, + Discharge(b, False, + Fun({H1, b}, + Absurd(Implies(a, b), + // a => b + DoubleNegElim(b, Fun({x, Bool}, Implies(a, x)), + // a => Not(Not(b)) + DoubleNegElim(a, Fun({x, Bool}, Implies(x, Not(Not(b)))), + // Not(Not(a)) => Not(Not(b)) + Contrapos(Not(b), Not(a), + Discharge(Not(b), Not(a), + Fun({H2, Not(b)}, + FalseElim(Not(a), Absurd(b, H1, H2))))))), + H))))); + // 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))); + // Conjunct1 : Pi (a b : Bool) (H : And(a, b)), a + env.add_theorem(conjunct1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, a), + Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}}, + NotImp1(a, Not(b), 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))); + // Conjunct2 : Pi (a b : Bool) (H : And(a, b)), b + env.add_theorem(conjunct2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, b), + Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}}, + EqMP(Not(Not(b)), b, DoubleNeg(b), NotImp2(a, Not(b), H)))); - // 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)), + // Disj1 : Pi (a b : Bool) (H : a), Or(a, b) + env.add_theorem(disj1_fn_name, 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))); + // Disj2 : Pi (a b : Bool) (H : b), Or(a, b) + env.add_theorem(disj2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, b}}, Or(a, b)), + Fun({{a, Bool}, {b, Bool}, {H, b}}, + // Not(a) => b + DoubleNegElim(b, Fun({x, Bool}, Implies(Not(a), x)), + // Not(a) => Not(Not(b)) + Contrapos(Not(b), a, + Discharge(Not(b), a, Fun({H1, Not(b)}, + FalseElim(a, Absurd(b, H, H1)))))))); + + // DisjCases : Pi (a b c: Bool) (H1 : Or(a,b)) (H2 : a -> c) (H3 : b -> c), c */ + env.add_theorem(disj_cases_fn_name, Pi({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a,b)}, {H2, a >> c}, {H3, b >> c}}, c), + Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a,b)}, {H2, a >> c}, {H3, b >> c}}, + EqMP(Not(Not(c)), c, DoubleNeg(c), + Discharge(Not(c), False, + Fun({H, Not(c)}, + Absurd(c, + MP(b, c, Discharge(b, c, H3), + MP(Not(a), b, H1, + // Not(a) + MT(a, c, Discharge(a, c, H2), H))), + H)))))); + + // Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a + 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 + 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 + 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))); + + // 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))); + + // 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(True, a, Fun({H2, True}, H))))); + 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))); @@ -149,39 +246,22 @@ void add_basic_thms(environment & env) { 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 + // 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 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 + // 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 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) + // 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 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)), diff --git a/src/kernel/basic_thms.h b/src/kernel/basic_thms.h index 7ad991537..ce31528ee 100644 --- a/src/kernel/basic_thms.h +++ b/src/kernel/basic_thms.h @@ -9,78 +9,118 @@ Author: Leonardo de Moura 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_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); } 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_absurd_fn(); +/** \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_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_double_neg_elim_fn(); +/** \brief (Theorem) a : Bool, P : Bool -> Bool, H : P (Not (Not a)) |- DoubleNegElim(a, P, H) : P a */ +inline expr DoubleNegElim(expr const & a, expr const & P, expr const & H) { return mk_app(mk_double_neg_elim_fn(), a, P, H); } + 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_false_imp_any_fn(); +/** \brief (Theorem) a : Bool, H : False |- a */ +inline expr FalseImpAny(expr const & a, expr const & H) { return mk_app(mk_false_imp_any_fn(), a, H); } + +expr mk_eq_mp_fn(); +/** \brief (Theorem) a 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_not_imp1_fn(); +/** \brief (Theorem) a b : Bool, H : Not(Implies(a, b)) |- NotImp1(a, b, H) : a */ +inline expr NotImp1(expr const & a, expr const & b, expr const & H) { return mk_app(mk_not_imp1_fn(), a, b, H); } + +expr mk_not_imp2_fn(); +/** \brief (Theorem) a b : Bool, H : Not(Implies(a, b)) |- NotImp2(a, b, H) : Not(b) */ +inline expr NotImp2(expr const & a, expr const & b, expr const & H) { return mk_app(mk_not_imp2_fn(), a, b, H); } + +expr mk_conj_fn(); +/** \brief (Theorem) a b : Bool, H1 : a, H2 : b |- Conj(a, b, H1, H2) : And(a, b) */ +inline expr Conj(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_conj_fn(), a, b, H1, H2); } + +expr mk_conjunct1_fn(); +/** \brief (Theorem) a b : Bool, H : And(a, b) |- Conjunct1(a, b, H) : a */ +inline expr Conjunct1(expr const & a, expr const & b, expr const & H) { return mk_app(mk_conjunct1_fn(), a, b, H); } + +expr mk_conjunct2_fn(); +/** \brief (Theorem) a b : Bool, H : And(a, b) |- Conjunct2(a, b, H) : b */ +inline expr Conjunct2(expr const & a, expr const & b, expr const & H) { return mk_app(mk_conjunct2_fn(), a, b, H); } + +expr mk_disj1_fn(); +/** \brief (Theorem) a b : Bool, H : a |- Disj1(a, b, H) : Or(a, b) */ +inline expr Disj1(expr const & a, expr const & b, expr const & H) { return mk_app(mk_disj1_fn(), a, b, H); } + +expr mk_disj2_fn(); +/** \brief (Theorem) a b : Bool, H : b |- Disj2(a, b, H) : Or(a, b) */ +inline expr Disj2(expr const & a, expr const & b, expr const & H) { return mk_app(mk_disj2_fn(), a, b, H); } + +expr mk_disj_cases_fn(); +/** \brief (Theorem) a b c : Bool, H1 : Or(a,b), H2 : a -> c, H3 : b -> c |- DisjCases(a, b, c, H1, H2, H3) : c */ +inline expr DisjCases(expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2, expr const & H3) { return mk_app({mk_disj_cases_fn(), a, b, c, H1, H2, H3}); } + 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_eqt_elim_fn(); +/** \brief (Theorem) a : Bool, H : a = True |- EqTElim(a, H) : a */ +inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); } + +expr mk_eqt_intro_fn(); +/** \brief (Theorem) a : Bool, H : a |- EqTIntro(a, H) : a = True */ +inline expr EqTIntro(expr const & a, expr const & H) { return mk_app(mk_eqt_intro_fn(), a, H); } + 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); }