refactor(kernel/builtin): move definition and axioms to basic.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
b1efdac07b
commit
dfe46b9d25
6 changed files with 70 additions and 102 deletions
|
|
@ -3,9 +3,77 @@ Import macros
|
|||
Definition TypeU := (Type U)
|
||||
Definition TypeM := (Type M)
|
||||
|
||||
Definition implies (a b : Bool) : Bool
|
||||
:= if a b true.
|
||||
|
||||
Infixr 25 => : implies.
|
||||
Infixr 25 ⇒ : implies.
|
||||
|
||||
Definition iff (a b : Bool) : Bool
|
||||
:= a == b.
|
||||
|
||||
Infixr 25 <=> : iff.
|
||||
Infixr 25 ⇔ : iff.
|
||||
|
||||
Definition not (a : Bool) : Bool
|
||||
:= if a false true.
|
||||
|
||||
Notation 40 ¬ _ : not.
|
||||
|
||||
Definition or (a b : Bool) : Bool
|
||||
:= ¬ a ⇒ b.
|
||||
|
||||
Infixr 30 || : or.
|
||||
Infixr 30 \/ : or.
|
||||
Infixr 30 ∨ : or.
|
||||
|
||||
Definition and (a b : Bool) : Bool
|
||||
:= ¬ (a ⇒ ¬ b).
|
||||
|
||||
Infixr 35 && : and.
|
||||
Infixr 35 /\ : and.
|
||||
Infixr 35 ∧ : and.
|
||||
|
||||
(* Forall is a macro for the identifier forall, we use that
|
||||
because the Lean parser has the builtin syntax sugar:
|
||||
forall x : T, P x
|
||||
for
|
||||
(forall T (fun x : T, P x))
|
||||
*)
|
||||
Definition Forall (A : TypeU) (P : A → Bool) : Bool
|
||||
:= P == (λ x : A, true).
|
||||
|
||||
Definition Exists (A : TypeU) (P : A → Bool) : Bool
|
||||
:= ¬ (Forall A (λ x : A, ¬ (P x))).
|
||||
|
||||
Definition eq {A : TypeU} (a b : A) : Bool
|
||||
:= a == b.
|
||||
|
||||
Infix 50 = : eq.
|
||||
|
||||
Axiom MP {a b : Bool} (H1 : a ⇒ b) (H2 : a) : b.
|
||||
|
||||
Axiom Discharge {a b : Bool} (H : a → b) : a ⇒ b.
|
||||
|
||||
Axiom Case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a.
|
||||
|
||||
Axiom Refl {A : TypeU} (a : A) : a == a.
|
||||
|
||||
Axiom Subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P b.
|
||||
|
||||
Definition SubstP {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
|
||||
:= Subst H1 H2.
|
||||
|
||||
Axiom Eta {A : TypeU} {B : A → TypeU} (f : Π x : A, B x) : (λ x : A, f x) == f.
|
||||
|
||||
Axiom ImpAntisym {a b : Bool} (H1 : a ⇒ b) (H2 : b ⇒ a) : a == b.
|
||||
|
||||
Axiom Abst {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (H : Π x : A, f x == g x) : f == g.
|
||||
|
||||
Axiom HSymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a.
|
||||
|
||||
Axiom HTrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c.
|
||||
|
||||
Theorem Trivial : true
|
||||
:= Refl true.
|
||||
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -22,32 +22,8 @@ void init_builtin_notation(environment const & env, io_state & ios, bool kernel_
|
|||
env->import_builtin(
|
||||
"lean_notation",
|
||||
[&]() {
|
||||
add_infix(env, ios, "=", 50, mk_homo_eq_fn());
|
||||
mark_implicit_arguments(env, mk_homo_eq_fn(), 1);
|
||||
mark_implicit_arguments(env, mk_if_fn(), 1);
|
||||
|
||||
add_prefix(env, ios, "\u00ac", 40, mk_not_fn()); // "¬"
|
||||
add_infixr(env, ios, "&&", 35, mk_and_fn()); // "&&"
|
||||
add_infixr(env, ios, "/\\", 35, mk_and_fn()); // "/\"
|
||||
add_infixr(env, ios, "\u2227", 35, mk_and_fn()); // "∧"
|
||||
add_infixr(env, ios, "||", 30, mk_or_fn()); // "||"
|
||||
add_infixr(env, ios, "\\/", 30, mk_or_fn()); // "\/"
|
||||
add_infixr(env, ios, "\u2228", 30, mk_or_fn()); // "∨"
|
||||
add_infixr(env, ios, "=>", 25, mk_implies_fn()); // "=>"
|
||||
add_infixr(env, ios, "\u21D2", 25, mk_implies_fn()); // "⇒"
|
||||
add_infixr(env, ios, "<=>", 25, mk_iff_fn()); // "<=>"
|
||||
add_infixr(env, ios, "\u21D4", 25, mk_iff_fn()); // "⇔"
|
||||
|
||||
// implicit arguments for builtin axioms
|
||||
mark_implicit_arguments(env, mk_mp_fn(), 2);
|
||||
mark_implicit_arguments(env, mk_discharge_fn(), 2);
|
||||
mark_implicit_arguments(env, mk_refl_fn(), 1);
|
||||
mark_implicit_arguments(env, mk_subst_fn(), 4);
|
||||
mark_implicit_arguments(env, mk_eta_fn(), 2);
|
||||
mark_implicit_arguments(env, mk_abst_fn(), 4);
|
||||
mark_implicit_arguments(env, mk_imp_antisym_fn(), 2);
|
||||
mark_implicit_arguments(env, mk_hsymm_fn(), 4);
|
||||
mark_implicit_arguments(env, mk_htrans_fn(), 6);
|
||||
|
||||
if (kernel_only)
|
||||
return;
|
||||
|
|
|
|||
|
|
@ -190,85 +190,10 @@ void import_kernel(environment const & env) {
|
|||
[&]() {
|
||||
env->add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
|
||||
env->add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
|
||||
|
||||
expr p1 = Bool >> Bool;
|
||||
expr p2 = Bool >> p1;
|
||||
expr f = Const("f");
|
||||
expr g = Const("g");
|
||||
expr a = Const("a");
|
||||
expr b = Const("b");
|
||||
expr c = Const("c");
|
||||
expr x = Const("x");
|
||||
expr y = Const("y");
|
||||
expr A = Const("A");
|
||||
expr A_pred = A >> Bool;
|
||||
expr B = Const("B");
|
||||
expr C = Const("C");
|
||||
expr q_type = Pi({A, TypeU}, A_pred >> Bool);
|
||||
expr piABx = Pi({x, A}, B(x));
|
||||
expr A_arrow_u = A >> TypeU;
|
||||
expr P = Const("P");
|
||||
expr H = Const("H");
|
||||
expr H1 = Const("H1");
|
||||
expr H2 = Const("H2");
|
||||
|
||||
env->add_builtin(mk_bool_type());
|
||||
env->add_builtin(mk_bool_value(true));
|
||||
env->add_builtin(mk_bool_value(false));
|
||||
env->add_builtin(mk_if_fn());
|
||||
|
||||
// implies(x, y) := if x y True
|
||||
env->add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
|
||||
|
||||
// iff(x, y) := x = y
|
||||
env->add_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y)));
|
||||
|
||||
// not(x) := if x False True
|
||||
env->add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
|
||||
|
||||
// or(x, y) := Not(x) => y
|
||||
env->add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), 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(Leo): 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)))))));
|
||||
|
||||
// homogeneous equality
|
||||
env->add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y)));
|
||||
|
||||
// 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)));
|
||||
|
||||
// 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)));
|
||||
|
||||
// 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) (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)));
|
||||
|
||||
// ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b
|
||||
env->add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b)));
|
||||
|
||||
// Abst : 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(abst_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)));
|
||||
|
||||
// HSymm : Pi (A B : Type u) (a : A) (b : B) (H1 : a = b), b = a
|
||||
env->add_axiom(hsymm_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {H1, Eq(a, b)}}, Eq(b, a)));
|
||||
|
||||
// HTrans : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c
|
||||
env->add_axiom(htrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)));
|
||||
});
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -16,9 +16,8 @@ using namespace lean;
|
|||
|
||||
static void tst0() {
|
||||
environment env;
|
||||
init_frontend(env);
|
||||
normalizer norm(env);
|
||||
import_kernel(env);
|
||||
import_arith(env);
|
||||
env->add_var("n", Nat);
|
||||
expr n = Const("n");
|
||||
lean_assert_eq(mk_nat_type(), Nat);
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
⊤
|
||||
Assumed: a
|
||||
a ⊕ a ⊕ a
|
||||
@Subst : Π (A : (Type U)) (a b : A) (P : A → Bool), P a → a == b → P b
|
||||
@Subst : Π (A : TypeU) (a b : A) (P : A → Bool), P a → a == b → P b
|
||||
Proved: EM2
|
||||
EM2 : Π a : Bool, a ∨ ¬ a
|
||||
EM2 a : a ∨ ¬ a
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue