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

refactor(library/basic_thms): move the proof of all basic theorems to a .Lean file

Browse source 
This commit also adds several new theorems that are useful for implementing the simplifier.
TODO: perhaps we should remove the declarations at basic_thms.h?

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-29 02:44:49 -08:00
parent a05c815d31
commit 411ebbc3c1
47 changed files with 642 additions and 561 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
examples/lean/ex3.lean
View file

@ -4,7 +4,7 @@ Theorem and_comm (a b : Bool) : (a ∧ b) ⇒ (b ∧ a) :=
Theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a) :=
Discharge (λ H_ab, DisjCases H_ab
(λ H_a, Disj2 b H_a)
(λ H_b, Disj1 a H_b))
(λ H_b, Disj1 H_b a))
(* ---------------------------------
(EM a) is the excluded middle a ∨ ¬a

20
src/builtin/CMakeLists.txt
View file

@ -9,18 +9,28 @@ add_library(builtin builtin.cpp)
# without installing it.
set(SHELL_DIR ${LEAN_BINARY_DIR}/shell)
file(GLOB LEANLIB "*.lean")
FOREACH(FILE ${LEANLIB})
function(add_theory_core FILE ARG EXTRA_DEPS)
get_filename_component(BASENAME ${FILE} NAME_WE)
set(FNAME "${BASENAME}.olean")
add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
COMMAND ${SHELL_DIR}/lean -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${FILE}
COMMAND ${SHELL_DIR}/lean ${ARG} -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE}
COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${SHELL_DIR}/${FNAME}
DEPENDS ${FILE} ${SHELL_DIR}/lean)
DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${SHELL_DIR}/lean ${EXTRA_DEPS})
add_custom_target(${FNAME}_builtin DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME})
add_dependencies(builtin ${FNAME}_builtin)
install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
ENDFOREACH(FILE)
endfunction()
function(add_kernel_theory FILE)
add_theory_core(${FILE} "-k" "")
endfunction()
function(add_theory FILE)
add_theory_core(${FILE} "" "${CMAKE_CURRENT_BINARY_DIR}/basic.olean")
endfunction()
add_kernel_theory("basic.lean")
add_theory("cast.lean")
file(GLOB LEANLIB "*.lua")
FOREACH(FILE ${LEANLIB})

261
src/builtin/basic.lean Normal file
View file

@ -0,0 +1,261 @@
Import macros
Definition TypeU := (Type U)
Definition SubstP {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
:= Subst H1 H2.
Theorem Trivial : true
:= Refl true.
Theorem TrueNeFalse : not (true == false)
:= Trivial.
Theorem EM (a : Bool) : a ∨ ¬ a
:= Case (λ x, x ∨ ¬ x) Trivial Trivial a.
Theorem FalseElim (a : Bool) (H : false) : a
:= Case (λ x, x) Trivial H a.
Theorem Absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
:= MP H2 H1.
Theorem EqMP {a b : Bool} (H1 : a == b) (H2 : a) : b
:= Subst H2 H1.
Theorem DoubleNeg (a : Bool) : (¬ ¬ a) == a
:= Case (λ x, (¬ ¬ x) == x) Trivial Trivial a.
Theorem DoubleNegElim {a : Bool} (H : ¬ ¬ a) : a
:= EqMP (DoubleNeg a) H.
Theorem MT {a b : Bool} (H1 : a ⇒ b) (H2 : ¬ b) : ¬ a
:= assume H : a, Absurd (MP H1 H) H2.
Theorem Contrapos {a b : Bool} (H : a ⇒ b) : ¬ b ⇒ ¬ a
:= assume H1 : ¬ b, MT H H1.
Theorem AbsurdElim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
:= FalseElim b (Absurd H1 H2).
Theorem NotImp1 {a b : Bool} (H : ¬ (a ⇒ b)) : a
:= DoubleNegElim
(show ¬ ¬ a,
assume H1 : ¬ a, Absurd (show a ⇒ b, assume H2 : a, AbsurdElim b H2 H1)
(show ¬ (a ⇒ b), H)).
Theorem NotImp2 {a b : Bool} (H : ¬ (a ⇒ b)) : ¬ b
:= assume H1 : b, Absurd (show a ⇒ b, assume H2 : a, H1)
(show ¬ (a ⇒ b), H).
(* Remark: conjunction is defined as ¬ (a ⇒ ¬ b) in Lean *)
Theorem Conj {a b : Bool} (H1 : a) (H2 : b) : a ∧ b
:= assume H : a ⇒ ¬ b, Absurd H2 (MP H H1).
Theorem Conjunct1 {a b : Bool} (H : a ∧ b) : a
:= NotImp1 H.
Theorem Conjunct2 {a b : Bool} (H : a ∧ b) : b
:= DoubleNegElim (NotImp2 H).
(* Remark: disjunction is defined as ¬ a ⇒ b in Lean *)
Theorem Disj1 {a : Bool} (H : a) (b : Bool) : a ∨ b
:= assume H1 : ¬ a, AbsurdElim b H H1.
Theorem Disj2 {b : Bool} (a : Bool) (H : b) : a ∨ b
:= assume H1 : ¬ a, H.
Theorem ArrowToImplies {a b : Bool} (H : a → b) : a ⇒ b
:= assume H1 : a, H H1.
Theorem Resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b
:= MP H1 H2.
Theorem DisjCases {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
:= DoubleNegElim
(assume H : ¬ c,
Absurd (show c, H3 (show b, Resolve1 H1 (show ¬ a, (MT (ArrowToImplies H2) H))))
H)
Theorem Refute {a : Bool} (H : ¬ a → false) : a
:= DisjCases (EM a) (λ H1 : a, H1) (λ H1 : ¬ a, FalseElim a (H H1)).
Theorem Symm {A : TypeU} {a b : A} (H : a == b) : b == a
:= Subst (Refl a) H.
Theorem Trans {A : TypeU} {a b c : A} (H1 : a == b) (H2 : b == c) : a == c
:= Subst H1 H2.
Theorem EqTElim {a : Bool} (H : a == true) : a
:= EqMP (Symm H) Trivial.
Theorem EqTIntro {a : Bool} (H : a) : a == true
:= ImpAntisym (assume H1 : a, Trivial)
(assume H2 : true, H).
Theorem Congr1 {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a
:= SubstP (fun h : (Π x : A, B x), f a == h a) (Refl (f a)) H.
(*
Remark: we must use heterogeneous equality in the following theorem because the types of (f a) and (f b)
are not "definitionally equal". They are (B a) and (B b).
They are provably equal, we just have to apply Congr1.
*)
Theorem Congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b
:= SubstP (fun x : A, f a == f x) (Refl (f a)) H.
(*
Remark: like the previous theorem we use heterogeneous equality. We cannot use Trans theorem
because the types are not definitionally equal.
*)
Theorem Congr {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b
:= HTrans (Congr2 f H2) (Congr1 b H1).
Theorem ForallElim {A : TypeU} {P : A → Bool} (H : Forall A P) (a : A) : P a
:= EqTElim (Congr1 a H).
Theorem ForallIntro {A : TypeU} {P : A → Bool} (H : Π x : A, P x) : Forall A P
:= Trans (Symm (Eta P))
(Abst (λ x, EqTIntro (H x))).
(* Remark: the existential is defined as (¬ (forall x : A, ¬ P x)) *)
Theorem ExistsElim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : Π (a : A) (H : P a), B) : B
:= Refute (λ R : ¬ B,
Absurd (ForallIntro (λ a : A, MT (assume H : P a, H2 a H) R))
H1).
Theorem ExistsIntro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
:= assume H1 : (∀ x : A, ¬ P x),
Absurd H (ForallElim H1 a).
(*
At this point, we have proved the theorems we need using the
definitions of forall, exists, and, or, =>, not. We mark (some of)
them as opaque. Opaque definitions improve performance, and
effectiveness of Lean's elaborator.
*)
SetOpaque implies true.
SetOpaque iff true.
SetOpaque not true.
SetOpaque or true.
SetOpaque and true.
SetOpaque forall true.
Theorem OrComm (a b : Bool) : (a ∨ b) == (b ∨ a)
:= ImpAntisym (assume H, DisjCases H (λ H1, Disj2 b H1) (λ H2, Disj1 H2 a))
(assume H, DisjCases H (λ H1, Disj2 a H1) (λ H2, Disj1 H2 b)).
Theorem OrAssoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c))
:= ImpAntisym (assume H : (a ∨ b) ∨ c,
DisjCases H (λ H1 : a ∨ b, DisjCases H1 (λ Ha : a, Disj1 Ha (b ∨ c)) (λ Hb : b, Disj2 a (Disj1 Hb c)))
(λ Hc : c, Disj2 a (Disj2 b Hc)))
(assume H : a ∨ (b ∨ c),
DisjCases H (λ Ha : a, (Disj1 (Disj1 Ha b) c))
(λ H1 : b ∨ c, DisjCases H1 (λ Hb : b, Disj1 (Disj2 a Hb) c)
(λ Hc : c, Disj2 (a ∨ b) Hc))).
Theorem OrId (a : Bool) : (a ∨ a) == a
:= ImpAntisym (assume H, DisjCases H (λ H1, H1) (λ H2, H2))
(assume H, Disj1 H a).
Theorem OrRhsFalse (a : Bool) : (a ∨ false) == a
:= ImpAntisym (assume H, DisjCases H (λ H1, H1) (λ H2, FalseElim a H2))
(assume H, Disj1 H false).
Theorem OrLhsFalse (a : Bool) : (false ∨ a) == a
:= Trans (OrComm false a) (OrRhsFalse a).
Theorem OrLhsTrue (a : Bool) : (true ∨ a) == true
:= EqTIntro (Case (λ x : Bool, true ∨ x) Trivial Trivial a).
Theorem OrRhsTrue (a : Bool) : (a ∨ true) == true
:= Trans (OrComm a true) (OrLhsTrue a).
Theorem OrAnotA (a : Bool) : (a ∨ ¬ a) == true
:= EqTIntro (EM a).
Theorem AndComm (a b : Bool) : (a ∧ b) == (b ∧ a)
:= ImpAntisym (assume H, Conj (Conjunct2 H) (Conjunct1 H))
(assume H, Conj (Conjunct2 H) (Conjunct1 H)).
Theorem AndId (a : Bool) : (a ∧ a) == a
:= ImpAntisym (assume H, Conjunct1 H)
(assume H, Conj H H).
Theorem AndAssoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c))
:= ImpAntisym (assume H, Conj (Conjunct1 (Conjunct1 H)) (Conj (Conjunct2 (Conjunct1 H)) (Conjunct2 H)))
(assume H, Conj (Conj (Conjunct1 H) (Conjunct1 (Conjunct2 H))) (Conjunct2 (Conjunct2 H))).
Theorem AndRhsTrue (a : Bool) : (a ∧ true) == a
:= ImpAntisym (assume H : a ∧ true, Conjunct1 H)
(assume H : a, Conj H Trivial).
Theorem AndLhsTrue (a : Bool) : (true ∧ a) == a
:= Trans (AndComm true a) (AndRhsTrue a).
Theorem AndRhsFalse (a : Bool) : (a ∧ false) == false
:= ImpAntisym (assume H, Conjunct2 H)
(assume H, FalseElim (a ∧ false) H).
Theorem AndLhsFalse (a : Bool) : (false ∧ a) == false
:= Trans (AndComm false a) (AndRhsFalse a).
Theorem AndAnotA (a : Bool) : (a ∧ ¬ a) == false
:= ImpAntisym (assume H, Absurd (Conjunct1 H) (Conjunct2 H))
(assume H, FalseElim (a ∧ ¬ a) H).
Theorem NotTrue : (¬ true) == false
:= Trivial
Theorem NotFalse : (¬ false) == true
:= Trivial
Theorem NotAnd (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b)
:= Case (λ x, (¬ (x ∧ b)) == (¬ x ∨ ¬ b))
(Case (λ y, (¬ (true ∧ y)) == (¬ true ∨ ¬ y)) Trivial Trivial b)
(Case (λ y, (¬ (false ∧ y)) == (¬ false ∨ ¬ y)) Trivial Trivial b)
a
Theorem NotOr (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b)
:= Case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b))
(Case (λ y, (¬ (true ∨ y)) == (¬ true ∧ ¬ y)) Trivial Trivial b)
(Case (λ y, (¬ (false ∨ y)) == (¬ false ∧ ¬ y)) Trivial Trivial b)
a
Theorem NotEq (a b : Bool) : (¬ (a == b)) == ((¬ a) == b)
:= Case (λ x, (¬ (x == b)) == ((¬ x) == b))
(Case (λ y, (¬ (true == y)) == ((¬ true) == y)) Trivial Trivial b)
(Case (λ y, (¬ (false == y)) == ((¬ false) == y)) Trivial Trivial b)
a
Theorem NotImp (a b : Bool) : (¬ (a ⇒ b)) == (a ∧ ¬ b)
:= Case (λ x, (¬ (x ⇒ b)) == (x ∧ ¬ b))
(Case (λ y, (¬ (true ⇒ y)) == (true ∧ ¬ y)) Trivial Trivial b)
(Case (λ y, (¬ (false ⇒ y)) == (false ∧ ¬ y)) Trivial Trivial b)
a
Theorem NotCongr {a b : Bool} (H : a == b) : (¬ a) == (¬ b)
:= Congr2 not H.
Theorem ForallEqIntro {A : (Type U)} {P Q : A → Bool} (H : Pi x : A, P x == Q x) : (∀ x : A, P x) == (∀ x : A, Q x)
:= Congr2 (Forall A) (Abst H).
Theorem ExistsEqIntro {A : (Type U)} {P Q : A → Bool} (H : Pi x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x)
:= Congr2 (Exists A) (Abst H).
Theorem NotForall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ (P x))
:= let L1 : (¬ (∀ x : A, ¬ (¬ (P x)))) == (∃ x : A, (¬ (P x))) := Refl (∃ x : A, ¬ (P x)),
L2 : (¬ (∀ x : A, P x)) == (¬ (∀ x : A, ¬ (¬ (P x)))) :=
NotCongr (ForallEqIntro (λ x : A, (Symm (DoubleNeg (P x)))))
in Trans L2 L1.
Theorem NotExists (A : (Type U)) (P : A → Bool) : (¬ (∃ x : A, P x)) == (∀ x : A, ¬ (P x))
:= let L1 : (¬ (∃ x : A, P x)) == (¬ (¬ (∀ x : A, ¬ (P x)))) := Refl (¬ (∃ x : A, P x)),
L2 : (¬ (¬ (∀ x : A, ¬ (P x)))) == (∀ x : A, ¬ (P x)) := DoubleNeg (∀ x : A, ¬ (P x))
in Trans L1 L2.

