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

Mark 'implicit' parameters, and move them to the beginning

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-07 21:47:58 -07:00
parent e558edcd52
commit 2d4caa7450
4 changed files with 46 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/kernel/basic_thms.cpp
View file

@ -99,7 +99,7 @@ void add_basic_thms(environment & env) {
// 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))));
Subst(Bool, Not(Not(a)), a, P, 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)),
@ -119,7 +119,7 @@ void add_basic_thms(environment & env) {
// 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)));
Subst(Bool, a, b, Fun({x, Bool}, x), 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),
@ -174,9 +174,9 @@ void add_basic_thms(environment & env) {
Discharge(Not(a), b, Fun({H1, Not(a)},
FalseElim(b, Absurd(a, H, H1))))));
// 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}},
// Disj2 : Pi (b a : Bool) (H : b), Or(a, b)
env.add_theorem(disj2_fn_name, Pi({{b, Bool}, {a, Bool}, {H, b}}, Or(a, b)),
Fun({{b, Bool}, {a, Bool}, {H, b}},
// Not(a) => b
DoubleNegElim(b, Fun({x, Bool}, Implies(Not(a), x)),
// Not(a) => Not(Not(b))
@ -200,17 +200,17 @@ void add_basic_thms(environment & env) {
// 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)));
Subst(A, a, b, Fun({x, A}, Eq(x,a)), 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)));
Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2)));
// TransExt: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c
env.add_theorem(trans_ext_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)));
Subst(B, b, c, Fun({x, B}, Eq(a, x)), 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),
@ -249,18 +249,18 @@ void add_basic_thms(environment & env) {
// 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)));
Subst(piABx, f, g, Fun({h, piABx}, Eq(f(a), h(a))), 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
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)));
// Congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b
env.add_theorem(congr2_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}}, Eq(f(a), f(b))),
Fun({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}},
Subst(A, a, b, Fun({x, A}, Eq(f(a), f(x))), 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
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)}},
TransExt(B(a), B(b), f(a), f(b), g(b),
Congr2(A, B, f, a, b, H2), Congr1(A, B, f, g, b, H1))));
Congr2(A, B, a, b, f, H2), Congr1(A, B, f, g, b, H1))));
// ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a

49
src/kernel/basic_thms.h
View file

@ -25,7 +25,7 @@ expr mk_false_elim_fn();
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 */
/** \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();
@ -33,15 +33,15 @@ expr mk_double_neg_fn();
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 */
/** \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();
/** \brief (Theorem) a b : Bool, H1 : a => b, H2 : Not(b) |- MT(a, b, H1, H2) : Not(a) */
/** \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();
/** \brief (Theorem) a b : Bool, H : a => b |- Contrapos(a, b, H): Neg(b) => Neg(a) */
/** \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();
@ -49,27 +49,27 @@ expr mk_false_imp_any_fn();
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 */
/** \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 */
/** \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) */
/** \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) */
/** \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 */
/** \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 */
/** \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();
@ -77,50 +77,47 @@ expr mk_disj1_fn();
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); }
/** \brief (Theorem) {b} a : Bool, H : b |- Disj2(a, b, H) : Or(a, b) */
inline expr Disj2(expr const & b, expr const & a, expr const & H) { return mk_app(mk_disj2_fn(), b, a, 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 */
/** \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();
/** \brief (Theorem) A : Type u, a b : A, H : a = b |- Symm(A, a, b, H) : b = a */
/** \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();
/** \brief (Theorem) A : Type u, a b c : A, H1 : a = b, H2 : b = c |- Trans(A, a, b, c, H1, H2) : a = c */
/** \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_trans_ext_fn();
/** \brief (Theorem) A : Type u, B : Type u, a : A, b c : B, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
/** \brief (Theorem) {A : Type u}, {B : Type u}, {a : A}, {b c : B}, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
inline expr TransExt(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_trans_ext_fn(), A, B, a, b, c, H1, H2}); }
expr mk_eqt_elim_fn();
/** \brief (Theorem) a : Bool, H : a = True |- EqTElim(a, H) : a */
/** \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 */
/** \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();
/** \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 */
/** \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();
/** \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}); }
/** \brief (Theorem) {A : Type u}, {B : A -> Type u}, {a b : A}, f : (Pi x : A, B x), 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 & a, expr const & b, expr const & f, expr const & H) { return mk_app({mk_congr2_fn(), A, B, a, b, f, H}); }
expr mk_congr_fn();
/** \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 */
/** \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_forall_elim_fn();
// \brief (Theorem) A : Type u, P : A -> Bool, H : (Forall A P), a : A |- Forallelim(A, P, H, a) : P a
// \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); }
/** \brief Add basic theorems to Environment */

4
src/kernel/builtin.cpp
View file

@ -233,8 +233,8 @@ void add_basic_theory(environment & env) {
// 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)));
// Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b
env.add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {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)));

14
src/kernel/builtin.h
View file

@ -94,17 +94,17 @@ inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); }
/** \brief Modus Ponens axiom */
expr mk_mp_fn();
/** \brief (Axiom) a : Bool, b : Bool, H1 : a => b, H2 : a |- MP(a, b, H1, H2) : b */
/** \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); }
/** \brief Discharge axiom */
expr mk_discharge_fn();
/** \brief (Axiom) a : Bool, b : Bool, H : a -> b |- Discharge(a, b, H) : a => b */
/** \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); }
/** \brief Reflexivity axiom */
expr mk_refl_fn();
/** \brief (Axiom) A : Type u, a : A |- Refl(A, a) : a = a */
/** \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); }
/** \brief Case analysis axiom */
@ -114,17 +114,17 @@ inline expr Case(expr const & P, expr const & H1, expr const & H2, expr const &
/** \brief Substitution axiom */
expr mk_subst_fn();
/** \brief (Axiom) A : Type u, P : A -> Bool, a b : A, H1 : P a, H2 : a = b |- Subst(A, P, a, b, H1, H2) : P b */
inline expr Subst(expr const & A, expr const & P, expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app({mk_subst_fn(), A, P, a, b, H1, H2}); }
/** \brief (Axiom) {A : Type u}, {a b : A}, P : A -> Bool, H1 : P a, H2 : a = b |- Subst(A, a, b, P, H1, H2) : P b */
inline expr Subst(expr const & A, expr const & a, expr const & b, expr const & P, expr const & H1, expr const & H2) { return mk_app({mk_subst_fn(), A, a, b, P, H1, H2}); }
/** \brief Eta conversion axiom */
expr mk_eta_fn();
/** \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) */
/** \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); }
/** \brief Implies Anti-symmetry */
expr mk_imp_antisym_fn();
/** \brief (Axiom) a : Bool, b : Bool, H1 : a => b, H2 : b => a |- ImpAntisym(a, b, H1, H2) : a = b */
/** \brief (Axiom) {a : Bool}, {b : Bool}, H1 : a => b, H2 : b => a |- ImpAntisym(a, b, H1, H2) : a = b */
inline expr ImpAntisym(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_imp_antisym_fn(), a, b, H1, H2); }
class environment;