14
src/frontends/lean/frontend.cpp
View file

@ -17,6 +17,7 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
#include "kernel/expr_maps.h"
#include "kernel/expr_sets.h"
#include "kernel/builtin.h"
#include "library/expr_pair.h"
#include "library/expr_pair_maps.h"
#include "library/io_state.h"
@ -519,10 +520,17 @@ static lean_extension & to_ext(environment const & env) {
/**
\brief Import all definitions and notation.
*/
void init_frontend(environment const & env, io_state & ios) {
void init_frontend(environment const & env, io_state & ios, bool kernel_only) {
ios.set_formatter(mk_pp_formatter(env));
import_all(env);
init_builtin_notation(env, ios);
if (kernel_only)
import_kernel(env);
else
import_all(env);
init_builtin_notation(env, ios, kernel_only);
}
void init_frontend(environment const & env) {
io_state ios;
init_frontend(env, ios);
}
void add_infix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) {

3
src/frontends/lean/frontend.h
View file

@ -16,7 +16,8 @@ namespace lean {
/**
\brief Import all definitions and notation.
*/
void init_frontend(environment const & env, io_state & ios);
void init_frontend(environment const & env, io_state & ios, bool kernel_only = false);
void init_frontend(environment const & env);
/**
@name Notation for parsing and pretty printing.

56
src/frontends/lean/notation.cpp
View file

@ -18,7 +18,7 @@ void add_alias(environment const & env, name const & n, name const & m) {
/**
\brief Initialize builtin notation.
*/
void init_builtin_notation(environment const & env, io_state & ios) {
void init_builtin_notation(environment const & env, io_state & ios, bool kernel_only) {
env->import_builtin(
"lean_notation",
[&]() {
@ -38,6 +38,20 @@ void init_builtin_notation(environment const & env, io_state & ios) {
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;
add_infixl(env, ios, "+", 65, mk_nat_add_fn());
add_infixl(env, ios, "-", 65, mk_nat_sub_fn());
add_prefix(env, ios, "-", 75, mk_nat_neg_fn());
@ -81,46 +95,6 @@ void init_builtin_notation(environment const & env, io_state & ios) {
add_coercion(env, mk_nat_to_int_fn());
add_coercion(env, mk_int_to_real_fn());
add_coercion(env, mk_nat_to_real_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);
add_alias(env, "Subst", "SubstP");
mark_implicit_arguments(env, "SubstP", 3);
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);
// implicit arguments for basic theorems
mark_implicit_arguments(env, mk_absurd_fn(), 1);
mark_implicit_arguments(env, mk_double_neg_elim_fn(), 1);
mark_implicit_arguments(env, mk_mt_fn(), 2);
mark_implicit_arguments(env, mk_contrapos_fn(), 2);
mark_implicit_arguments(env, mk_eq_mp_fn(), 2);
mark_implicit_arguments(env, mk_not_imp1_fn(), 2);
mark_implicit_arguments(env, mk_not_imp2_fn(), 2);
mark_implicit_arguments(env, mk_conj_fn(), 2);
mark_implicit_arguments(env, mk_conjunct1_fn(), 2);
mark_implicit_arguments(env, mk_conjunct2_fn(), 2);
mark_implicit_arguments(env, mk_disj1_fn(), 1);
mark_implicit_arguments(env, mk_disj2_fn(), 1);
mark_implicit_arguments(env, mk_disj_cases_fn(), 3);
mark_implicit_arguments(env, mk_refute_fn(), 1);
mark_implicit_arguments(env, mk_symm_fn(), 3);
mark_implicit_arguments(env, mk_trans_fn(), 4);
mark_implicit_arguments(env, mk_eqt_elim_fn(), 1);
mark_implicit_arguments(env, mk_eqt_intro_fn(), 1);
mark_implicit_arguments(env, mk_congr1_fn(), 4);
mark_implicit_arguments(env, mk_congr2_fn(), 4);
mark_implicit_arguments(env, mk_congr_fn(), 6);
mark_implicit_arguments(env, mk_forall_elim_fn(), 2);
mark_implicit_arguments(env, mk_forall_intro_fn(), 2);
mark_implicit_arguments(env, mk_exists_elim_fn(), 3);
mark_implicit_arguments(env, mk_exists_intro_fn(), 2);
});
}
}

2
src/frontends/lean/notation.h
View file

@ -12,5 +12,5 @@ constexpr unsigned g_arrow_precedence = 25;
constexpr unsigned g_app_precedence = std::numeric_limits<unsigned>::max();
class environment;
class io_state;
void init_builtin_notation(environment const & env, io_state & st);
void init_builtin_notation(environment const & env, io_state & st, bool kernel_only = false);
}

38
src/frontends/lean/parser.cpp
View file

@ -93,7 +93,8 @@ static name g_infixl_kwd("Infixl");
static name g_infixr_kwd("Infixr");
static name g_notation_kwd("Notation");
static name g_echo_kwd("Echo");
static name g_set_kwd("SetOption");
static name g_set_option_kwd("SetOption");
static name g_set_opaque_kwd("SetOpaque");
static name g_options_kwd("Options");
static name g_env_kwd("Environment");
static name g_import_kwd("Import");
@ -113,8 +114,8 @@ static list<name> g_tactic_cmds = { g_apply, g_done, g_back, g_abort, g_assumpti
/** \brief Table/List with all builtin command keywords */
static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd,
g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd, g_exit_kwd, g_push_kwd,
g_pop_kwd, g_scope_kwd, g_end_scope_kwd};
g_set_option_kwd, g_set_opaque_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd,
g_exit_kwd, g_push_kwd, g_pop_kwd, g_scope_kwd, g_end_scope_kwd};
// ==========================================
// ==========================================
@ -2341,7 +2342,7 @@ class parser::imp {
}
/** Parse 'SetOption' [id] [value] */
void parse_set() {
void parse_set_option() {
next();
auto id_pos = pos();
name id = check_identifier_next("invalid set options, identifier (i.e., option name) expected");
@ -2393,6 +2394,29 @@ class parser::imp {
regular(m_io_state) << " Set: " << id << endl;
}
/** Parse 'SetOpaque' [id] [true/false] */
void parse_set_opaque() {
next();
name id;
if (curr() == scanner::token::Forall) {
id = "forall";
} else if (curr() == scanner::token::Exists) {
id = "exists";
} else {
check_identifier("invalid set opaque, identifier expected");
id = curr_name();
}
next();
auto val_pos = pos();
name val = check_identifier_next("invalid opaque flag, true/false expected");
if (val == "true")
m_env->set_opaque(id, true);
else if (val == "false")
m_env->set_opaque(id, false);
else
throw parser_error("invalid opaque flag, true/false expected", val_pos);
}
optional<std::string> find_lua_file(std::string const & fname) {
try {
return some(find_file(fname, {".lua"}));
@ -2554,8 +2578,10 @@ class parser::imp {
parse_notation_decl();
} else if (cmd_id == g_echo_kwd) {
parse_echo();
} else if (cmd_id == g_set_kwd) {
parse_set();
} else if (cmd_id == g_set_option_kwd) {
parse_set_option();
} else if (cmd_id == g_set_opaque_kwd) {
parse_set_opaque();
} else if (cmd_id == g_import_kwd) {
parse_import();
} else if (cmd_id == g_help_kwd) {

4
src/frontends/lean/pp.cpp
View file

@ -256,10 +256,10 @@ class pp_fn {
return mk_result(format("_"), 1);
} else if (is_forall_fn(e)) {
// use alias when forall is used as a function symbol
return mk_result(format(const_name(mk_Forall_fn())), 1);
return mk_result(format("Forall"), 1);
} else if (is_exists_fn(e)) {
// use alias when exists is used as a function symbol
return mk_result(format(const_name(mk_Exists_fn())), 1);
return mk_result(format("Exists"), 1);
} else if (has_implicit_arguments(n)) {
return mk_result(format(get_explicit_version(m_env, n)), 1);
} else {

31
src/frontends/lean/scanner.cpp
View file

@ -24,8 +24,10 @@ static name g_in_name("in");
static name g_arrow_name("->");
static name g_eq_name("==");
static name g_forall_name("forall");
static name g_Forall_name("Forall");
static name g_forall_unicode("\u2200");
static name g_exists_name("exists");
static name g_Exists_name("Exists");
static name g_exists_unicode("\u2203");
static name g_placeholder_name("_");
static name g_show_name("show");
@ -206,28 +208,35 @@ scanner::token scanner::read_a_symbol() {
only_digits = (normalize(curr()) == '0');
} else {
m_name_val = mk_name(m_name_val, m_buffer, only_digits);
if (m_name_val == g_lambda_name)
if (m_name_val == g_lambda_name) {
return token::Lambda;
else if (m_name_val == g_pi_name)
} else if (m_name_val == g_pi_name) {
return token::Pi;
else if (m_name_val == g_forall_name)
} else if (m_name_val == g_forall_name) {
return token::Forall;
else if (m_name_val == g_exists_name)
} else if (m_name_val == g_exists_name) {
return token::Exists;
else if (m_name_val == g_type_name)
} else if (m_name_val == g_type_name) {
return token::Type;
else if (m_name_val == g_let_name)
} else if (m_name_val == g_let_name) {
return token::Let;
else if (m_name_val == g_in_name)
} else if (m_name_val == g_in_name) {
return token::In;
else if (m_name_val == g_placeholder_name)
} else if (m_name_val == g_placeholder_name) {
return token::Placeholder;
else if (m_name_val == g_show_name)
} else if (m_name_val == g_show_name) {
return token::Show;
else if (m_name_val == g_by_name)
} else if (m_name_val == g_by_name) {
return token::By;
else
} else if (m_name_val == g_Forall_name) {
m_name_val = g_forall_name;
return token::Id;
} else if (m_name_val == g_Exists_name) {
m_name_val = g_exists_name;
return token::Id;
} else {
return is_command(m_name_val) ? token::CommandId : token::Id;
}
}
}
}

21
src/kernel/builtin.cpp
View file

@ -192,8 +192,6 @@ bool is_not(expr const & e, expr & a) {
}
MK_CONSTANT(forall_fn, name("forall"));
MK_CONSTANT(exists_fn, name("exists"));
MK_CONSTANT(Forall_fn, name("Forall"));
MK_CONSTANT(Exists_fn, name("Exists"));
MK_CONSTANT(homo_eq_fn, name("eq"));
bool is_homo_eq(expr const & e, expr & lhs, expr & rhs) {
@ -219,9 +217,9 @@ MK_CONSTANT(abst_fn, name("Abst"));
MK_CONSTANT(htrans_fn, name("HTrans"));
MK_CONSTANT(hsymm_fn, name("HSymm"));
void import_basic(environment const & env) {
void import_kernel(environment const & env) {
env->import_builtin
("basic",
("kernel",
[&]() {
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);
@ -253,27 +251,24 @@ void import_basic(environment const & env) {
env->add_builtin(mk_if_fn());
// implies(x, y) := if x y True
env->add_opaque_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(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_opaque_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(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_opaque_definition(not_fn_name, p1, Fun({x, Bool}, bIf(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_opaque_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(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_opaque_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(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_opaque_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
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)))))));
// Aliases for forall and exists
env->add_definition(Forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Forall(A, P)));
env->add_definition(Exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Exists(A, P)));
// 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)));

6
src/kernel/builtin.h
View file

@ -121,8 +121,6 @@ inline bool is_forall(expr const & e) { return is_app(e) && is_forall_fn(arg(e,
/** \brief Return the term (Forall A P), where A is a type and P : A -> bool */
inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); }
inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); }
/** \brief Return alias \c Forall for \c forall */
expr mk_Forall_fn();
/** \brief Return the Lean exists operator. It has type: <tt>Pi (A : Type), (A -> Bool) -> Bool</tt> */
expr mk_exists_fn();
@ -131,8 +129,6 @@ inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e,
/** \brief Return the term (exists A P), where A is a type and P : A -> bool */
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); }
/** \brief Return alias \c Exists for \c exists */
expr mk_Exists_fn();
/** \brief Homogeneous equality. It has type: <tt>Pi (A : Type), A -> A -> Bool</tt> */
expr mk_homo_eq_fn();
@ -199,7 +195,7 @@ inline expr HTrans(expr const & A, expr const & B, expr const & C, expr const &
class environment;
/** \brief Initialize the environment with basic builtin declarations and axioms */
void import_basic(environment const & env);
void import_kernel(environment const & env);
/**
\brief Helper macro for defining constants such as bool_type, int_type, int_add, etc.

2
src/library/all/all.cpp
View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura
namespace lean {
void import_all(environment const & env) {
import_basic(env);
import_kernel(env);
import_basic_thms(env);
import_arith(env);
}

243
src/library/basic_thms.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
#include "kernel/abstract.h"
#include "kernel/type_checker.h"
#include "library/io_state.h"
#include "library/basic_thms.h"
#include "kernel/kernel_exception.h"
@ -23,7 +24,7 @@ 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(absurd_imp_any_fn, name("AbsurdImpAny"));
MK_CONSTANT(absurd_elim_fn, name("AbsurdElim"));
MK_CONSTANT(eq_mp_fn, name("EqMP"));
MK_CONSTANT(not_imp1_fn, name("NotImp1"));
MK_CONSTANT(not_imp2_fn, name("NotImp2"));
@ -47,243 +48,7 @@ MK_CONSTANT(exists_elim_fn, name("ExistsElim"));
MK_CONSTANT(exists_intro_fn, name("ExistsIntro"));
void import_basic_thms(environment const & env) {
env->import_builtin(
"basic_thms",
[&]() {
expr A = Const("A");
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
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");
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");
expr a1 = Const("a1");
expr R = Const("R");
expr A_pred = A >> Bool;
expr q_type = Pi({A, TypeU}, A_pred >> Bool);
expr piABx = Pi({x, A}, B(x));
expr A_arrow_u = A >> TypeU;
// Trivial : True
env->add_theorem(trivial_name, True, Refl(Bool, True));
// True_neq_False : Not(True = False)
env->add_theorem(true_neq_false_name, Not(Eq(True, False)), 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), Trivial, 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)));
// 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, a, b, Fun({x, Bool}, x), H2, H1)));
// 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)));
// DoubleNegElim : Pi (P : Bool) (H : Not (Not P)), P
env->add_theorem(double_neg_elim_fn_name, Pi({{P, Bool}, {H, Not(Not(P))}}, P),
Fun({{P, Bool}, {H, Not(Not(P))}},
EqMP(Not(Not(P)), P, DoubleNeg(P), H)));
// 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)}},
Discharge(a, False, Fun({H, a},
Absurd(b, MP(a, b, H1, H), H2)))));
// Contrapositive : Pi (a b : Bool) (H : a => b), (Not(b) => Not(a))
env->add_theorem(contrapos_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, Implies(Not(b), Not(a))),
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)));
// AbsurdImpliesAny : Pi (a c : Bool) (H1 : a) (H2 : Not a), c
env->add_theorem(absurd_imp_any_fn_name, Pi({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, c),
Fun({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}},
MP(False, c, FalseImpAny(c), Absurd(a, H1, H2))));
// 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
Discharge(a, b, Fun({H2, a}, H1)),
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))))));
// 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)));
// 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))));
// 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))))));
// 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}},
Discharge(Not(a), b, Fun({H1, Not(a)}, H))));
// 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))))));
// Refute : Pi {a : Bool} (H : not a -> false), a */
env->add_theorem(refute_fn_name, Pi({{a, Bool}, {H, Not(a) >> False}}, a),
Fun({{a, Bool}, {H, Not(a) >> False}},
DisjCases(a, Not(a), a, EM(a), Fun({H1, a}, H1), Fun({H1, Not(a)}, FalseElim(a, H(H1))))));
// 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, 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, b, c, Fun({x, A}, 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),
Fun({{a, Bool}, {H, Eq(a, True)}},
EqMP(True, a, Symm(Bool, a, True, H), Trivial)));
// 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}, Trivial)),
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)));
env->add_theorem(name("OrComm"), 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("OrAssoc"), 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)));
// 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, f, g, Fun({h, piABx}, Eq(f(a), h(a))), Refl(B(a), f(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(B(a), f(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)}},
HTrans(B(a), B(b), B(b), f(a), f(b), g(b),
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
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))));
// ForallIntro : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P)
env->add_theorem(forall_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P)),
Fun({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}},
Trans(A_pred, P, Fun({x, A}, P(x)), Fun({x, A}, True),
Symm(A_pred, Fun({x, A}, P(x)), P, Eta(A, Fun({x, A}, Bool), P)), // P == fun x : A, P x
Abst(A, Fun({x, A}, Bool), Fun({x, A}, P(x)), Fun({x, A}, True), Fun({x, A}, EqTIntro(P(x), H(x)))))));
// ExistsElim : Pi (A : Type U) (P : A -> Bool) (B : Bool) (H1 : exists x : A, P x) (H2 : Pi (a : A) (H : P a), B) : B :=
env->add_theorem(exists_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}}, B),
Fun({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}},
Refute(B, Fun({R, Not(B)},
Absurd(mk_forall(A, Fun({x, A}, Not(P(x)))),
ForallIntro(A, Fun({x, A}, Not(P(x))), Fun({a, A}, MT(P(a), B, Discharge(P(a), B, Fun({H, P(a)}, H2(a, H))), R))),
H1)))));
// ExistsIntro : Pi (A : Type u) (P : A -> bool) (a : A) (H : P a), exists A P
env->add_theorem(exists_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}}, mk_exists(A, P)),
Fun({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}},
Discharge(mk_forall(A, Fun({x, A}, Not(P(x)))), False,
Fun({H2, mk_forall(A, Fun({x, A}, Not(P(x))))},
Absurd(P(a), H, ForallElim(A, Fun({x, A}, Not(P(x))), H2, a))))));
});
io_state ios;
env->import("basic", ios);
}
}

10
src/library/basic_thms.h
View file

@ -48,10 +48,10 @@ expr mk_false_imp_any_fn();
/** \brief (Theorem) a : Bool |- false => a */
inline expr FalseImpAny(expr const & a) { return mk_app(mk_false_imp_any_fn(), a); }
expr mk_absurd_imp_any_fn();
expr mk_absurd_elim_fn();
/** \brief (Theorem) {a c : Bool}, H1 : a, H2 : Not(a) |- AbsurdImpAny(a, H1, H2) : c */
inline expr AbsurdImpAny(expr const & a, expr const & c, expr const & H1, expr const & H2) {
return mk_app(mk_absurd_imp_any_fn(), a, c, H1, H2);
inline expr AbsurdElim(expr const & a, expr const & c, expr const & H1, expr const & H2) {
return mk_app(mk_absurd_elim_fn(), a, c, H1, H2);
}
expr mk_eq_mp_fn();
@ -79,8 +79,8 @@ expr mk_conjunct2_fn();
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); }
/** \brief (Theorem) a : Bool, H : a, b : Bool |- Disj1(a, H, b) : Or(a, b) */
inline expr Disj1(expr const & a, expr const & H, expr const & b) { return mk_app(mk_disj1_fn(), a, H, b); }
expr mk_disj2_fn();
/** \brief (Theorem) {b} a : Bool, H : b |- Disj2(a, b, H) : Or(a, b) */

4
src/library/tactic/boolean_tactics.cpp
View file

@ -277,7 +277,7 @@ optional<proof_state_pair> disj_tactic(proof_state const & s, name gname) {
proof_builder pb = s.get_proof_builder();
proof_builder new_pb1 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
proof_map new_m(m);
new_m.insert(gname, Disj1(arg(*conclusion, 1), arg(*conclusion, 2), find(m, gname)));
new_m.insert(gname, Disj1(arg(*conclusion, 1), find(m, gname), arg(*conclusion, 2)));
return pb(new_m, a);
});
proof_builder new_pb2 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
@ -332,7 +332,7 @@ tactic absurd_tactic() {
if (is_not(p1.second, a)) {
for (auto const & p2 : g.get_hypotheses()) {
if (p2.second == a) {
expr pr = AbsurdImpAny(a, c, mk_constant(p2.first), mk_constant(p1.first));
expr pr = AbsurdElim(a, c, mk_constant(p2.first), mk_constant(p1.first));
proofs.emplace_front(gname, pr);
return optional<goal>(); // remove goal
}

235
src/shell/lean.cpp
View file

@ -18,6 +18,8 @@ Author: Leonardo de Moura
#include "util/lean_path.h"
#include "kernel/printer.h"
#include "kernel/environment.h"
#include "kernel/kernel_exception.h"
#include "kernel/formatter.h"
#include "library/io_state.h"
#include "library/kernel_bindings.h"
#include "frontends/lean/parser.h"
@ -88,6 +90,7 @@ static struct option g_long_options[] = {
{"lean", no_argument, 0, 'l'},
{"olean", no_argument, 0, 'b'},
{"lua", no_argument, 0, 'u'},
{"kernel", no_argument, 0, 'k'},
{"path", no_argument, 0, 'p'},
{"luahook", required_argument, 0, 'c'},
{"githash", no_argument, 0, 'g'},
@ -99,122 +102,132 @@ static struct option g_long_options[] = {
};
int main(int argc, char ** argv) {
lean::save_stack_info();
lean::register_modules();
bool export_objects = false;
std::string output;
input_kind default_k = input_kind::Lean; // default
while (true) {
int c = getopt_long(argc, argv, "lupgvhc:012s:012o:", g_long_options, NULL);
if (c == -1)
break; // end of command line
switch (c) {
case 'v':
display_header(std::cout);
return 0;
case 'g':
std::cout << g_githash << "\n";
return 0;
case 'h':
display_help(std::cout);
return 0;
case 'l':
default_k = input_kind::Lean;
break;
case 'u':
default_k = input_kind::Lua;
break;
case 'b':
default_k = input_kind::OLean;
break;
case 'c':
script_state::set_check_interrupt_freq(atoi(optarg));
break;
case 'p':
std::cout << lean::get_lean_path() << "\n";
return 0;
case 's':
lean::set_thread_stack_size(atoi(optarg)*1024);
break;
case 'o':
output = optarg;
export_objects = true;
break;
default:
std::cerr << "Unknown command line option\n";
display_help(std::cerr);
return 1;
try {
lean::save_stack_info();
lean::register_modules();
bool kernel_only = false;
bool export_objects = false;
std::string output;
input_kind default_k = input_kind::Lean; // default
while (true) {
int c = getopt_long(argc, argv, "klupgvhc:012s:012o:", g_long_options, NULL);
if (c == -1)
break; // end of command line
switch (c) {
case 'v':
display_header(std::cout);
return 0;
case 'g':
std::cout << g_githash << "\n";
return 0;
case 'h':
display_help(std::cout);
return 0;
case 'l':
default_k = input_kind::Lean;
break;
case 'u':
default_k = input_kind::Lua;
break;
case 'b':
default_k = input_kind::OLean;
break;
case 'c':
script_state::set_check_interrupt_freq(atoi(optarg));
break;
case 'p':
std::cout << lean::get_lean_path() << "\n";
return 0;
case 's':
lean::set_thread_stack_size(atoi(optarg)*1024);
break;
case 'k':
kernel_only = true;
break;
case 'o':
output = optarg;
export_objects = true;
break;
default:
std::cerr << "Unknown command line option\n";
display_help(std::cerr);
return 1;
}
}
}
if (optind >= argc) {
display_header(std::cout);
signal(SIGINT, on_ctrl_c);
if (default_k == input_kind::Lean) {
#if defined(LEAN_WINDOWS)
std::cout << "Type 'Exit.' to exit or 'Help.' for help."<< std::endl;
#else
std::cout << "Type Ctrl-D or 'Exit.' to exit or 'Help.' for help."<< std::endl;
#endif
if (optind >= argc) {
display_header(std::cout);
signal(SIGINT, on_ctrl_c);
if (default_k == input_kind::Lean) {
#if defined(LEAN_WINDOWS)
std::cout << "Type 'Exit.' to exit or 'Help.' for help."<< std::endl;
#else
std::cout << "Type Ctrl-D or 'Exit.' to exit or 'Help.' for help."<< std::endl;
#endif
environment env;
io_state ios;
init_frontend(env, ios, kernel_only);
script_state S;
shell sh(env, &S);
int status = sh() ? 0 : 1;
if (export_objects)
env->export_objects(output);
return status;
} else {
lean_assert(default_k == input_kind::Lua);
script_state S;
S.dostring(g_lua_repl);
}
} else {
environment env;
io_state ios;
init_frontend(env, ios);
io_state ios;
init_frontend(env, ios, kernel_only);
script_state S;
shell sh(env, &S);
int status = sh() ? 0 : 1;
bool ok = true;
for (int i = optind; i < argc; i++) {
char const * ext = get_file_extension(argv[i]);
input_kind k = default_k;
if (ext) {
if (strcmp(ext, "lean") == 0) {
k = input_kind::Lean;
} else if (strcmp(ext, "olean") == 0) {
k = input_kind::OLean;
} else if (strcmp(ext, "lua") == 0) {
k = input_kind::Lua;
}
}
if (k == input_kind::Lean) {
std::ifstream in(argv[i]);
if (in.bad() || in.fail()) {
std::cerr << "Failed to open file '" << argv[i] << "'\n";
return 1;
}
if (!parse_commands(env, ios, in, &S, false, false))
ok = false;
} else if (k == input_kind::OLean) {
try {
env->load(std::string(argv[i]), ios);
} catch (lean::exception & ex) {
std::cerr << "Failed to load binary file '" << argv[i] << "': " << ex.what() << "\n";
ok = false;
}
} else if (k == input_kind::Lua) {
try {
S.dofile(argv[i]);
} catch (lean::exception & ex) {
std::cerr << ex.what() << std::endl;
ok = false;
}
} else {
lean_unreachable(); // LCOV_EXCL_LINE
}
}
if (export_objects)
env->export_objects(output);
return status;
} else {
lean_assert(default_k == input_kind::Lua);
script_state S;
S.dostring(g_lua_repl);
return ok ? 0 : 1;
}
} else {
environment env;
io_state ios;
init_frontend(env, ios);
script_state S;
bool ok = true;
for (int i = optind; i < argc; i++) {
char const * ext = get_file_extension(argv[i]);
input_kind k = default_k;
if (ext) {
if (strcmp(ext, "lean") == 0) {
k = input_kind::Lean;
} else if (strcmp(ext, "olean") == 0) {
k = input_kind::OLean;
} else if (strcmp(ext, "lua") == 0) {
k = input_kind::Lua;
}
}
if (k == input_kind::Lean) {
std::ifstream in(argv[i]);
if (in.bad() || in.fail()) {
std::cerr << "Failed to open file '" << argv[i] << "'\n";
return 1;
}
if (!parse_commands(env, ios, in, &S, false, false))
ok = false;
} else if (k == input_kind::OLean) {
try {
env->load(std::string(argv[i]), ios);
} catch (lean::exception & ex) {
std::cerr << "Failed to load binary file '" << argv[i] << "': " << ex.what() << "\n";
ok = false;
}
} else if (k == input_kind::Lua) {
try {
S.dofile(argv[i]);
} catch (lean::exception & ex) {
std::cerr << ex.what() << std::endl;
ok = false;
}
} else {
lean_unreachable(); // LCOV_EXCL_LINE
}
}
if (export_objects)
env->export_objects(output);
return ok ? 0 : 1;
} catch (lean::kernel_exception & ex) {
std::cerr << "Error: " << ex.pp(lean::mk_simple_formatter(), lean::options()) << "\n";
} catch (lean::exception & ex) {
std::cerr << "Error: " << ex.what() << "\n";
}
}

3
src/tests/frontends/lean/CMakeLists.txt
View file

@ -1,12 +1,15 @@
add_executable(lean_frontend_tst frontend.cpp)
target_link_libraries(lean_frontend_tst ${EXTRA_LIBS})
add_test(lean_frontend ${CMAKE_CURRENT_BINARY_DIR}/lean_frontend_tst)
set_tests_properties(lean_frontend PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(lean_scanner scanner.cpp)
target_link_libraries(lean_scanner ${EXTRA_LIBS})
add_test(lean_scanner ${CMAKE_CURRENT_BINARY_DIR}/lean_scanner)
add_executable(lean_parser parser.cpp)
target_link_libraries(lean_parser ${EXTRA_LIBS})
add_test(lean_parser ${CMAKE_CURRENT_BINARY_DIR}/lean_parser)
set_tests_properties(lean_parser PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(lean_pp pp.cpp)
target_link_libraries(lean_pp ${EXTRA_LIBS})
add_test(lean_pp ${CMAKE_CURRENT_BINARY_DIR}/lean_pp)
set_tests_properties(lean_pp PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")

5
src/tests/kernel/CMakeLists.txt
View file

@ -4,9 +4,11 @@ add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr)
add_executable(normalizer normalizer.cpp)
target_link_libraries(normalizer ${EXTRA_LIBS})
add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer)
set_tests_properties(normalizer PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(threads threads.cpp)
target_link_libraries(threads ${EXTRA_LIBS})
add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads)
set_tests_properties(threads PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(free_vars free_vars.cpp)
target_link_libraries(free_vars ${EXTRA_LIBS})
add_test(free_vars ${CMAKE_CURRENT_BINARY_DIR}/free_vars)
@ -19,15 +21,18 @@ add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace)
add_executable(type_checker type_checker.cpp)
target_link_libraries(type_checker ${EXTRA_LIBS})
add_test(type_checker ${CMAKE_CURRENT_BINARY_DIR}/type_checker)
set_tests_properties(type_checker PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(environment environment.cpp)
target_link_libraries(environment ${EXTRA_LIBS})
add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment)
set_tests_properties(environment PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(occurs occurs.cpp)
target_link_libraries(occurs ${EXTRA_LIBS})
add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)
add_executable(metavar metavar.cpp)
target_link_libraries(metavar ${EXTRA_LIBS})
add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)
set_tests_properties(metavar PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(instantiate instantiate.cpp)
target_link_libraries(instantiate ${EXTRA_LIBS})
add_test(instantiate ${CMAKE_CURRENT_BINARY_DIR}/instantiate)

14
src/tests/kernel/environment.cpp
View file

@ -15,7 +15,7 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "kernel/printer.h"
#include "library/arith/arith.h"
#include "library/all/all.h"
#include "frontends/lean/frontend.h"
using namespace lean;
static void tst1() {
@ -63,7 +63,7 @@ static void tst2() {
static void tst3() {
std::cout << "tst3\n";
environment env = mk_toplevel();
environment env; init_frontend(env);
try {
env->add_definition("a", Int, Const("a"));
lean_unreachable();
@ -108,7 +108,7 @@ static void tst3() {
static void tst4() {
std::cout << "tst4\n";
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_definition("a", Int, iVal(1), true); // add opaque definition
expr t = iAdd(Const("a"), iVal(1));
std::cout << t << " --> " << normalize(t, env) << "\n";
@ -121,7 +121,7 @@ static void tst4() {
}
static void tst5() {
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_definition("a", Int, iVal(1), true); // add opaque definition
try {
std::cout << type_check(iAdd(Const("a"), Int), env) << "\n";
@ -132,7 +132,7 @@ static void tst5() {
}
static void tst6() {
environment env = mk_toplevel();
environment env; init_frontend(env);
level u = env->add_uvar("u", level() + 1);
level w = env->add_uvar("w", u + 1);
env->add_var("f", mk_arrow(Type(u), Type(u)));
@ -159,7 +159,7 @@ static void tst6() {
}
static void tst7() {
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("a", Int);
env->add_var("b", Int);
expr t = If(Int, True, Const("a"), Const("b"));
@ -207,7 +207,7 @@ static void tst9() {
static void tst10() {
environment env;
import_all(env);
init_frontend(env);
env->add_definition("a", Int, iVal(1));
lean_assert(env->get_object("a").get_weight() == 1);
expr a = Const("a");

6
src/tests/kernel/metavar.cpp
View file

@ -22,7 +22,7 @@ Author: Leonardo de Moura
#include "library/placeholder.h"
#include "library/io_state.h"
#include "library/arith/arith.h"
#include "library/all/all.h"
#include "frontends/lean/frontend.h"
using namespace lean;
static std::ostream & operator<<(std::ostream & out, metavar_env const & menv) {
@ -546,7 +546,7 @@ static void tst26() {
*/
std::cout << "\ntst26\n";
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
buffer<unification_constraint> up;
type_checker checker(env);
@ -588,7 +588,7 @@ static void tst27() {
*/
std::cout << "\ntst27\n";
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
buffer<unification_constraint> up;
type_checker checker(env);

14
src/tests/kernel/normalizer.cpp
View file

@ -19,7 +19,7 @@ Author: Leonardo de Moura
#include "kernel/metavar.h"
#include "library/deep_copy.h"
#include "library/arith/int.h"
#include "library/all/all.h"
#include "frontends/lean/frontend.h"
using namespace lean;
expr normalize(expr const & e) {
@ -190,7 +190,8 @@ static void tst2() {
}
static void tst3() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
env->add_var("a", Bool);
expr t1 = Const("a");
expr t2 = Const("a");
@ -217,7 +218,8 @@ static expr mk_big(unsigned depth) {
static void tst5() {
#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD)
expr t = mk_big(18);
environment env = mk_toplevel();
environment env;
init_frontend(env);
env->add_var("f", Bool >> (Bool >> Bool));
env->add_var("a", Bool);
normalizer proc(env);
@ -253,7 +255,7 @@ static void tst6() {
static void tst7() {
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
expr m1 = menv->mk_metavar();
expr x = Const("x");
@ -277,7 +279,7 @@ static void tst7() {
static void tst8() {
environment env;
import_all(env);
init_frontend(env);
env->add_var("P", Int >> (Int >> Bool));
expr P = Const("P");
expr v0 = Var(0);
@ -305,7 +307,7 @@ static void tst9() {
static void tst10() {
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
context ctx({{"x", Bool}, {"y", Bool}});
expr m = menv->mk_metavar(ctx);

4
src/tests/kernel/threads.cpp
View file

@ -14,7 +14,7 @@ Author: Leonardo de Moura
#include "library/max_sharing.h"
#include "library/deep_copy.h"
#include "library/arith/arith.h"
#include "library/all/all.h"
#include "frontends/lean/frontend.h"
using namespace lean;
expr norm(expr const & e, environment & env) {
@ -26,7 +26,7 @@ expr norm(expr const & e, environment & env) {
}
static void mk(expr const & a) {
environment env = mk_toplevel();
environment env; init_frontend(env);
expr b = Const("b");
for (unsigned i = 0; i < 100; i++) {
expr h = Const("h");

51
src/tests/kernel/type_checker.cpp
View file

@ -22,8 +22,8 @@ Author: Leonardo de Moura
#include "kernel/type_checker_justification.h"
#include "library/basic_thms.h"
#include "library/arith/arith.h"
#include "library/all/all.h"
#include "library/io_state.h"
#include "frontends/lean/frontend.h"
using namespace lean;
expr c(char const * n) { return mk_constant(n); }
@ -78,7 +78,8 @@ static void tst2() {
}
static void tst3() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
expr f = Fun("a", Bool, Eq(Const("a"), True));
std::cout << type_check(f, env) << "\n";
lean_assert(type_check(f, env) == mk_arrow(Bool, Bool));
@ -87,14 +88,16 @@ static void tst3() {
}
static void tst4() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
expr a = Eq(iVal(1), iVal(2));
expr pr = mk_lambda("x", a, Var(0));
std::cout << type_check(pr, env) << "\n";
}
static void tst5() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
env->add_var("P", Bool);
expr P = Const("P");
expr H = Const("H");
@ -111,7 +114,8 @@ static void tst5() {
}
static void tst6() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
expr A = Const("A");
expr f = Const("f");
expr x = Const("x");
@ -125,7 +129,8 @@ static void tst6() {
}
static void tst7() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
expr A = Const(name{"foo", "bla", "bla", "foo"});
expr f = Const("f");
expr x = Const("x");
@ -139,7 +144,8 @@ static void tst7() {
}
static void tst8() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
env->add_var("P", mk_arrow(Int, mk_arrow(Int, Bool)));
env->add_var("x", Int);
expr P = Const("P");
@ -158,7 +164,8 @@ static void tst8() {
}
static void tst9() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
env->add_var("P", mk_arrow(Int, mk_arrow(Int, Bool)));
env->add_var("x", Int);
expr P = Const("P");
@ -177,7 +184,8 @@ static void tst9() {
}
static void tst10() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
env->add_var("f", mk_arrow(Int, Int));
env->add_var("b", Int);
expr f = Const("f");
@ -193,7 +201,8 @@ static void tst10() {
}
static void tst11() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
env->add_var("f", Int >> (Int >> Int));
env->add_var("a", Int);
unsigned n = 1000;
@ -223,7 +232,8 @@ static expr mk_big(unsigned depth) {
static void tst12() {
#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD)
expr t = mk_big(18);
environment env = mk_toplevel();
environment env;
init_frontend(env);
env->add_var("f", Int >> (Int >> Int));
env->add_var("a", Int);
type_checker checker(env);
@ -245,7 +255,8 @@ static void tst12() {
}
static void tst13() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
env->add_var("f", Type() >> Type());
expr f = Const("f");
std::cout << type_check(f(Bool), env) << "\n";
@ -254,7 +265,7 @@ static void tst13() {
static void tst14() {
environment env;
import_all(env);
init_frontend(env);
expr f = Const("f");
expr a = Const("a");
env->add_var("f", Int >> Int);
@ -272,7 +283,7 @@ static void tst14() {
static void tst15() {
environment env;
import_all(env);
init_frontend(env);
context ctx1, ctx2;
expr A = Const("A");
expr vec1 = Const("vec1");
@ -340,7 +351,7 @@ static void f2(type_checker & tc, expr const & F) {
static void tst17() {
environment env;
import_all(env);
init_frontend(env);
type_checker tc(env);
expr A = Const("A");
expr F;
@ -363,7 +374,8 @@ static std::ostream & operator<<(std::ostream & out, buffer<unification_constrai
}
static void tst18() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
type_inferer type_of(env);
expr f = Const("f");
expr g = Const("g");
@ -394,7 +406,8 @@ static expr mk_big(unsigned val, unsigned depth) {
}
static void tst19() {
environment env = mk_toplevel();
environment env;
init_frontend(env);
type_inferer type_of(env);
type_checker type_of_slow(env);
expr t = mk_big(0, 10);
@ -416,7 +429,7 @@ static void tst19() {
static void tst20() {
environment env;
import_all(env);
init_frontend(env);
context ctx1, ctx2;
expr A = Const("A");
expr vec1 = Const("vec1");
@ -444,7 +457,7 @@ static void tst20() {
static void tst21() {
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
buffer<unification_constraint> uc;
type_inferer inferer(env);

1
src/tests/library/CMakeLists.txt
View file

@ -13,6 +13,7 @@ add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy)
add_executable(arith_tst arith.cpp)
target_link_libraries(arith_tst ${EXTRA_LIBS})
add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst)
set_tests_properties(arith_tst PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(update_expr update_expr.cpp)
target_link_libraries(update_expr ${EXTRA_LIBS})
add_test(update_expr ${CMAKE_CURRENT_BINARY_DIR}/update_expr)

14
src/tests/library/arith.cpp
View file

@ -11,13 +11,13 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h"
#include "kernel/abstract.h"
#include "library/arith/arith.h"
#include "library/all/all.h"
#include "frontends/lean/frontend.h"
using namespace lean;
static void tst0() {
environment env;
normalizer norm(env);
import_basic(env);
import_kernel(env);
import_arith(env);
env->add_var("n", Nat);
expr n = Const("n");
@ -48,7 +48,7 @@ static void tst0() {
static void tst1() {
environment env;
import_all(env);
init_frontend(env);
expr e = mk_int_value(mpz(10));
lean_assert(is_int_value(e));
lean_assert(type_check(e, env) == Int);
@ -57,7 +57,7 @@ static void tst1() {
static void tst2() {
environment env;
import_all(env);
init_frontend(env);
expr e = iAdd(iVal(10), iVal(30));
std::cout << e << "\n";
std::cout << normalize(e, env) << "\n";
@ -74,7 +74,7 @@ static void tst2() {
static void tst3() {
environment env;
import_all(env);
init_frontend(env);
expr e = iMul(iVal(10), iVal(30));
std::cout << e << "\n";
std::cout << normalize(e, env) << "\n";
@ -91,7 +91,7 @@ static void tst3() {
static void tst4() {
environment env;
import_all(env);
init_frontend(env);
expr e = iSub(iVal(10), iVal(30));
std::cout << e << "\n";
std::cout << normalize(e, env) << "\n";
@ -108,7 +108,7 @@ static void tst4() {
static void tst5() {
environment env;
import_all(env);
init_frontend(env);
env->add_var(name("a"), Int);
expr e = Eq(iVal(3), iVal(4));
std::cout << e << " --> " << normalize(e, env) << "\n";

1
src/tests/library/elaborator/CMakeLists.txt
View file

@ -1,3 +1,4 @@
add_executable(elaborator_tst elaborator.cpp)
target_link_libraries(elaborator_tst ${EXTRA_LIBS})
add_test(elaborator_tst ${CMAKE_CURRENT_BINARY_DIR}/elaborator_tst)
set_tests_properties(elaborator_tst PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")

58
src/tests/library/elaborator/elaborator.cpp
View file

@ -14,13 +14,13 @@ Author: Leonardo de Moura
#include "library/basic_thms.h"
#include "library/placeholder.h"
#include "library/arith/arith.h"
#include "library/all/all.h"
#include "library/elaborator/elaborator.h"
#include "frontends/lean/frontend.h"
using namespace lean;
static void tst1() {
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
@ -75,7 +75,7 @@ static void tst2() {
?m4 in { Id, nat2int, nat2real }
*/
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
@ -116,7 +116,7 @@ static void tst3() {
?m5 in { Id, int2real }
*/
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
@ -158,7 +158,7 @@ static void tst4() {
?m6 in { Id, int2real }
*/
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
@ -202,7 +202,7 @@ static void tst5() {
?m4 in { Id, int2real }
*/
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
@ -239,7 +239,7 @@ static void tst6() {
Theorem T : (f a (f b b)) == a := Subst _ _ _ _ H1 H2
*/
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
@ -307,7 +307,7 @@ static void unsolved(expr const & e, environment const & env) {
static void tst7() {
std::cout << "\nTST 7\n";
environment env;
import_all(env);
init_frontend(env);
expr A = Const("A");
expr B = Const("B");
expr F = Const("F");
@ -328,7 +328,7 @@ static void tst7() {
static void tst8() {
std::cout << "\nTST 8\n";
environment env;
import_all(env);
init_frontend(env);
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
@ -354,7 +354,7 @@ static void tst8() {
static void tst9() {
std::cout << "\nTST 9\n";
environment env;
import_all(env);
init_frontend(env);
expr Nat = Const("N");
env->add_var("N", Type());
env->add_var("vec", Nat >> Type());
@ -386,7 +386,7 @@ static void tst9() {
static void tst10() {
std::cout << "\nTST 10\n";
environment env;
import_all(env);
init_frontend(env);
expr Nat = Const("N");
env->add_var("N", Type());
expr R = Const("R");
@ -410,7 +410,7 @@ static void tst10() {
static void tst11() {
std::cout << "\nTST 11\n";
environment env;
import_all(env);
init_frontend(env);
expr A = Const("A");
expr B = Const("B");
expr a = Const("a");
@ -428,7 +428,7 @@ static void tst11() {
static void tst12() {
std::cout << "\nTST 12\n";
environment env;
import_all(env);
init_frontend(env);
expr lst = Const("list");
expr nil = Const("nil");
expr cons = Const("cons");
@ -449,7 +449,7 @@ static void tst12() {
static void tst13() {
std::cout << "\nTST 13\n";
environment env;
import_all(env);
init_frontend(env);
expr B = Const("B");
expr A = Const("A");
expr x = Const("x");
@ -472,7 +472,7 @@ static void tst13() {
static void tst14() {
std::cout << "\nTST 14\n";
environment env;
import_all(env);
init_frontend(env);
expr A = Const("A");
expr B = Const("B");
expr f = Const("f");
@ -513,7 +513,7 @@ static void tst14() {
static void tst15() {
std::cout << "\nTST 15\n";
environment env;
import_all(env);
init_frontend(env);
expr A = Const("A");
expr B = Const("B");
expr C = Const("C");
@ -539,7 +539,7 @@ static void tst15() {
static void tst16() {
std::cout << "\nTST 16\n";
environment env;
import_all(env);
init_frontend(env);
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
@ -560,7 +560,7 @@ static void tst16() {
EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3))),
env);
environment env2;
import_all(env2);
init_frontend(env2);
success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3))),
Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
@ -577,7 +577,7 @@ static void tst16() {
void tst17() {
std::cout << "\nTST 17\n";
environment env;
import_all(env);
init_frontend(env);
expr A = Const("A");
expr B = Const("B");
expr a = Const("a");
@ -592,7 +592,7 @@ void tst17() {
void tst18() {
std::cout << "\nTST 18\n";
environment env;
import_all(env);
init_frontend(env);
expr A = Const("A");
expr h = Const("h");
expr f = Const("f");
@ -606,7 +606,7 @@ void tst18() {
void tst19() {
std::cout << "\nTST 19\n";
environment env;
import_all(env);
init_frontend(env);
expr R = Const("R");
expr A = Const("A");
expr r = Const("r");
@ -633,7 +633,7 @@ void tst19() {
void tst20() {
std::cout << "\nTST 20\n";
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
expr N = Const("N1");
expr M = Const("M1");
@ -666,7 +666,7 @@ void tst20() {
void tst21() {
std::cout << "\nTST 21\n";
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
expr N = Const("N");
expr M = Const("M");
@ -698,7 +698,7 @@ void tst21() {
void tst22() {
std::cout << "\nTST 22\n";
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
expr N = Const("N");
env->add_var("N", Type());
@ -733,7 +733,7 @@ void tst22() {
void tst23() {
std::cout << "\nTST 23\n";
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
expr N = Const("N");
env->add_var("N", Type());
@ -763,7 +763,7 @@ void tst23() {
void tst24() {
std::cout << "\nTST 24\n";
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
expr N = Const("N");
env->add_var("N", Type());
@ -783,7 +783,7 @@ void tst24() {
void tst25() {
std::cout << "\nTST 25\n";
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
expr N = Const("N");
env->add_var("N", Type());
@ -819,7 +819,7 @@ void tst26() {
Axiom H : g _ a = a
*/
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);
@ -849,7 +849,7 @@ void tst27() {
fun f : _, eq _ ((g _ f) a) a
*/
environment env;
import_all(env);
init_frontend(env);
metavar_env menv;
buffer<unification_constraint> ucs;
type_checker checker(env);

1
src/tests/library/rewriter/CMakeLists.txt
View file

@ -1,6 +1,7 @@
add_executable(rewriter_tst rewriter.cpp)
target_link_libraries(rewriter_tst ${EXTRA_LIBS})
add_test(rewriter_tst ${CMAKE_CURRENT_BINARY_DIR}/rewriter_tst)
set_tests_properties(rewriter_tst PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(fo_match_tst fo_match.cpp)
target_link_libraries(fo_match_tst ${EXTRA_LIBS})

29
src/tests/library/rewriter/rewriter.cpp
View file

@ -17,6 +17,7 @@ Author: Soonho Kong
#include "library/rewriter/fo_match.h"
#include "library/rewriter/rewriter.h"
#include "library/basic_thms.h"
#include "frontends/lean/frontend.h"
using namespace lean;
using std::cout;
@ -37,7 +38,7 @@ static void theorem_rewriter1_tst() {
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("a", Nat);
env->add_var("b", Nat);
env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z
@ -69,7 +70,7 @@ static void theorem_rewriter2_tst() {
Eq(nAdd(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("a", Nat);
env->add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0
@ -107,7 +108,7 @@ static void then_rewriter1_tst() {
Eq(nAdd(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("a", Nat);
env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z
env->add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0
@ -163,7 +164,7 @@ static void then_rewriter2_tst() {
Eq(nAdd(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("a", Nat);
env->add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z
env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z
@ -222,7 +223,7 @@ static void orelse_rewriter1_tst() {
Eq(nAdd(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("a", Nat);
env->add_var("b", Nat);
env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z
@ -269,7 +270,7 @@ static void orelse_rewriter2_tst() {
Eq(nAdd(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("a", Nat);
env->add_var("b", Nat);
env->add_axiom("ADD_ASSOC", add_assoc_thm_type);
@ -318,7 +319,7 @@ static void try_rewriter1_tst() {
Eq(nAdd(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("a", Nat);
env->add_var("b", Nat);
env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z
@ -369,7 +370,7 @@ static void try_rewriter2_tst() {
Eq(nAdd(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("a", Nat);
env->add_var("b", Nat);
env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z
@ -415,7 +416,7 @@ static void app_rewriter1_tst() {
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("f1", Nat >> Nat);
env->add_var("f2", Nat >> (Nat >> Nat));
env->add_var("f3", Nat >> (Nat >> (Nat >> Nat)));
@ -505,7 +506,7 @@ static void repeat_rewriter1_tst() {
Eq(nAdd(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("a", Nat);
env->add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z
env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z
@ -563,7 +564,7 @@ static void repeat_rewriter2_tst() {
Eq(nAdd(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("a", Nat);
env->add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z
env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z
@ -610,7 +611,7 @@ static void depth_rewriter1_tst() {
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("f1", Nat >> Nat);
env->add_var("f2", Nat >> (Nat >> Nat));
env->add_var("f3", Nat >> (Nat >> (Nat >> Nat)));
@ -657,7 +658,7 @@ static void lambda_body_rewriter_tst() {
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
environment env = mk_toplevel();
environment env; init_frontend(env);
env->add_var("f1", Nat >> Nat);
env->add_var("f2", Nat >> (Nat >> Nat));
env->add_var("f3", Nat >> (Nat >> (Nat >> Nat)));
@ -702,7 +703,7 @@ static void lambda_type_rewriter_tst() {
// Result : fun (x : vec(Nat, b + a)), x
cout << "=== lambda_type_rewriter_tst() ===" << std::endl;
context ctx;
environment env = mk_toplevel();
environment env; init_frontend(env);
expr a = Const("a"); // a : Nat
env->add_var("a", Nat);
expr b = Const("b"); // b : Nat

1
src/tests/library/tactic/CMakeLists.txt
View file

@ -1,3 +1,4 @@
add_executable(tactic_tst tactic.cpp)
target_link_libraries(tactic_tst ${EXTRA_LIBS})
add_test(tactic ${CMAKE_CURRENT_BINARY_DIR}/tactic_tst)
set_tests_properties(tactic PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")

6
src/tests/library/tactic/tactic.cpp
View file

@ -9,12 +9,12 @@ Author: Leonardo de Moura
#include "util/interrupt.h"
#include "kernel/builtin.h"
#include "kernel/kernel_exception.h"
#include "library/all/all.h"
#include "library/tactic/goal.h"
#include "library/tactic/proof_builder.h"
#include "library/tactic/proof_state.h"
#include "library/tactic/tactic.h"
#include "library/tactic/boolean_tactics.h"
#include "frontends/lean/frontend.h"
using namespace lean;
tactic loop_tactic() {
@ -49,7 +49,7 @@ static void check_failure(tactic t, ro_environment const & env, io_state const &
static void tst1() {
environment env;
io_state io(options(), mk_simple_formatter());
import_all(env);
init_frontend(env);
env->add_var("p", Bool);
env->add_var("q", Bool);
expr p = Const("p");
@ -115,7 +115,7 @@ static void tst1() {
static void tst2() {
environment env;
io_state io(options(), mk_simple_formatter());
import_all(env);
init_frontend(env);
env->add_var("p", Bool);
env->add_var("q", Bool);
env->add_var("r", Bool);

16
tests/lean/bug.lean.expected.out
View file

@ -5,13 +5,15 @@ A : (Type U), A' : (Type U), H : A == A' ⊢
(?M::3 ≈ (Type U)) ⊕ (?M::3 ≈ (Type M)) ⊕ (?M::3 ≈ (Type 1)) ⊕ (?M::3 ≈ Type) ⊕ (?M::3 ≈ Bool)
Destruct/Decompose
A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ (Type U)
(line: 1: pos: 44) Type of argument 1 must be convertible to the expected type in the application of
@Symm
with arguments:
?M::0
?M::1
?M::2
H
Normalize
A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ TypeU
(line: 1: pos: 44) Type of argument 1 must be convertible to the expected type in the application of
@Symm
with arguments:
?M::0
?M::1
?M::2
H
Failed to solve
A : (Type U), A' : (Type U), H : A == A' ⊢ (?M::5 ≈ (Type U)) ⊕ (?M::5 ≈ (Type U+1))
Destruct/Decompose

1
tests/lean/cast4.lean
View file

@ -2,7 +2,6 @@ Import cast
SetOption pp::colors false
Definition TypeM := (Type M)
Definition TypeU := (Type U)
Check fun (A A': TypeM)
(B : A -> TypeM)

1
tests/lean/cast4.lean.expected.out
View file

@ -3,7 +3,6 @@
Imported 'cast'
Set: pp::colors
Defined: TypeM
Defined: TypeU
λ (A A' : TypeM)
(B : A → TypeM)
(B' : A' → TypeM)

2
tests/lean/disj1.lean.expected.out
View file

@ -4,4 +4,4 @@
Proved: T1
Proved: T2
Theorem T2 (a b : Bool) : a ∨ b ⇒ b ∨ a :=
Discharge (λ H : a ∨ b, DisjCases H (λ H : a, Disj2 b H) (λ H : b, Disj1 a H))
Discharge (λ H : a ∨ b, DisjCases H (λ H : a, Disj2 b H) (λ H : b, Disj1 H a))

1
tests/lean/elab4.lean.expected.out
View file

@ -5,6 +5,7 @@
Assumed: R
Proved: R2
Set: lean::pp::implicit
Import "basic"
Variable C {A B : Type} (H : @eq Type A B) (a : A) : B
Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) :
@eq Type A A'

1
tests/lean/elab5.lean.expected.out
View file

@ -5,6 +5,7 @@
Assumed: R
Proved: R2
Set: lean::pp::implicit
Import "basic"
Variable C {A B : Type} (H : @eq Type A B) (a : A) : B
Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) :
@eq Type A A'

7
tests/lean/find.lean.expected.out
View file

@ -1,8 +1,7 @@
Set: pp::colors
Set: pp::unicode
Theorem Congr1 {A : (Type U)} {B : A → (Type U)} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a
Theorem Congr2 {A : (Type U)} {B : A → (Type U)} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b
Theorem Congr {A : (Type U)} {B : A → (Type U)} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) :
f a == g b
Theorem Congr1 {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a
Theorem Congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b
Theorem Congr {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b
Error (line: 3, pos: 0) executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression 'foo'
Error (line: 4, pos: 0) executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:18), unfinished capture

1
tests/lean/norm_bug1.lean
View file

@ -2,7 +2,6 @@ Import cast
SetOption pp::colors false
Definition TypeM := (Type M)
Definition TypeU := (Type U)
Check fun (A A': TypeM)
(a : A)

1
tests/lean/norm_bug1.lean.expected.out
View file

@ -3,7 +3,6 @@
Imported 'cast'
Set: pp::colors
Defined: TypeM
Defined: TypeU
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 :
Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
λ (A A' : TypeM)

3
tests/lean/tactic10.lean.expected.out
View file

@ -6,5 +6,4 @@
Defined: h
Proved: T2
Theorem T2 (a b : Bool) : h a b ⇒ f b ⇒ a :=
Discharge
(λ H : a ∨ b, Discharge (λ H::1 : ¬ b, DisjCases H (λ H : a, H) (λ H : b, AbsurdImpAny b a H H::1)))
Discharge (λ H : a ∨ b, Discharge (λ H::1 : ¬ b, DisjCases H (λ H : a, H) (λ H : b, AbsurdElim a H H::1)))

3
tests/lean/tactic8.lean.expected.out
View file

@ -2,5 +2,4 @@
Set: pp::unicode
Proved: T
Theorem T (a b : Bool) : a ∨ b ⇒ ¬ b ⇒ a :=
Discharge
(λ H : a ∨ b, Discharge (λ H::1 : ¬ b, DisjCases H (λ H : a, H) (λ H : b, AbsurdImpAny b a H H::1)))
Discharge (λ H : a ∨ b, Discharge (λ H::1 : ¬ b, DisjCases H (λ H : a, H) (λ H : b, AbsurdElim a H H::1)))

2
tests/lean/tactic9.lean.expected.out
View file

@ -3,4 +3,4 @@
Defined: f
Proved: T
Theorem T (a b : Bool) : a ∨ b ⇒ f b ⇒ a :=
Discharge (λ H : a ∨ b, Discharge (λ H::1 : f b, DisjCases H (λ H : a, H) (λ H : b, AbsurdImpAny b a H H::1)))
Discharge (λ H : a ∨ b, Discharge (λ H::1 : f b, DisjCases H (λ H : a, H) (λ H : b, AbsurdElim a H H::1)))

2
tests/lean/tst4.lean.expected.out
View file

@ -10,7 +10,7 @@
Assumed: EqNice
@EqNice N n1 n2
@f N n1 n2 : N
@Congr : Π (A : (Type U)) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), f == g → a == b → f a == g b
@Congr : Π (A : TypeU) (B : A → TypeU) (f g : Π x : A, B x) (a b : A), f == g → a == b → f a == g b
@f N n1 n2
Assumed: a
Assumed: b

1
tests/lean/type_inf_bug1.lean
View file

@ -2,7 +2,6 @@ Import cast
SetOption pp::colors false
Definition TypeM := (Type M)
Definition TypeU := (Type U)
Check fun (A A': TypeM)
(a : A)

1
tests/lean/type_inf_bug1.lean.expected.out
View file

@ -3,7 +3,6 @@
Imported 'cast'
Set: pp::colors
Defined: TypeM
Defined: TypeU
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 :
Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
λ (A A' : TypeM)