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

refactor(builtin): remove old library, we will build a new one for Lean 0.2

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-15 15:56:28 -07:00
parent c6af56260e
commit 391b2fe739
39 changed files with 0 additions and 3796 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/CMakeLists.txt
View file

@ -237,7 +237,6 @@ endif()
set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage") set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")
set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS}) set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS})
add_subdirectory(shell) add_subdirectory(shell)
# add_subdirectory(builtin)
add_subdirectory(emacs) add_subdirectory(emacs)
add_subdirectory(tests/util) add_subdirectory(tests/util)

104
src/builtin/CMakeLists.txt
View file

@ -1,104 +0,0 @@
# This directory contains Lean builtin libraries and Lua scripts
# needed to run Lean. The builtin Lean libraries are compiled
# using ${LEAN_BINARY_DIR}/shell/lean
# The library builtin is not a real library.
# It is just a hack to force CMake to consider our custom targets
add_library(builtin builtin.cpp)
# We copy files to the shell directory, to make sure we can test lean
# without installing it.
set(SHELL_DIR ${LEAN_BINARY_DIR}/shell)
file(GLOB LEANLIB "*.lua")
FOREACH(FILE ${LEANLIB})
get_filename_component(FNAME ${FILE} NAME)
add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
COMMAND ${CMAKE_COMMAND} -E copy ${FILE} ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
COMMAND ${CMAKE_COMMAND} -E copy ${FILE} ${SHELL_DIR}/${FNAME}
DEPENDS ${FILE})
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)
# The following command invokes the lean binary.
# So, it CANNOT be executed if we are cross-compiling.
function(add_theory_core FILE ARG)
set(EXTRA_DEPS ${ARGN})
get_filename_component(BASENAME ${FILE} NAME_WE)
set(FNAME "${BASENAME}.olean")
add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
COMMAND ${SHELL_DIR}/lean.sh ${ARG} -q -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE}
COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${SHELL_DIR}/${FNAME}
COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/obj/${FNAME}
DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} lean_sh ${EXTRA_DEPS})
add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${EXTRA_DEPS})
add_dependencies(builtin ${BASENAME}_builtin)
install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
add_test("${BASENAME}_builtin_test" ${SHELL_DIR}/lean -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}_test ${ARG} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE})
endfunction()
# When cross compiling, we cannot execute lean during the build.
# So, we just copy the precompiled .olean files.
function(copy_olean FILE)
get_filename_component(BASENAME ${FILE} NAME_WE)
set(FNAME "${BASENAME}.olean")
add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_SOURCE_DIR}/obj/${FNAME} ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_SOURCE_DIR}/obj/${FNAME} ${SHELL_DIR}/${FNAME}
DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/obj/${FNAME})
add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME})
add_dependencies(builtin ${BASENAME}_builtin)
install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
endfunction()
function(add_kernel_theory FILE)
if(CMAKE_CROSSCOMPILING)
copy_olean(${FILE})
else()
add_theory_core(${FILE} "-n" ${ARGN})
endif()
endfunction()
function(add_theory FILE)
if(CMAKE_CROSSCOMPILING)
copy_olean(${FILE})
else()
add_theory_core(${FILE} "" ${ARGN})
endif()
endfunction()
# The following command invokes the lean binary to update .cpp/.h interface files
# associated with a .lean file.
function(update_interface FILE DEST ARG)
get_filename_component(BASENAME ${FILE} NAME_WE)
set(CPPFILE "${LEAN_SOURCE_DIR}/${DEST}/${BASENAME}_decls.cpp")
set(HFILE "${LEAN_SOURCE_DIR}/${DEST}/${BASENAME}_decls.h")
# We also create a fake .h file, it serves as the output for the following
# custom command. We don't use CPPFILE and HFILE as the output to avoid
# a cyclic dependency.
set(HFILE_fake "${LEAN_BINARY_DIR}/${DEST}/${BASENAME}_fake.h")
add_custom_command(OUTPUT ${HFILE_fake}
COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/lean2cpp.sh "${SHELL_DIR}/lean.sh" "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}/${FILE}" "${CPPFILE}" "${ARG}$"
COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/lean2h.sh "${SHELL_DIR}/lean.sh" "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}/${FILE}" "${HFILE}" "${ARG}$"
COMMAND ${CMAKE_COMMAND} -E copy ${HFILE} ${HFILE_fake}
DEPENDS ${FILE} lean_sh)
add_custom_target("${BASENAME}_decls" DEPENDS ${HFILE_fake})
add_dependencies(builtin ${BASENAME}_decls)
endfunction()
add_kernel_theory("kernel.lean" ${CMAKE_CURRENT_BINARY_DIR}/macros.lua ${CMAKE_CURRENT_BINARY_DIR}/tactic.lua)
add_kernel_theory("Nat.lean" ${CMAKE_CURRENT_BINARY_DIR}/kernel.olean)
add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
add_theory("subtype.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
add_theory("optional.lean" "${CMAKE_CURRENT_BINARY_DIR}/subtype.olean")
add_theory("sum.lean" "${CMAKE_CURRENT_BINARY_DIR}/optional.olean")
add_theory("num.lean" "${CMAKE_CURRENT_BINARY_DIR}/subtype.olean")
update_interface("kernel.olean" "kernel" "-n")
update_interface("Nat.olean" "library/arith" "-n")
update_interface("Int.olean" "library/arith" "")
update_interface("Real.olean" "library/arith" "")

68
src/builtin/Int.lean
View file

@ -1,68 +0,0 @@
import Nat
variable Int : Type
alias ℤ : Int
builtin nat_to_int : Nat → Int
coercion nat_to_int
namespace Int
builtin numeral
builtin add : Int → Int → Int
infixl 65 + : add
builtin mul : Int → Int → Int
infixl 70 * : mul
builtin div : Int → Int → Int
infixl 70 div : div
builtin le : Int → Int → Bool
infix 50 <= : le
infix 50 ≤ : le
definition ge (a b : Int) : Bool := b ≤ a
infix 50 >= : ge
infix 50 ≥ : ge
definition lt (a b : Int) : Bool := ¬ (a ≥ b)
infix 50 < : lt
definition gt (a b : Int) : Bool := ¬ (a ≤ b)
infix 50 > : gt
definition sub (a b : Int) : Int := a + -1 * b
infixl 65 - : sub
definition neg (a : Int) : Int := -1 * a
notation 75 - _ : neg
definition mod (a b : Int) : Int := a - b * (a div b)
infixl 70 mod : mod
definition divides (a b : Int) : Bool := (b mod a) = 0
infix 50 | : divides
definition abs (a : Int) : Int := if (0 ≤ a) then a else (- a)
notation 55 | _ | : abs
set_opaque sub true
set_opaque neg true
set_opaque mod true
set_opaque divides true
set_opaque abs true
set_opaque ge true
set_opaque lt true
set_opaque gt true
end
namespace Nat
definition sub (a b : Nat) : Int := nat_to_int a - nat_to_int b
infixl 65 - : sub
definition neg (a : Nat) : Int := - (nat_to_int a)
notation 75 - _ : neg
set_opaque sub true
set_opaque neg true
end

361
src/builtin/Nat.lean
View file

@ -1,361 +0,0 @@
import kernel
import macros
variable Nat : Type
alias ℕ : Nat
namespace Nat
builtin numeral
builtin add : Nat → Nat → Nat
infixl 65 + : add
builtin mul : Nat → Nat → Nat
infixl 70 * : mul
builtin le : Nat → Nat → Bool
infix 50 <= : le
infix 50 ≤ : le
definition ge (a b : Nat) := b ≤ a
infix 50 >= : ge
infix 50 ≥ : ge
definition lt (a b : Nat) := a + 1 ≤ b
infix 50 < : lt
definition gt (a b : Nat) := b < a
infix 50 > : gt
definition id (a : Nat) := a
notation 55 | _ | : id
axiom succ_nz (a : Nat) : a + 1 ≠ 0
axiom succ_inj {a b : Nat} (H : a + 1 = b + 1) : a = b
axiom add_zeror (a : Nat) : a + 0 = a
axiom add_succr (a b : Nat) : a + (b + 1) = (a + b) + 1
axiom mul_zeror (a : Nat) : a * 0 = 0
axiom mul_succr (a b : Nat) : a * (b + 1) = a * b + a
axiom le_def (a b : Nat) : a ≤ b ↔ ∃ c, a + c = b
axiom induction {P : Nat → Bool} (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : ∀ a, P a
theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a
:= induction H1 H2 a
theorem pred_nz {a : Nat} : a ≠ 0 → ∃ b, b + 1 = a
:= induction_on a
(λ H : 0 ≠ 0, false_elim (∃ b, b + 1 = 0) (a_neq_a_elim H))
(λ (n : Nat) (iH : n ≠ 0 → ∃ b, b + 1 = n) (H : n + 1 ≠ 0),
or_elim (em (n = 0))
(λ Heq0 : n = 0, exists_intro 0 (calc 0 + 1 = n + 1 : { symm Heq0 }))
(λ Hne0 : n ≠ 0,
obtain (w : Nat) (Hw : w + 1 = n), from (iH Hne0),
exists_intro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw })))
theorem discriminate {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : ∀ n, a = n + 1 → B) : B
:= or_elim (em (a = 0))
(λ Heq0 : a = 0, H1 Heq0)
(λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (pred_nz Hne0),
H2 w (symm Hw))
theorem add_zerol (a : Nat) : 0 + a = a
:= induction_on a
(show 0 + 0 = 0, from add_zeror 0)
(λ (n : Nat) (iH : 0 + n = n),
calc 0 + (n + 1) = (0 + n) + 1 : add_succr 0 n
... = n + 1 : { iH })
theorem add_succl (a b : Nat) : (a + 1) + b = (a + b) + 1
:= induction_on b
(calc (a + 1) + 0 = a + 1 : add_zeror (a + 1)
... = (a + 0) + 1 : { symm (add_zeror a) })
(λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1),
calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : add_succr (a + 1) n
... = ((a + n) + 1) + 1 : { iH }
... = (a + (n + 1)) + 1 : { show (a + n) + 1 = a + (n + 1), from symm (add_succr a n) })
theorem add_comm (a b : Nat) : a + b = b + a
:= induction_on b
(calc a + 0 = a : add_zeror a
... = 0 + a : symm (add_zerol a))
(λ (n : Nat) (iH : a + n = n + a),
calc a + (n + 1) = (a + n) + 1 : add_succr a n
... = (n + a) + 1 : { iH }
... = (n + 1) + a : symm (add_succl n a))
theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c)
:= symm (induction_on a
(calc 0 + (b + c) = b + c : add_zerol (b + c)
... = (0 + b) + c : { symm (add_zerol b) })
(λ (n : Nat) (iH : n + (b + c) = (n + b) + c),
calc (n + 1) + (b + c) = (n + (b + c)) + 1 : add_succl n (b + c)
... = ((n + b) + c) + 1 : { iH }
... = ((n + b) + 1) + c : symm (add_succl (n + b) c)
... = ((n + 1) + b) + c : { show (n + b) + 1 = (n + 1) + b, from symm (add_succl n b) }))
theorem mul_zerol (a : Nat) : 0 * a = 0
:= induction_on a
(show 0 * 0 = 0, from mul_zeror 0)
(λ (n : Nat) (iH : 0 * n = 0),
calc 0 * (n + 1) = (0 * n) + 0 : mul_succr 0 n
... = 0 + 0 : { iH }
... = 0 : add_zerol 0)
theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b
:= induction_on b
(calc (a + 1) * 0 = 0 : mul_zeror (a + 1)
... = a * 0 : symm (mul_zeror a)
... = a * 0 + 0 : symm (add_zeror (a * 0)))
(λ (n : Nat) (iH : (a + 1) * n = a * n + n),
calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : mul_succr (a + 1) n
... = a * n + n + (a + 1) : { iH }
... = a * n + n + a + 1 : symm (add_assoc (a * n + n) a 1)
... = a * n + (n + a) + 1 : { show a * n + n + a = a * n + (n + a),
from add_assoc (a * n) n a }
... = a * n + (a + n) + 1 : { add_comm n a }
... = a * n + a + n + 1 : { symm (add_assoc (a * n) a n) }
... = a * (n + 1) + n + 1 : { symm (mul_succr a n) }
... = a * (n + 1) + (n + 1) : add_assoc (a * (n + 1)) n 1)
theorem mul_onel (a : Nat) : 1 * a = a
:= induction_on a
(show 1 * 0 = 0, from mul_zeror 1)
(λ (n : Nat) (iH : 1 * n = n),
calc 1 * (n + 1) = 1 * n + 1 : mul_succr 1 n
... = n + 1 : { iH })
theorem mul_oner (a : Nat) : a * 1 = a
:= induction_on a
(show 0 * 1 = 0, from mul_zeror 1)
(λ (n : Nat) (iH : n * 1 = n),
calc (n + 1) * 1 = n * 1 + 1 : mul_succl n 1
... = n + 1 : { iH })
theorem mul_comm (a b : Nat) : a * b = b * a
:= induction_on b
(calc a * 0 = 0 : mul_zeror a
... = 0 * a : symm (mul_zerol a))
(λ (n : Nat) (iH : a * n = n * a),
calc a * (n + 1) = a * n + a : mul_succr a n
... = n * a + a : { iH }
... = (n + 1) * a : symm (mul_succl n a))
theorem distributer (a b c : Nat) : a * (b + c) = a * b + a * c
:= induction_on a
(calc 0 * (b + c) = 0 : mul_zerol (b + c)
... = 0 + 0 : add_zeror 0
... = 0 * b + 0 : { symm (mul_zerol b) }
... = 0 * b + 0 * c : { symm (mul_zerol c) })
(λ (n : Nat) (iH : n * (b + c) = n * b + n * c),
calc (n + 1) * (b + c) = n * (b + c) + (b + c) : mul_succl n (b + c)
... = n * b + n * c + (b + c) : { iH }
... = n * b + n * c + b + c : symm (add_assoc (n * b + n * c) b c)
... = n * b + (n * c + b) + c : { add_assoc (n * b) (n * c) b }
... = n * b + (b + n * c) + c : { add_comm (n * c) b }
... = n * b + b + n * c + c : { symm (add_assoc (n * b) b (n * c)) }
... = (n + 1) * b + n * c + c : { symm (mul_succl n b) }
... = (n + 1) * b + (n * c + c) : add_assoc ((n + 1) * b) (n * c) c
... = (n + 1) * b + (n + 1) * c : { symm (mul_succl n c) })
theorem distributel (a b c : Nat) : (a + b) * c = a * c + b * c
:= calc (a + b) * c = c * (a + b) : mul_comm (a + b) c
... = c * a + c * b : distributer c a b
... = a * c + c * b : { mul_comm c a }
... = a * c + b * c : { mul_comm c b }
theorem mul_assoc (a b c : Nat) : (a * b) * c = a * (b * c)
:= symm (induction_on a
(calc 0 * (b * c) = 0 : mul_zerol (b * c)
... = 0 * c : symm (mul_zerol c)
... = (0 * b) * c : { symm (mul_zerol b) })
(λ (n : Nat) (iH : n * (b * c) = n * b * c),
calc (n + 1) * (b * c) = n * (b * c) + (b * c) : mul_succl n (b * c)
... = n * b * c + (b * c) : { iH }
... = (n * b + b) * c : symm (distributel (n * b) b c)
... = (n + 1) * b * c : { symm (mul_succl n b) }))
theorem add_left_comm (a b c : Nat) : a + (b + c) = b + (a + c)
:= left_comm add_comm add_assoc a b c
theorem mul_left_comm (a b c : Nat) : a * (b * c) = b * (a * c)
:= left_comm mul_comm mul_assoc a b c
theorem add_injr {a b c : Nat} : a + b = a + c → b = c
:= induction_on a
(λ H : 0 + b = 0 + c,
calc b = 0 + b : symm (add_zerol b)
... = 0 + c : H
... = c : add_zerol c)
(λ (n : Nat) (iH : n + b = n + c → b = c) (H : n + 1 + b = n + 1 + c),
let L1 : n + b + 1 = n + c + 1
:= (calc n + b + 1 = n + (b + 1) : add_assoc n b 1
... = n + (1 + b) : { add_comm b 1 }
... = n + 1 + b : symm (add_assoc n 1 b)
... = n + 1 + c : H
... = n + (1 + c) : add_assoc n 1 c
... = n + (c + 1) : { add_comm 1 c }
... = n + c + 1 : symm (add_assoc n c 1)),
L2 : n + b = n + c := succ_inj L1
in iH L2)
theorem add_injl {a b c : Nat} (H : a + b = c + b) : a = c
:= add_injr (calc b + a = a + b : add_comm _ _
... = c + b : H
... = b + c : add_comm _ _)
theorem add_eqz {a b : Nat} (H : a + b = 0) : a = 0
:= discriminate
(λ H1 : a = 0, H1)
(λ (n : Nat) (H1 : a = n + 1),
absurd_elim (a = 0)
H (calc a + b = n + 1 + b : { H1 }
... = n + (1 + b) : add_assoc n 1 b
... = n + (b + 1) : { add_comm 1 b }
... = n + b + 1 : symm (add_assoc n b 1)
... ≠ 0 : succ_nz (n + b)))
theorem le_intro {a b c : Nat} (H : a + c = b) : a ≤ b
:= (symm (le_def a b)) ◂ (show (∃ x, a + x = b), from exists_intro c H)
theorem le_elim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b
:= (le_def a b) ◂ H
theorem le_refl (a : Nat) : a ≤ a := le_intro (add_zeror a)
theorem le_zero (a : Nat) : 0 ≤ a := le_intro (add_zerol a)
theorem le_trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1),
obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le_elim H2),
le_intro (calc a + (w1 + w2) = a + w1 + w2 : symm (add_assoc a w1 w2)
... = b + w2 : { Hw1 }
... = c : Hw2)
theorem le_add {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c
:= obtain (w : Nat) (Hw : a + w = b), from (le_elim H),
le_intro (calc a + c + w = a + (c + w) : add_assoc a c w
... = a + (w + c) : { add_comm c w }
... = a + w + c : symm (add_assoc a w c)
... = b + c : { Hw })
theorem le_antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1),
obtain (w2 : Nat) (Hw2 : b + w2 = a), from (le_elim H2),
let L1 : w1 + w2 = 0
:= add_injr (calc a + (w1 + w2) = a + w1 + w2 : { symm (add_assoc a w1 w2) }
... = b + w2 : { Hw1 }
... = a : Hw2
... = a + 0 : symm (add_zeror a)),
L2 : w1 = 0 := add_eqz L1
in calc a = a + 0 : symm (add_zeror a)
... = a + w1 : { symm L2 }
... = b : Hw1
theorem not_lt_0 (a : Nat) : ¬ a < 0
:= not_intro (λ H : a + 1 ≤ 0,
obtain (w : Nat) (Hw1 : a + 1 + w = 0), from (le_elim H),
absurd
(calc a + w + 1 = a + (w + 1) : add_assoc _ _ _
... = a + (1 + w) : { add_comm _ _ }
... = a + 1 + w : symm (add_assoc _ _ _)
... = 0 : Hw1)
(succ_nz (a + w)))
theorem lt_intro {a b c : Nat} (H : a + 1 + c = b) : a < b
:= le_intro H
theorem lt_elim {a b : Nat} (H : a < b) : ∃ x, a + 1 + x = b
:= le_elim H
theorem lt_le {a b : Nat} (H : a < b) : a ≤ b
:= obtain (w : Nat) (Hw : a + 1 + w = b), from (le_elim H),
le_intro (calc a + (1 + w) = a + 1 + w : symm (add_assoc _ _ _)
... = b : Hw)
theorem lt_ne {a b : Nat} (H : a < b) : a ≠ b
:= not_intro (λ H1 : a = b,
obtain (w : Nat) (Hw : a + 1 + w = b), from (lt_elim H),
absurd (calc w + 1 = 1 + w : add_comm _ _
... = 0 :
add_injr (calc b + (1 + w) = b + 1 + w : symm (add_assoc b 1 w)
... = a + 1 + w : { symm H1 }
... = b : Hw
... = b + 0 : symm (add_zeror b)))
(succ_nz w))
theorem lt_nrefl (a : Nat) : ¬ a < a
:= not_intro (λ H : a < a,
absurd (refl a) (lt_ne H))
theorem lt_trans {a b c : Nat} (H1 : a < b) (H2 : b < c) : a < c
:= obtain (w1 : Nat) (Hw1 : a + 1 + w1 = b), from (lt_elim H1),
obtain (w2 : Nat) (Hw2 : b + 1 + w2 = c), from (lt_elim H2),
lt_intro (calc a + 1 + (w1 + 1 + w2) = a + 1 + (w1 + (1 + w2)) : { add_assoc w1 1 w2 }
... = (a + 1 + w1) + (1 + w2) : symm (add_assoc _ _ _)
... = b + (1 + w2) : { Hw1 }
... = b + 1 + w2 : symm (add_assoc _ _ _)
... = c : Hw2)
theorem lt_le_trans {a b c : Nat} (H1 : a < b) (H2 : b ≤ c) : a < c
:= obtain (w1 : Nat) (Hw1 : a + 1 + w1 = b), from (lt_elim H1),
obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le_elim H2),
lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2 : symm (add_assoc _ _ _)
... = b + w2 : { Hw1 }
... = c : Hw2)
theorem le_lt_trans {a b c : Nat} (H1 : a ≤ b) (H2 : b < c) : a < c
:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1),
obtain (w2 : Nat) (Hw2 : b + 1 + w2 = c), from (lt_elim H2),
lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2 : symm (add_assoc _ _ _)
... = a + (1 + w1) + w2 : { add_assoc a 1 w1 }
... = a + (w1 + 1) + w2 : { add_comm 1 w1 }
... = a + w1 + 1 + w2 : { symm (add_assoc a w1 1) }
... = b + 1 + w2 : { Hw1 }
... = c : Hw2)
theorem ne_lt_succ {a b : Nat} (H1 : a ≠ b) (H2 : a < b + 1) : a < b
:= obtain (w : Nat) (Hw : a + 1 + w = b + 1), from (lt_elim H2),
let L : a + w = b := add_injl (calc a + w + 1 = a + (w + 1) : add_assoc _ _ _
... = a + (1 + w) : { add_comm _ _ }
... = a + 1 + w : symm (add_assoc _ _ _)
... = b + 1 : Hw)
in discriminate (λ Hz : w = 0, absurd_elim (a < b) (calc a = a + 0 : symm (add_zeror _)
... = a + w : { symm Hz }
... = b : L)
H1)
(λ (p : Nat) (Hp : w = p + 1), lt_intro (calc a + 1 + p = a + (1 + p) : add_assoc _ _ _
... = a + (p + 1) : { add_comm _ _ }
... = a + w : { symm Hp }
... = b : L))
theorem strong_induction {P : Nat → Bool} (H : ∀ n, (∀ m, m < n → P m) → P n) : ∀ a, P a
:= take a,
let stronger : P a ∧ ∀ m, m < a → P m :=
-- we prove a stronger result by regular induction on a
induction_on a
(show P 0 ∧ ∀ m, m < 0 → P m, from
let c2 : ∀ m, m < 0 → P m := λ (m : Nat) (Hlt : m < 0), absurd_elim (P m) Hlt (not_lt_0 m),
c1 : P 0 := H 0 c2
in and_intro c1 c2)
(λ (n : Nat) (iH : P n ∧ ∀ m, m < n → P m),
show P (n + 1) ∧ ∀ m, m < n + 1 → P m, from
let iH1 : P n := and_eliml iH,
iH2 : ∀ m, m < n → P m := and_elimr iH,
c2 : ∀ m, m < n + 1 → P m := λ (m : Nat) (Hlt : m < n + 1),
or_elim (em (m = n))
(λ Heq : m = n, subst iH1 (symm Heq))
(λ Hne : m ≠ n, iH2 m (ne_lt_succ Hne Hlt)),
c1 : P (n + 1) := H (n + 1) c2
in and_intro c1 c2)
in and_eliml stronger
set_opaque add true
set_opaque mul true
set_opaque le true
set_opaque id true
-- We should only mark constants as opaque after we proved the theorems/properties we need.
-- set_opaque ge true
-- set_opaque lt true
-- set_opaque gt true
-- set_opaque id true
end

12
src/builtin/README.md
View file

@ -1,12 +0,0 @@
Builtin libraries and scripts
------------------------------
This directory contains builtin Lean theories and additional Lua
scripts that are distributed with Lean. Some of the theories (e.g.,
`kernel.lean`) are automatically loaded when we start Lean. Others
must be imported using the `import` command.
Several Lean components rely on these libraries. For example, they use
the axioms and theorems defined in these libraries to build proofs.

44
src/builtin/Real.lean
View file

@ -1,44 +0,0 @@
import Int
variable Real : Type
alias ℝ : Real
builtin int_to_real : Int → Real
coercion int_to_real
definition nat_to_real (a : Nat) : Real := int_to_real (nat_to_int a)
coercion nat_to_real
namespace Real
builtin numeral
builtin add : Real → Real → Real
infixl 65 + : add
builtin mul : Real → Real → Real
infixl 70 * : mul
builtin div : Real → Real → Real
infixl 70 / : div
builtin le : Real → Real → Bool
infix 50 <= : le
infix 50 ≤ : le
definition ge (a b : Real) : Bool := b ≤ a
infix 50 >= : ge
infix 50 ≥ : ge
definition lt (a b : Real) : Bool := ¬ (a ≥ b)
infix 50 < : lt
definition gt (a b : Real) : Bool := ¬ (a ≤ b)
infix 50 > : gt
definition sub (a b : Real) : Real := a + -1.0 * b
infixl 65 - : sub
definition neg (a : Real) : Real := -1.0 * a
notation 75 - _ : neg
definition abs (a : Real) : Real := if (0.0 ≤ a) then a else (- a)
notation 55 | _ | : abs
end

74
src/builtin/bin.lean
View file

@ -1,74 +0,0 @@
import num tactic macros
namespace num
definition z := zero
definition d (x : num) := x + x
set_option simplifier::unfold true
theorem add_d_d (x y : num) : d x + d y = d (x + y)
:= by simp
theorem ssd (x : num) : succ (succ (d x)) = d (succ x)
:= by simp
theorem add_sd_d (x y : num) : succ (d x) + d y = succ (d (x + y))
:= by simp
theorem add_d_sd (x y : num) : d x + succ (d y) = succ (d (x + y))
:= by simp
theorem add_sd_sd (x y : num) : succ (d x) + succ (d y) = d (succ (x + y))
:= by simp
theorem d_z : d zero = zero
:= by simp
theorem s_s_z : succ (succ zero) = d (succ zero)
:= by simp
definition d1 (x : num) := succ (d x)
theorem d1_def (x : num) : d1 x = succ (d x)
:= refl _
set_opaque d true
add_rewrite s_s_z d_z add_d_d ssd add_sd_d add_d_sd add_sd_sd d1_def
scope
theorem test1 : d1 z = one
:= by simp
theorem test2 : d1 one = one + one + one
:= by simp
theorem test3 : d (d1 one) = one + one + one + one + one + one
:= by simp
theorem test4 : d (d1 (d (d1 one))) =
d (d (d (d (d1 z)))) + d (d (d (d1 z))) + succ (succ z)
:= by simp
theorem test5 : d (succ (succ (succ (succ (succ zero))))) = d (d1 (d one))
:= by simp
(*
local s = parse_lean("num::succ")
local z = parse_lean("num::zero")
local d = parse_lean("num::d")
local d1 = parse_lean("num::d1")
local add = parse_lean("num::add")
local t1 = s(s(s(s(s(s(s(s(s(s(z))))))))))
local t2, pr = simplify(t1)
print(t2)
print(pr)
local t1 = add(d(d(d(d(d(d(s(z))))))), d(d(d(d(s(z))))))
local t2, pr = simplify(t1)
print(t2)
print(pr)
*)
pop_scope
end

10
src/builtin/builtin.cpp
View file

@ -1,10 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
namespace lean {
// this is just a placeholder for forcing CMake to build the olean files
void open_extra() {}
}

43
src/builtin/dia.lean
View file

@ -1,43 +0,0 @@
import macros
theorem bool_inhab : inhabited Bool
:= inhabited_intro true
-- Excluded middle from eps_ax, boolext, funext, and subst
theorem em_new (p : Bool) : p ∨ ¬ p
:= let u := @eps Bool bool_inhab (λ x, x = true ∨ p),
v := @eps Bool bool_inhab (λ x, x = false ∨ p) in
have Hu : u = true ∨ p,
from @eps_ax Bool bool_inhab (λ x, x = true ∨ p) true (or_introl (refl true) p),
have Hv : v = false ∨ p,
from @eps_ax Bool bool_inhab (λ x, x = false ∨ p) false (or_introl (refl false) p),
have H1 : u ≠ v ∨ p,
from or_elim Hu
(assume Hut : u = true,
or_elim Hv
(assume Hvf : v = false,
have Hne : u ≠ v,
from subst (subst true_ne_false (symm Hut)) (symm Hvf),
or_introl Hne p)
(assume Hp : p, or_intror (u ≠ v) Hp))
(assume Hp : p, or_intror (u ≠ v) Hp),
have H2 : p → u = v,
from assume Hp : p,
have Hpred : (λ x, x = true ∨ p) = (λ x, x = false ∨ p),
from funext (take x : Bool,
have Hl : (x = true ∨ p) → (x = false ∨ p),
from assume A, or_intror (x = false) Hp,
have Hr : (x = false ∨ p) → (x = true ∨ p),
from assume A, or_intror (x = true) Hp,
show (x = true ∨ p) = (x = false ∨ p),
from boolext Hl Hr),
show u = v,
from @subst (Bool → Bool) (λ x : Bool, (@eq Bool x true) ∨ p) (λ x : Bool, (@eq Bool x false) ∨ p)
(λ q : Bool → Bool, @eps Bool bool_inhab (λ x : Bool, (@eq Bool x true) ∨ p) = @eps Bool bool_inhab q)
(@refl Bool (@eps Bool bool_inhab (λ x : Bool, (@eq Bool x true) ∨ p)))
Hpred,
have H3 : u ≠ v → ¬ p,
from contrapos H2,
or_elim H1
(assume Hne : u ≠ v, or_intror p (H3 Hne))
(assume Hp : p, or_introl Hp (¬ p))

27
src/builtin/find.lua
View file

@ -1,27 +0,0 @@
-- Define the command
--
-- Find [regex]
--
-- It displays objects in the environment whose name match the given regular expression.
-- Example: the command
-- Find "^[cC]on"
-- Displays all objects that start with the string "con" or "Con"
cmd_macro("find",
{ macro_arg.String },
function(env, pattern)
local opts = get_options()
-- Do not display the definition value
opts = opts:update({"lean", "pp", "definition_value"}, false)
local fmt = get_formatter()
local found = false
for obj in env:objects() do
if obj:has_name() and obj:has_type() and string.match(tostring(obj:get_name()), pattern) then
print(fmt(obj, opts))
found = true
end
end
if not found then
error("no object name in the environment matches the regular expression '" .. pattern .. "'")
end
end
)

1083
src/builtin/kernel.lean
View file

File diff suppressed because it is too large Load diff

32
src/builtin/lean2cpp.lean
View file

@ -1,32 +0,0 @@
(*
-- Auxiliary script for generating .cpp files that define
-- constants defined in Lean
local env = get_environment()
local num_imports = 0
print('/*')
print('Copyright (c) 2013 Microsoft Corporation. All rights reserved.')
print('Released under Apache 2.0 license as described in the file LICENSE.')
print('*/')
print("// Automatically generated file, DO NOT EDIT")
print('#include "kernel/environment.h"')
print('#include "kernel/decl_macros.h"')
print('namespace lean {')
for obj in env:objects() do
if obj:is_begin_import() or obj:is_begin_builtin_import() then
num_imports = num_imports + 1
elseif obj:is_end_import() then
num_imports = num_imports - 1
elseif num_imports == 0 and obj:has_name() and obj:has_type() and not is_explicit(env, obj:get_name()) and not obj:is_builtin() then
local is_fn = env:normalize(obj:get_type()):is_pi()
io.write('MK_CONSTANT(')
name_to_cpp_decl(obj:get_name())
if is_fn then
io.write('_fn')
end
io.write(', ')
name_to_cpp_expr(obj:get_name())
print(');')
end
end
print('}')
*)

13
src/builtin/lean2cpp.sh
View file

@ -1,13 +0,0 @@
#!/bin/sh
LEAN=$1 # Lean executable
SOURCE_DIR=$2 # Where the .lean and .lua auxiliary files are located
LEAN_FILE=$3 # Lean file to be exported
DEST=$4 # where to put the CPP file
ARGS=$5 # extra arguments
if $LEAN -q $ARGS $LEAN_FILE $SOURCE_DIR/name_conv.lua $SOURCE_DIR/lean2cpp.lean > $DEST.tmp
then
mv $DEST.tmp $DEST
else
echo "Failed to generate $DEST"
exit 1
fi

71
src/builtin/lean2h.lean
View file

@ -1,71 +0,0 @@
(*
-- Auxiliary script for generating .h file that declare mk_* and is_* functions for
-- constants defined in Lean
local env = get_environment()
local num_imports = 0
print('/*')
print('Copyright (c) 2013 Microsoft Corporation. All rights reserved.')
print('Released under Apache 2.0 license as described in the file LICENSE.')
print('*/')
print("// Automatically generated file, DO NOT EDIT")
print('#include "kernel/expr.h"')
print('namespace lean {')
for obj in env:objects() do
if obj:is_begin_import() or obj:is_begin_builtin_import() then
num_imports = num_imports + 1
elseif obj:is_end_import() then
num_imports = num_imports - 1
elseif num_imports == 0 and obj:has_name() and obj:has_type() and not is_explicit(env, obj:get_name()) and not obj:is_builtin() then
local ty = env:normalize(obj:get_type())
local is_fn = ty:is_pi()
local arity = 0
while ty:is_pi() do
n, d, ty = ty:fields()
arity = arity + 1
end
local is_th = obj:is_theorem() or obj:is_axiom()
io.write("expr mk_")
name_to_cpp_decl(obj:get_name())
if is_fn then
io.write("_fn");
end
print("();")
io.write("bool is_")
name_to_cpp_decl(obj:get_name())
if is_fn then
io.write("_fn");
end
print("(expr const & e);")
if is_fn and not is_th then
io.write("inline bool is_")
name_to_cpp_decl(obj:get_name())
io.write("(expr const & e) { return is_app(e) && is_");
name_to_cpp_decl(obj:get_name())
print("_fn(arg(e, 0)) && num_args(e) == " .. (arity+1) .. "; }")
end
if is_fn then
io.write("inline expr mk_")
name_to_cpp_decl(obj:get_name())
if is_th then
io.write("_th");
end
io.write("(");
for i = 1, arity do
if i > 1 then
io.write(", ")
end
io.write("expr const & e" .. tostring(i))
end
io.write(") { return mk_app({mk_");
name_to_cpp_decl(obj:get_name())
io.write("_fn()")
for i = 1, arity do
io.write(", e" .. tostring(i))
end
print ("}); }")
end
end
end
print('}')
*)

13
src/builtin/lean2h.sh
View file

@ -1,13 +0,0 @@
#!/bin/sh
LEAN=$1 # Lean executable
SOURCE_DIR=$2 # Where the .lean and .lua auxiliary files are located
LEAN_FILE=$3 # Lean file to be exported
DEST=$4 # where to put the CPP file
ARGS=$5 # extra arguments
if $LEAN -q $ARGS $LEAN_FILE $SOURCE_DIR/name_conv.lua $SOURCE_DIR/lean2h.lean > $DEST.tmp
then
mv $DEST.tmp $DEST
else
echo "Failed to generate $DEST"
exit 1
fi

195
src/builtin/list.lean
View file

@ -1,195 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import num subtype optional macros tactic
using num
using subtype
namespace list
definition none {A : (Type U)} : optional A
:= optional::@none A
definition some {A : (Type U)} (a : A) : optional A
:= optional::some a
definition list_rep (A : (Type U))
:= (num → optional A) # num
definition list_pred (A : (Type U))
:= λ p : list_rep A, ∀ i, i < (proj2 p) ↔ (proj1 p) i ≠ (@none A)
definition list (A : (Type U))
:= subtype (list_rep A) (list_pred A)
definition len {A : (Type U)} (l : list A) : num
:= proj2 (rep l)
definition fn {A : (Type U)} (l : list A) : num → optional A
:= proj1 (rep l)
theorem ext {A : (Type U)} {l1 l2 : list A} (H1 : len l1 = len l2) (H2 : fn l1 = fn l2) : l1 = l2
:= have Heq : rep l1 = rep l2,
from pairext _ _ H2 (to_heq H1),
rep_inj Heq
definition nil_rep (A : (Type U)) : list_rep A
:= (pair (λ n : num, @none A) zero : list_rep A)
theorem nil_pred (A : (Type U)) : list_pred A (nil_rep A)
:= take i : num,
let nil := nil_rep A
in iff_intro
(assume Hl : i < (proj2 nil),
have H1 : i < zero,
from Hl,
absurd_elim ((proj1 nil) i ≠ (@none A)) H1 (not_lt_zero i))
(assume Hr : (proj1 nil) i ≠ (@none A),
have H1 : (@none A) ≠ (@none A),
from Hr,
false_elim (i < (proj2 nil)) (a_neq_a_elim H1))
theorem inhab (A : (Type U)) : inhabited (list A)
:= subtype_inhabited (exists_intro (nil_rep A) (nil_pred A))
definition nil {A : (Type U)} : list A
:= abst (nil_rep A) (list::inhab A)
theorem len_nil {A : (Type U)} : len (@nil A) = zero
:= have H1 : rep (@nil A) = (pair (λ n : num, @none A) zero : list_rep A),
from rep_abst (list::inhab A) (nil_rep A) (nil_pred A),
have H2 : len (@nil A) = proj2 (rep (@nil A)),
from refl (len (@nil A)),
have H3 : proj2 (rep (@nil A)) = zero,
from proj2_congr H1,
trans H2 H3
definition cons_rep {A : (Type U)} (h : A) (t : list A) : list_rep A
:= pair (λ n, if n = (len t) then (some h) else (fn t) n) (succ (len t))
theorem cons_rep_fn_at {A : (Type U)} (h : A) (t : list A) (i : num)
: (proj1 (cons_rep h t)) i = (if i = len t then some h else (fn t) i)
:= have Heq : proj1 (cons_rep h t) = λ n, if n = len t then some h else (fn t) n,
from refl (proj1 (cons_rep h t)),
congr1 Heq i
definition cons_pred {A : (Type U)} (h : A) (t : list A) : list_pred A (cons_rep h t)
:= take i : num,
let c := cons_rep h t in
have Hci : (proj1 c) i = (if i = (len t) then (some h) else (fn t) i),
from cons_rep_fn_at h t i,
have Ht : ∀ i, i < (len t) ↔ (fn t) i ≠ (@none A),
from P_rep t,
iff_intro
(assume Hl : i < (succ (len t)),
or_elim (em (i = len t))
(assume Heq : i = len t,
calc (proj1 c) i = (if i = (len t) then (some h) else (fn t) i) : Hci
... = some h : by simp
... ≠ @none A : optional::distinct h)
(assume Hne : i ≠ len t,
have Hlt : i < len t,
from lt_succ_ne_to_lt Hl Hne,
calc (proj1 c) i = (if i = (len t) then (some h) else (fn t) i) : Hci
... = (fn t) i : by simp
... ≠ @none A : (Ht i) ◂ Hlt))
(assume Hr : (proj1 c) i ≠ (@none A),
or_elim (em (i = len t))
(assume Heq : i = len t,
subst (n_lt_succ_n (len t)) (symm Heq))
(assume Hne : i ≠ len t,
have Hne2 : (fn t) i ≠ (@none A),
from calc (fn t) i = (if i = (len t) then (some h) else (fn t) i) : by simp
... = (proj1 c) i : symm Hci
... ≠ (@none A) : Hr,
have Hlt : i < len t,
from (symm (Ht i)) ◂ Hne2,
show i < succ (len t),
from lt_to_lt_succ Hlt))
definition cons {A : (Type U)} (h : A) (t : list A) : list A
:= abst (cons_rep h t) (list::inhab A)
theorem cons_fn_at {A : (Type U)} (h : A) (t : list A) (i : num)
: (fn (cons h t)) i = (if i = len t then some h else (fn t) i)
:= have H1 : rep (cons h t) = (cons_rep h t) ,
from rep_abst (list::inhab A) (cons_rep h t) (cons_pred h t),
have H2 : fn (cons h t) = proj1 (cons_rep h t),
from proj1_congr H1,
have H3 : fn (cons h t) i = (proj1 (cons_rep h t)) i,
from congr1 H2 i,
have H4 : (proj1 (cons_rep h t)) i = (if i = len t then some h else (fn t) i),
from cons_rep_fn_at h t i,
trans H3 H4
theorem len_cons {A : (Type U)} (h : A) (t : list A) : len (cons h t) = succ (len t)
:= have H1 : rep (cons h t) = cons_rep h t,
from rep_abst (list::inhab A) (cons_rep h t) (cons_pred h t),
have H2 : proj2 (cons_rep h t) = succ (len t),
from refl (proj2 (cons_rep h t)),
have H3 : proj2 (rep (cons h t)) = proj2 (cons_rep h t),
from proj2_congr H1,
trans H3 H2
theorem cons_ne_nil {A : (Type U)} (h : A) (t : list A) : cons h t ≠ nil
:= not_intro (assume R : cons h t = nil,
have Heq1 : cons_rep h t = (nil_rep A),
from abst_inj (list::inhab A) (cons_pred h t) (nil_pred A) R,
have Heq2 : succ (len t) = zero,
from proj2_congr Heq1,
absurd Heq2 (succ_nz (len t)))
theorem flip_iff {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b
:= subst (refl (¬ a)) H
theorem cons_inj {A : (Type U)} {h1 h2 : A} {t1 t2 : list A} : cons h1 t1 = cons h2 t2 → h1 = h2 ∧ t1 = t2
:= assume Heq : cons h1 t1 = cons h2 t2,
have Heq_rep : (cons_rep h1 t1) = (cons_rep h2 t2),
from abst_inj (list::inhab A) (cons_pred h1 t1) (cons_pred h2 t2) Heq,
have Heq_len : len t1 = len t2,
from succ_inj (proj2_congr Heq_rep),
have Heq_fn : (λ n, if n = len t2 then some h1 else (fn t1) n) =
(λ n, if n = len t2 then some h2 else (fn t2) n),
from subst (proj1_congr Heq_rep) Heq_len,
have Heq_some : some h1 = some h2,
from calc some h1 = if len t2 = len t2 then some h1 else (fn t1) (len t2) : by simp
... = if len t2 = len t2 then some h2 else (fn t2) (len t2) : congr1 Heq_fn (len t2)
... = some h2 : by simp,
have Heq_head : h1 = h2,
from optional::injectivity Heq_some,
have Heq_fn_t : fn t1 = fn t2,
from funext (λ i,
or_elim (em (i = len t2))
(λ Heqi : i = len t2,
have Hlti2 : ¬ (i < len t2),
from eq_to_not_lt Heqi,
have Hlti1 : ¬ (i < len t1),
from subst Hlti2 (symm Heq_len),
have Ht1 : i < len t1 ↔ (fn t1) i ≠ (@none A),
from P_rep t1 i,
have Ht2 : i < len t2 ↔ (fn t2) i ≠ (@none A),
from P_rep t2 i,
have Heq1 : (fn t1) i = (@none A),
from not_not_elim ((flip_iff Ht1) ◂ Hlti1),
have Heq2 : (fn t2) i = (@none A),
from not_not_elim ((flip_iff Ht2) ◂ Hlti2),
trans Heq1 (symm Heq2))
(λ Hnei : i ≠ len t2,
calc fn t1 i = if i = len t2 then some h1 else (fn t1) i : by simp
... = if i = len t2 then some h2 else (fn t2) i : congr1 Heq_fn i
... = fn t2 i : by simp)),
have Heq_tail : t1 = t2,
from ext Heq_len Heq_fn_t,
and_intro Heq_head Heq_tail
theorem cons_inj_head {A : (Type U)} {h1 h2 : A} {t1 t2 : list A} : cons h1 t1 = cons h2 t2 → h1 = h2
:= assume H, and_eliml (cons_inj H)
theorem cons_inj_tail {A : (Type U)} {h1 h2 : A} {t1 t2 : list A} : cons h1 t1 = cons h2 t2 → t1 = t2
:= assume H, and_elimr (cons_inj H)
set_opaque list true
set_opaque cons true
set_opaque nil true
set_opaque len true
end
definition list := list::list

142
src/builtin/macros.lua
View file

@ -1,142 +0,0 @@
-- Extra macros for automating proof construction using Lua.
-- This macro creates the syntax-sugar
-- name bindings ',' expr
-- For a function f with signature
-- f : ... (A : Type) ... (Pi x : A, ...)
--
-- farity is the arity of f
-- typepos is the position of (A : Type) argument
-- lambdapos is the position of the (Pi x : A, ...) argument
--
function binder_macro(name, f, farity, typepos, lambdapos)
local precedence = 0
macro(name, { macro_arg.Parameters, macro_arg.Comma, macro_arg.Expr },
function (env, bindings, body)
local r = body
for i = #bindings, 1, -1 do
local bname = bindings[i][1]
local btype = bindings[i][2]
local args = {}
args[#args + 1] = f
for j = 1, farity, 1 do
if j == typepos then
args[#args + 1] = btype
elseif j == lambdapos then
args[#args + 1] = fun(bname, btype, r)
else
args[#args + 1] = mk_placeholder()
end
end
r = mk_app(unpack(args))
end
return r
end,
precedence)
end
-- The following macro is used to create nary versions of operators such as mp.
-- Example: suppose we invoke
--
-- nary_macro("eqmp'", Const("eqmp"), 4)
--
-- Then, the macro expression
--
-- eqmp' Foo H1 H2 H3
--
-- produces the expression
--
-- (eqmp (eqmp (eqmp Foo H1) H2) H3)
function nary_macro(name, f, farity)
local bin_app = function(e1, e2)
local args = {}
args[#args + 1] = f
for i = 1, farity - 2, 1 do
args[#args + 1] = mk_placeholder()
end
args[#args + 1] = e1
args[#args + 1] = e2
return mk_app(unpack(args))
end
macro(name, { macro_arg.Expr, macro_arg.Expr, macro_arg.Exprs },
function (env, e1, e2, rest)
local r = bin_app(e1, e2)
for i = 1, #rest do
r = bin_app(r, rest[i])
end
return r
end)
end
-- exists::elim syntax-sugar
-- Example:
-- Assume we have the following two axioms
-- Axiom Ax1: exists x y, P x y
-- Axiom Ax2: forall x y, not P x y
-- Now, the following macro expression
-- obtain (a b : Nat) (H : P a b) from Ax1,
-- show false, from absurd H (instantiate Ax2 a b)
-- expands to
-- exists::elim Ax1
-- (fun (a : Nat) (Haux : ...),
-- exists::elim Haux
-- (fun (b : Na) (H : P a b),
-- show false, from absurd H (instantiate Ax2 a b)
macro("obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg.Expr, macro_arg.Comma, macro_arg.Expr },
function (env, bindings, fromid, exPr, body)
local n = #bindings
if n < 2 then
error("invalid 'obtain' expression at least two bindings must be provided")
end
if fromid ~= name("from") then
error("invalid 'obtain' expression, 'from' keyword expected, got '" .. tostring(fromid) .. "'")
end
local exElim = mk_constant("exists_elim")
local H_name = bindings[n][1]
local H_type = bindings[n][2]
local a_name = bindings[n-1][1]
local a_type = bindings[n-1][2]
for i = n - 2, 1, -1 do
local Haux = name("obtain", "macro", "H", i)
body = mk_app(exElim, mk_placeholder(), mk_placeholder(), mk_placeholder(), mk_constant(Haux),
fun(a_name, a_type, fun(H_name, H_type, body)))
H_name = Haux
H_type = mk_placeholder()
a_name = bindings[i][1]
a_type = bindings[i][2]
-- We added a new binding, so we must lift free vars
body = body:lift_free_vars(0, 1)
end
-- exPr occurs after the bindings, so it is in the context of them.
-- However, this is not the case for ExistsElim.
-- So, we must lower the free variables there
exPr = exPr:lower_free_vars(n, n)
return mk_app(exElim, mk_placeholder(), mk_placeholder(), mk_placeholder(), exPr,
fun(a_name, a_type, fun(H_name, H_type, body)))
end,
0)
function mk_lambdas(bindings, body)
local r = body
for i = #bindings, 1, -1 do
r = fun(bindings[i][1], bindings[i][2], r)
end
return r
end
-- Allow (assume x : A, B) to be used instead of (fun x : A, B).
-- It can be used to make scripts more readable, when (fun x : A, B) is being used to encode a discharge
macro("assume", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Expr},
function (env, bindings, body)
return mk_lambdas(bindings, body)
end,
0)
-- Allow (assume x : A, B) to be used instead of (fun x : A, B).
-- It can be used to make scripts more readable, when (fun x : A, B) is being used to encode a forall_intro
macro("take", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Expr},
function (env, bindings, body)
return mk_lambdas(bindings, body)
end,
0)

44
src/builtin/name_conv.lua
View file

@ -1,44 +0,0 @@
-- Output a C++ statement that creates the given name
function sanitize(s)
s, _ = string.gsub(s, "'", "_")
return s
end
function name_to_cpp_expr(n)
function rec(n)
if not n:is_atomic() then
rec(n:get_prefix())
io.write(", ")
end
if n:is_string() then
local s = n:get_string()
io.write("\"" .. sanitize(s) .. "\"")
else
error("numeral hierarchical names are not supported in the C++ interface: " .. tostring(n))
end
end
io.write("name(")
if n:is_atomic() then
rec(n)
else
io.write("{")
rec(n)
io.write("}")
end
io.write(")")
end
-- Output a C++ constant name based on the given hierarchical name
-- It uses '_' to glue the hierarchical name parts
function name_to_cpp_decl(n)
if not n:is_atomic(n) then
name_to_cpp_decl(n:get_prefix())
io.write("_")
end
if n:is_string() then
local s = n:get_string()
io.write(sanitize(s))
else
error("numeral hierarchical names are not supported in the C++ interface: " .. tostring(n))
end
end

711
src/builtin/num.lean
View file

@ -1,711 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import macros subtype tactic
using subtype
namespace num
theorem inhabited_ind : inhabited ind
-- We use as the witness for non-emptiness, the value w in ind that is not convered by f.
:= obtain f His, from infinity,
obtain w Hw, from and_elimr His,
inhabited_intro w
definition S := ε (inhabited_ex_intro infinity) (λ f, injective f ∧ non_surjective f)
definition Z := ε inhabited_ind (λ y, ∀ x, ¬ S x = y)
theorem injective_S : injective S
:= and_eliml (exists_to_eps infinity)
theorem non_surjective_S : non_surjective S
:= and_elimr (exists_to_eps infinity)
theorem S_ne_Z (i : ind) : S i ≠ Z
:= obtain w Hw, from non_surjective_S,
eps_ax inhabited_ind w Hw i
definition N (i : ind) : Bool
:= ∀ P, P Z → (∀ x, P x → P (S x)) → P i
theorem N_Z : N Z
:= λ P Hz Hi, Hz
theorem N_S {i : ind} (H : N i) : N (S i)
:= λ P Hz Hi, Hi i (H P Hz Hi)
theorem N_smallest : ∀ P : ind → Bool, P Z → (∀ x, P x → P (S x)) → (∀ i, N i → P i)
:= λ P Hz Hi i Hni, Hni P Hz Hi
definition num := subtype ind N
theorem inhab : inhabited num
:= subtype_inhabited (exists_intro Z N_Z)
definition zero : num
:= abst Z inhab
theorem zero_pred : N Z
:= N_Z
definition succ (n : num) : num
:= abst (S (rep n)) inhab
theorem succ_pred (n : num) : N (S (rep n))
:= have N_n : N (rep n),
from P_rep n,
show N (S (rep n)),
from N_S N_n
theorem succ_inj {a b : num} : succ a = succ b → a = b
:= assume Heq1 : succ a = succ b,
have Heq2 : S (rep a) = S (rep b),
from abst_inj inhab (succ_pred a) (succ_pred b) Heq1,
have rep_eq : (rep a) = (rep b),
from injective_S (rep a) (rep b) Heq2,
show a = b,
from rep_inj rep_eq
theorem succ_inj_rw {a b : num} : succ a = succ b ↔ a = b
:= iff_intro
(assume Hl, succ_inj Hl)
(assume Hr, congr2 succ Hr)
add_rewrite succ_inj_rw
theorem succ_nz (a : num) : ¬ (succ a = zero)
:= not_intro (assume R : succ a = zero,
have Heq1 : S (rep a) = Z,
from abst_inj inhab (succ_pred a) zero_pred R,
show false,
from absurd Heq1 (S_ne_Z (rep a)))
add_rewrite succ_nz
theorem induction {P : num → Bool} (H1 : P zero) (H2 : ∀ n, P n → P (succ n)) : ∀ a, P a
:= take a,
let Q := λ x, N x ∧ P (abst x inhab)
in have QZ : Q Z,
from and_intro zero_pred H1,
have QS : ∀ x, Q x → Q (S x),
from take x, assume Qx,
have Hp1 : P (succ (abst x inhab)),
from H2 (abst x inhab) (and_elimr Qx),
have Hp2 : P (abst (S (rep (abst x inhab))) inhab),
from Hp1,
have Nx : N x,
from and_eliml Qx,
have rep_eq : rep (abst x inhab) = x,
from rep_abst inhab x Nx,
show Q (S x),
from and_intro (N_S Nx) (subst Hp2 rep_eq),
have Qa : P (abst (rep a) inhab),
from and_elimr (N_smallest Q QZ QS (rep a) (P_rep a)),
have abst_eq : abst (rep a) inhab = a,
from abst_rep inhab a,
show P a,
from subst Qa abst_eq
theorem induction_on {P : num → Bool} (a : num) (H1 : P zero) (H2 : ∀ n, P n → P (succ n)) : P a
:= induction H1 H2 a
theorem dichotomy (m : num) : m = zero ∨ (∃ n, m = succ n)
:= induction_on m
(by simp)
(λ n iH, or_intror _
(@exists_intro _ (λ x, succ n = succ x) n (refl (succ n))))
theorem sn_ne_n (n : num) : succ n ≠ n
:= induction_on n
(succ_nz zero)
(λ (n : num) (iH : succ n ≠ n),
not_intro
(assume R : succ (succ n) = succ n,
absurd (succ_inj R) iH))
add_rewrite sn_ne_n
set_opaque num true
set_opaque Z true
set_opaque S true
set_opaque zero true
set_opaque succ true
definition lt (m n : num) := ∃ P, (∀ i, P (succ i) → P i) ∧ P m ∧ ¬ P n
infix 50 < : lt
theorem lt_elim {m n : num} {B : Bool} (H1 : m < n)
(H2 : ∀ (P : num → Bool), (∀ i, P (succ i) → P i) → P m → ¬ P n → B)
: B
:= obtain P Pdef, from H1,
H2 P (and_eliml Pdef) (and_eliml (and_elimr Pdef)) (and_elimr (and_elimr Pdef))
theorem lt_intro {m n : num} {P : num → Bool} (H1 : ∀ i, P (succ i) → P i) (H2 : P m) (H3 : ¬ P n) : m < n
:= exists_intro P (and_intro H1 (and_intro H2 H3))
set_opaque lt true
theorem lt_nrefl (n : num) : ¬ (n < n)
:= not_intro
(assume N : n < n,
lt_elim N (λ P Pred Pn nPn, absurd Pn nPn))
add_rewrite lt_nrefl
theorem lt_succ {m n : num} : succ m < n → m < n
:= assume H : succ m < n,
lt_elim H
(λ (P : num → Bool) (Pred : ∀ i, P (succ i) → P i) (Psm : P (succ m)) (nPn : ¬ P n),
have Pm : P m,
from Pred m Psm,
show m < n,
from lt_intro Pred Pm nPn)
theorem not_lt_zero (n : num) : ¬ (n < zero)
:= induction_on n
(show ¬ (zero < zero),
from lt_nrefl zero)
(λ (n : num) (iH : ¬ (n < zero)),
show ¬ (succ n < zero),
from not_intro
(assume N : succ n < zero,
have nLTzero : n < zero,
from lt_succ N,
show false,
from absurd nLTzero iH))
add_rewrite not_lt_zero
definition one := succ zero
theorem one_eq_succ_zero : one = succ zero
:= refl one
theorem zero_lt_one : zero < one
:= let P : num → Bool := λ x, x = zero
in have Ppred : ∀ i, P (succ i) → P i,
from take i, assume Ps : P (succ i),
have si_eq_z : succ i = zero,
from Ps,
have si_ne_z : succ i ≠ zero,
from succ_nz i,
show P i,
from absurd_elim (P i) si_eq_z (succ_nz i),
have Pz : P zero,
from (refl zero),
have nPs : ¬ P (succ zero),
from succ_nz zero,
show zero < succ zero,
from lt_intro Ppred Pz nPs
theorem succ_mono_lt {m n : num} : m < n → succ m < succ n
:= assume H : m < n,
lt_elim H
(λ (P : num → Bool) (Ppred : ∀ i, P (succ i) → P i) (Pm : P m) (nPn : ¬ P n),
let Q : num → Bool := λ x, x = succ m ∨ P x
in have Qpred : ∀ i, Q (succ i) → Q i,
from take i, assume Qsi : Q (succ i),
or_elim Qsi
(assume Hl : succ i = succ m,
have Him : i = m, from succ_inj Hl,
have Pi : P i, from subst Pm (symm Him),
or_intror _ Pi)
(assume Hr : P (succ i),
have Pi : P i, from Ppred i Hr,
or_intror _ Pi),
have Qsm : Q (succ m),
from or_introl (refl (succ m)) _,
have nQsn : ¬ Q (succ n),
from not_intro
(assume R : Q (succ n),
or_elim R
(assume Hl : succ n = succ m,
absurd Pm (subst nPn (succ_inj Hl)))
(assume Hr : P (succ n), absurd (Ppred n Hr) nPn)),
show succ m < succ n,
from lt_intro Qpred Qsm nQsn)
theorem lt_to_lt_succ {m n : num} : m < n → m < succ n
:= assume H : m < n,
lt_elim H
(λ (P : num → Bool) (Ppred : ∀ i, P (succ i) → P i) (Pm : P m) (nPn : ¬ P n),
have nPsn : ¬ P (succ n),
from not_intro
(assume R : P (succ n),
absurd (Ppred n R) nPn),
show m < succ n,
from lt_intro Ppred Pm nPsn)
theorem n_lt_succ_n (n : num) : n < succ n
:= induction_on n
(show zero < succ zero, from zero_lt_one)
(λ (n : num) (iH : n < succ n),
succ_mono_lt iH)
add_rewrite n_lt_succ_n
theorem lt_to_neq {m n : num} : m < n → m ≠ n
:= assume H : m < n,
lt_elim H
(λ (P : num → Bool) (Ppred : ∀ i, P (succ i) → P i) (Pm : P m) (nPn : ¬ P n),
not_intro
(assume R : m = n,
absurd Pm (subst nPn (symm R))))
theorem eq_to_not_lt {m n : num} : m = n → ¬ (m < n)
:= assume Heq : m = n,
not_intro (assume R : m < n, absurd (subst R Heq) (lt_nrefl n))
theorem zero_lt_succ_n {n : num} : zero < succ n
:= induction_on n
(show zero < succ zero, from zero_lt_one)
(λ (n : num) (iH : zero < succ n),
lt_to_lt_succ iH)
add_rewrite zero_lt_succ_n
theorem lt_succ_to_disj {m n : num} : m < succ n → m = n ∨ m < n
:= assume H : m < succ n,
lt_elim H
(λ (P : num → Bool) (Ppred : ∀ i, P (succ i) → P i) (Pm : P m) (nPsn : ¬ P (succ n)),
or_elim (em (m = n))
(assume Heq : m = n, or_introl Heq _)
(assume Hne : m ≠ n,
let Q : num → Bool := λ x, x ≠ n ∧ P x
in have Qpred : ∀ i, Q (succ i) → Q i,
from take i, assume Hsi : Q (succ i),
have H1 : succ i ≠ n,
from and_eliml Hsi,
have Psi : P (succ i),
from and_elimr Hsi,
have Pi : P i,
from Ppred i Psi,
have neq : i ≠ n,
from not_intro (assume N : i = n,
absurd (subst Psi N) nPsn),
and_intro neq Pi,
have Qm : Q m,
from and_intro Hne Pm,
have nQn : ¬ Q n,
from not_intro
(assume N : n ≠ n ∧ P n,
absurd (refl n) (and_eliml N)),
show m = n ∨ m < n,
from or_intror _ (lt_intro Qpred Qm nQn)))
theorem disj_to_lt_succ {m n : num} : m = n ∨ m < n → m < succ n
:= assume H : m = n ∨ m < n,
or_elim H
(λ Hl : m = n,
have H1 : n < succ n,
from n_lt_succ_n n,
show m < succ n,
from subst H1 (symm Hl))
(λ Hr : m < n, lt_to_lt_succ Hr)
theorem lt_succ_ne_to_lt {m n : num} : m < succ n → m ≠ n → m < n
:= assume (H1 : m < succ n) (H2 : m ≠ n),
resolve1 (lt_succ_to_disj H1) H2
definition simp_rec_rel {A : (Type U)} (fn : num → A) (x : A) (f : A → A) (n : num)
:= fn zero = x ∧ (∀ m, m < n → fn (succ m) = f (fn m))
definition simp_rec_fun {A : (Type U)} (x : A) (f : A → A) (n : num) : num → A
:= ε (inhabited_fun num (inhabited_intro x)) (λ fn : num → A, simp_rec_rel fn x f n)
-- The basic idea is:
-- (simp_rec_fun x f n) returns a function that 'works' for all m < n
-- We have that n < succ n, then we can define (simp_rec x f n) as:
definition simp_rec {A : (Type U)} (x : A) (f : A → A) (n : num) : A
:= simp_rec_fun x f (succ n) n
theorem simp_rec_def {A : (Type U)} (x : A) (f : A → A) (n : num)
: (∃ fn, simp_rec_rel fn x f n)
↔
(simp_rec_fun x f n zero = x ∧
∀ m, m < n → simp_rec_fun x f n (succ m) = f (simp_rec_fun x f n m))
:= iff_intro
(assume Hl : (∃ fn, simp_rec_rel fn x f n),
obtain (fn : num → A) (Hfn : simp_rec_rel fn x f n),
from Hl,
have inhab : inhabited (num → A),
from (inhabited_fun num (inhabited_intro x)),
show simp_rec_rel (simp_rec_fun x f n) x f n,
from @eps_ax (num → A) inhab (λ fn, simp_rec_rel fn x f n) fn Hfn)
(assume Hr,
have H1 : simp_rec_rel (simp_rec_fun x f n) x f n,
from Hr,
show (∃ fn, simp_rec_rel fn x f n),
from exists_intro (simp_rec_fun x f n) H1)
theorem simp_rec_ex {A : (Type U)} (x : A) (f : A → A) (n : num)
: ∃ fn, simp_rec_rel fn x f n
:= induction_on n
(let fn : num → A := λ n, x in
have fz : fn zero = x, by simp,
have fs : ∀ m, m < zero → fn (succ m) = f (fn m),
from take m, assume Hmn : m < zero,
absurd_elim (fn (succ m) = f (fn m))
Hmn
(not_lt_zero m),
show ∃ fn, simp_rec_rel fn x f zero,
from exists_intro fn (and_intro fz fs))
(λ (n : num) (iH : ∃ fn, simp_rec_rel fn x f n),
obtain (fn : num → A) (Hfn : simp_rec_rel fn x f n), from iH,
let fn1 : num → A := λ m, if succ n = m then f (fn n) else fn m in
have fnz : fn zero = x, from and_eliml Hfn,
have f1z : fn1 zero = x, by simp,
have f1s : ∀ m, m < succ n → fn1 (succ m) = f (fn1 m),
from take m, assume Hlt : m < succ n,
or_elim (lt_succ_to_disj Hlt)
(assume Hl : m = n, by simp)
(assume Hr : m < n,
have Haux1 : fn (succ m) = f (fn m),
from (and_elimr Hfn m Hr),
have Hrw1 : (succ n = succ m) ↔ false,
from eqf_intro (not_intro (assume N : succ n = succ m,
have nLt : ¬ m < n,
from eq_to_not_lt (symm (succ_inj N)),
absurd Hr nLt)),
have Haux2 : m < succ n,
from lt_to_lt_succ Hr,
have Haux3 : ¬ (succ n = m),
from ne_symm (lt_to_neq Haux2),
have Hrw2 : fn m = fn1 m,
by simp,
calc fn1 (succ m) = if succ n = succ m then f (fn n) else fn (succ m) : refl (fn1 (succ m))
... = if false then f (fn n) else fn (succ m) : { Hrw1 }
... = fn (succ m) : if_false _ _
... = f (fn m) : Haux1
... = f (fn1 m) : { Hrw2 }),
show ∃ fn, simp_rec_rel fn x f (succ n),
from exists_intro fn1 (and_intro f1z f1s))
theorem simp_rec_lemma1 {A : (Type U)} (x : A) (f : A → A) (n : num)
: simp_rec_fun x f n zero = x ∧
∀ m, m < n → simp_rec_fun x f n (succ m) = f (simp_rec_fun x f n m)
:= (simp_rec_def x f n) ◂ (simp_rec_ex x f n)
theorem simp_rec_lemma2 {A : (Type U)} (x : A) (f : A → A) (n m1 m2 : num)
: n < m1 → n < m2 → simp_rec_fun x f m1 n = simp_rec_fun x f m2 n
:= induction_on n
(assume H1 H2,
calc simp_rec_fun x f m1 zero = x : and_eliml (simp_rec_lemma1 x f m1)
... = simp_rec_fun x f m2 zero : symm (and_eliml (simp_rec_lemma1 x f m2)))
(λ (n : num) (iH : n < m1 → n < m2 → simp_rec_fun x f m1 n = simp_rec_fun x f m2 n),
assume (Hs1 : succ n < m1) (Hs2 : succ n < m2),
have H1 : n < m1,
from lt_succ Hs1,
have H2 : n < m2,
from lt_succ Hs2,
have Heq1 : simp_rec_fun x f m1 (succ n) = f (simp_rec_fun x f m1 n),
from and_elimr (simp_rec_lemma1 x f m1) n H1,
have Heq2 : simp_rec_fun x f m1 n = simp_rec_fun x f m2 n,
from iH H1 H2,
have Heq3 : simp_rec_fun x f m2 (succ n) = f (simp_rec_fun x f m2 n),
from and_elimr (simp_rec_lemma1 x f m2) n H2,
show simp_rec_fun x f m1 (succ n) = simp_rec_fun x f m2 (succ n),
by simp)
theorem simp_rec_thm {A : (Type U)} (x : A) (f : A → A)
: simp_rec x f zero = x ∧
∀ m, simp_rec x f (succ m) = f (simp_rec x f m)
:= have Heqz : simp_rec_fun x f (succ zero) zero = x,
from and_eliml (simp_rec_lemma1 x f (succ zero)),
have Hz : simp_rec x f zero = x,
from calc simp_rec x f zero = simp_rec_fun x f (succ zero) zero : refl _
... = x : Heqz,
have Hs : ∀ m, simp_rec x f (succ m) = f (simp_rec x f m),
from take m,
have Hlt1 : m < succ (succ m),
from lt_to_lt_succ (n_lt_succ_n m),
have Hlt2 : m < succ m,
from n_lt_succ_n m,
have Heq1 : simp_rec_fun x f (succ (succ m)) (succ m) = f (simp_rec_fun x f (succ (succ m)) m),
from and_elimr (simp_rec_lemma1 x f (succ (succ m))) m Hlt1,
have Heq2 : simp_rec_fun x f (succ (succ m)) m = simp_rec_fun x f (succ m) m,
from simp_rec_lemma2 x f m (succ (succ m)) (succ m) Hlt1 Hlt2,
calc simp_rec x f (succ m) = simp_rec_fun x f (succ (succ m)) (succ m) : refl _
... = f (simp_rec_fun x f (succ (succ m)) m) : Heq1
... = f (simp_rec_fun x f (succ m) m) : { Heq2 }
... = f (simp_rec x f m) : refl _,
show simp_rec x f zero = x ∧ ∀ m, simp_rec x f (succ m) = f (simp_rec x f m),
from and_intro Hz Hs
definition pre (m : num) := if m = zero then zero else ε inhab (λ n, succ n = m)
theorem pre_zero : pre zero = zero
:= by (Then (unfold num::pre) simp)
theorem pre_succ (m : num) : pre (succ m) = m
:= have Heq : (λ n, succ n = succ m) = (λ n, n = m),
from funext (λ n, iff_intro (assume Hl, succ_inj Hl)
(assume Hr, congr2 succ Hr)),
calc pre (succ m) = ε inhab (λ n, succ n = succ m) : by (Then (unfold num::pre) simp)
... = ε inhab (λ n, n = m) : { Heq }
... = m : eps_singleton inhab m
add_rewrite pre_zero pre_succ
theorem succ_pre (m : num) : m ≠ zero → succ (pre m) = m
:= assume H : m ≠ zero,
have H1 : ∃ n, m = succ n,
from resolve1 (dichotomy m) H,
obtain (w : num) (H2 : m = succ w), from H1,
have H3 : (λ n, succ n = m) = (λ n, n = w),
from funext (λ n, by simp),
calc succ (pre m) = succ (if m = zero then zero else ε inhab (λ n, succ n = m)) : refl _
... = succ (ε inhab (λ n, n = w)) : by simp
... = succ w : { eps_singleton inhab w }
... = m : symm H2
definition prim_rec_fun {A : (Type U)} (x : A) (f : A → num → A)
:= simp_rec (λ n : num, x) (λ fn n, f (fn (pre n)) n)
definition prim_rec {A : (Type U)} (x : A) (f : A → num → A) (m : num)
:= prim_rec_fun x f m (pre m)
theorem prim_rec_thm {A : (Type U)} (x : A) (f : A → num → A)
: prim_rec x f zero = x ∧
∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m
:= let faux := λ fn n, f (fn (pre n)) n in
have Hz : prim_rec x f zero = x,
from have Heq1 : simp_rec (λ n, x) faux zero = (λ n : num, x),
from and_eliml (simp_rec_thm (λ n, x) faux),
calc prim_rec x f zero = prim_rec_fun x f zero (pre zero) : refl _
... = prim_rec_fun x f zero zero : { pre_zero }
... = simp_rec (λ n, x) faux zero zero : refl _
... = x : congr1 Heq1 zero,
have Hs : ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m,
from take m,
have Heq1 : pre (succ m) = m,
from pre_succ m,
have Heq2 : simp_rec (λ n, x) faux (succ m) = faux (simp_rec (λ n, x) faux m),
from and_elimr (simp_rec_thm (λ n, x) faux) m,
calc prim_rec x f (succ m) = prim_rec_fun x f (succ m) (pre (succ m)) : refl _
... = prim_rec_fun x f (succ m) m : { Heq1 }
... = simp_rec (λ n, x) faux (succ m) m : refl _
... = faux (simp_rec (λ n, x) faux m) m : congr1 Heq2 m
... = f (prim_rec x f m) m : refl _,
show prim_rec x f zero = x ∧ ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m,
from and_intro Hz Hs
theorem prim_rec_zero {A : (Type U)} (x : A) (f : A → num → A) : prim_rec x f zero = x
:= and_eliml (prim_rec_thm x f)
theorem prim_rec_succ {A : (Type U)} (x : A) (f : A → num → A) (m : num) : prim_rec x f (succ m) = f (prim_rec x f m) m
:= and_elimr (prim_rec_thm x f) m
set_opaque simp_rec_rel true
set_opaque simp_rec_fun true
set_opaque simp_rec true
set_opaque prim_rec_fun true
set_opaque prim_rec true
definition add (a b : num) : num
:= prim_rec a (λ x n, succ x) b
infixl 65 + : add
theorem add_zeror (a : num) : a + zero = a
:= prim_rec_zero a (λ x n, succ x)
theorem add_succr (a b : num) : a + succ b = succ (a + b)
:= prim_rec_succ a (λ x n, succ x) b
definition mul (a b : num) : num
:= prim_rec zero (λ x n, x + a) b
infixl 70 * : mul
theorem mul_zeror (a : num) : a * zero = zero
:= prim_rec_zero zero (λ x n, x + a)
theorem mul_succr (a b : num) : a * (succ b) = a * b + a
:= prim_rec_succ zero (λ x n, x + a) b
add_rewrite add_zeror add_succr mul_zeror mul_succr
set_opaque add true
set_opaque mul true
theorem add_zerol (a : num) : zero + a = a
:= induction_on a (by simp) (by simp)
theorem add_succl (a b : num) : (succ a) + b = succ (a + b)
:= induction_on b (by simp) (by simp)
add_rewrite add_zerol add_succl
theorem add_comm (a b : num) : a + b = b + a
:= induction_on b (by simp) (by simp)
theorem add_assoc (a b c : num) : (a + b) + c = a + (b + c)
:= induction_on a (by simp) (by simp)
theorem add_left_comm (a b c : num) : a + (b + c) = b + (a + c)
:= left_comm add_comm add_assoc a b c
add_rewrite add_assoc add_comm add_left_comm
theorem mul_zerol (a : num) : zero * a = zero
:= induction_on a (by simp) (by simp)
theorem mul_succl (a b : num) : (succ a) * b = a * b + b
:= induction_on b (by simp) (by simp)
add_rewrite mul_zerol mul_succl
theorem mul_onel (a : num) : (succ zero) * a = a
:= induction_on a (by simp) (by simp)
theorem mul_oner (a : num) : a * (succ zero) = a
:= induction_on a (by simp) (by simp)
add_rewrite mul_onel mul_oner
theorem mul_comm (a b : num) : a * b = b * a
:= induction_on b (by simp) (by simp)
theorem distributer (a b c : num) : a * (b + c) = a * b + a * c
:= induction_on a (by simp) (by simp)
add_rewrite mul_comm distributer
theorem distributel (a b c : num) : (a + b) * c = a * c + b * c
:= induction_on a (by simp) (by simp)
add_rewrite distributel
theorem mul_assoc (a b c : num) : (a * b) * c = a * (b * c)
:= induction_on b (by simp) (by simp)
theorem mul_left_comm (a b c : num) : a * (b * c) = b * (a * c)
:= left_comm mul_comm mul_assoc a b c
add_rewrite mul_assoc mul_left_comm
theorem lt_addr {a b : num} (c : num) : a < b → a + c < b + c
:= assume H : a < b,
induction_on c
(by simp)
(λ (c : num) (iH : a + c < b + c),
have H1 : succ (a + c) < succ (b + c),
from succ_mono_lt iH,
show a + succ c < b + succ c,
from subst (subst H1 (symm (add_succr a c))) (symm (add_succr b c)))
theorem addl_lt {a b c : num} : a + c < b → a < b
:= induction_on c
(assume H : a + zero < b, subst H (add_zeror a))
(λ (c : num) (iH : a + c < b → a < b),
assume H : a + (succ c) < b,
have H1 : succ (a + c) < b,
from subst H (add_succr a c),
have H2 : a + c < b,
from lt_succ H1,
show a < b, from iH H2)
theorem lt_to_nez {a b : num} (H : a < b) : b ≠ zero
:= not_intro (assume N : b = zero,
absurd (subst H N) (not_lt_zero a))
theorem lt_ex1 {a b : num} : a < b → ∃ c, a + (succ c) = b
:= induction_on a
(assume H : zero < b,
have H1 : b ≠ zero, from lt_to_nez H,
have H2 : succ (pre b) = b, from succ_pre b H1,
show ∃ c, zero + (succ c) = b,
from exists_intro (pre b) (by simp))
(λ (a : num) (iH : a < b → ∃ c, a + (succ c) = b),
assume H : succ a < b,
have H1 : a < b, from lt_succ H,
obtain (c : num) (Hc : a + (succ c) = b), from iH H1,
have Hcnz : c ≠ zero,
from not_intro (assume L1 : c = zero,
have Hb : b = a + (succ c), from symm Hc,
have L2 : succ a = b, by simp,
show false, from absurd L2 (lt_to_neq H)),
have Hspc : succ (pre c) = c,
from succ_pre c Hcnz,
show ∃ c, (succ a) + (succ c) = b,
from exists_intro (pre c) (calc (succ a) + (succ (pre c)) = succ (a + c) : by simp
... = a + (succ c) : symm (add_succr _ _)
... = b : Hc ))
theorem lt_ex2 {a b : num} : (∃ c, a + (succ c) = b) → a < b
:= assume Hex : ∃ c, a + (succ c) = b,
obtain (c : num) (Hc : a + (succ c) = b), from Hex,
have H1 : succ (a + c) = b,
from subst Hc (add_succr a c),
have H2 : a + c < b,
from subst (n_lt_succ_n (a + c)) H1,
show a < b,
from addl_lt H2
theorem lt_ex (a b : num) : a < b ↔ ∃ c, a + (succ c) = b
:= iff_intro (assume Hl, lt_ex1 Hl) (assume Hr, lt_ex2 Hr)
theorem lt_to_ex {a b : num} (H : a < b) : ∃ c, a + (succ c) = b
:= lt_ex1 H
theorem ex_to_lt {a b c : num} (H : a + succ c = b) : a < b
:= lt_ex2 (exists_intro c H)
theorem lt_trans {a b c : num} : a < b → b < c → a < c
:= assume H1 H2,
obtain (w1 : num) (Hw1 : a + succ w1 = b), from lt_to_ex H1,
obtain (w2 : num) (Hw2 : b + succ w2 = c), from lt_to_ex H2,
have Hac : a + succ (succ (w1 + w2)) = c,
from calc a + succ (succ (w1 + w2)) = (a + succ w1) + succ w2 : by simp_no_assump
... = b + succ w2 : { Hw1 }
... = c : { Hw2 },
ex_to_lt Hac
theorem strong_induction {P : num → Bool} (H : ∀ n, (∀ m, m < n → P m) → P n) : ∀ a, P a
:= take a : num,
have stronger : P a ∧ ∀ m, m < a → P m,
from induction_on a -- we prove a stronger result by regular induction on a
(have c2 : ∀ m, m < zero → P m,
from λ (m : num) (Hlt : m < zero), absurd_elim (P m) Hlt (not_lt_zero m),
have c1 : P zero,
from H zero c2,
show P zero ∧ ∀ m, m < zero → P m,
from and_intro c1 c2)
(λ (n : num) (iH : P n ∧ ∀ m, m < n → P m),
have iH1 : P n,
from and_eliml iH,
have iH2 : ∀ m, m < n → P m,
from and_elimr iH,
have c2 : ∀ m, m < succ n → P m,
from take m : num, assume Hlt : m < succ n,
or_elim (em (m = n))
(assume Heq : m = n, subst iH1 (symm Heq))
(assume Hne : m ≠ n, iH2 m (lt_succ_ne_to_lt Hlt Hne)),
have c1 : P (succ n),
from H (succ n) c2,
and_intro c1 c2),
show P a,
from and_eliml stronger
definition fact (a : num) : num
:= prim_rec one (λ x n, succ n * x) a
theorem fact_zero : fact zero = one
:= prim_rec_zero one (λ x n : num, succ n * x)
theorem fact_succ (n : num) : fact (succ n) = succ n * fact n
:= prim_rec_succ one (λ x n : num, succ n * x) n
definition exp (a b : num) : num
:= prim_rec one (λ x n, a * x) b
theorem exp_zero (a : num) : exp a zero = one
:= prim_rec_zero one (λ x n, a * x)
theorem exp_succ (a b : num) : exp a (succ b) = a * (exp a b)
:= prim_rec_succ one (λ x n, a * x) b
set_opaque fact true
set_opaque exp true
end
definition num := num::num

BIN
src/builtin/obj/Int.olean
View file

Binary file not shown.

BIN
src/builtin/obj/Nat.olean
View file

Binary file not shown.

BIN
src/builtin/obj/Real.olean
View file

Binary file not shown.

BIN
src/builtin/obj/kernel.olean
View file

Binary file not shown.

BIN
src/builtin/obj/num.olean
View file

Binary file not shown.

BIN
src/builtin/obj/optional.olean
View file

Binary file not shown.

BIN
src/builtin/obj/specialfn.olean
View file

Binary file not shown.

BIN
src/builtin/obj/subtype.olean
View file

Binary file not shown.

BIN
src/builtin/obj/sum.olean
View file

Binary file not shown.

125
src/builtin/optional.lean
View file

@ -1,125 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import macros subtype
using subtype
-- We are encoding the (optional A) as a subset of A → Bool where
-- none is the predicate that is false everywhere
-- some(a) is the predicate that is true only at a
definition optional_pred (A : (Type U)) := (λ p : A → Bool, (∀ x, ¬ p x) ∨ exists_unique p)
definition optional (A : (Type U)) := subtype (A → Bool) (optional_pred A)
namespace optional
theorem some_pred {A : (Type U)} (a : A) : optional_pred A (λ x, x = a)
:= or_intror
(∀ x, ¬ x = a)
(exists_intro a
(and_intro (refl a) (take y, assume H : y ≠ a, H)))
theorem none_pred (A : (Type U)) : optional_pred A (λ x, false)
:= or_introl (take x, not_false_trivial) (exists_unique (λ x, false))
theorem inhab (A : (Type U)) : inhabited (optional A)
:= subtype_inhabited (exists_intro (λ x, false) (none_pred A))
definition none {A : (Type U)} : optional A
:= abst (λ x, false) (inhab A)
definition some {A : (Type U)} (a : A) : optional A
:= abst (λ x, x = a) (inhab A)
definition is_some {A : (Type U)} (n : optional A) := ∃ x : A, some x = n
theorem injectivity {A : (Type U)} {a a' : A} : some a = some a' → a = a'
:= assume Heq : some a = some a',
have eq_reps : (λ x, x = a) = (λ x, x = a'),
from abst_inj (inhab A) (some_pred a) (some_pred a') Heq,
show a = a',
from (congr1 eq_reps a) ◂ (refl a)
theorem distinct {A : (Type U)} (a : A) : some a ≠ none
:= not_intro (assume N : some a = none,
have eq_reps : (λ x, x = a) = (λ x, false),
from abst_inj (inhab A) (some_pred a) (none_pred A) N,
show false,
from (congr1 eq_reps a) ◂ (refl a))
definition value {A : (Type U)} (n : optional A) (H : is_some n) : A
:= ε (inhabited_ex_intro H) (λ x, some x = n)
theorem is_some_some {A : (Type U)} (a : A) : is_some (some a)
:= exists_intro a (refl (some a))
theorem not_is_some_none {A : (Type U)} : ¬ is_some (@none A)
:= not_intro (assume N : is_some (@none A),
obtain (w : A) (Hw : some w = @none A),
from N,
show false,
from absurd Hw (distinct w))
theorem value_some {A : (Type U)} (a : A) (H : is_some (some a)) : value (some a) H = a
:= have eq1 : some (value (some a) H) = some a,
from eps_ax (inhabited_ex_intro H) a (refl (some a)),
show value (some a) H = a,
from injectivity eq1
theorem false_pred {A : (Type U)} {p : A → Bool} (H : ∀ x, ¬ p x) : p = λ x, false
:= funext (λ x, eqf_intro (H x))
theorem singleton_pred {A : (Type U)} {p : A → Bool} {w : A} (H : p w ∧ ∀ y, y ≠ w → ¬ p y) : p = (λ x, x = w)
:= funext (take x, iff_intro
(assume Hpx : p x,
show x = w,
from by_contradiction (assume N : x ≠ w,
show false, from absurd Hpx (and_elimr H x N)))
(assume Heq : x = w,
show p x,
from subst (and_eliml H) (symm Heq)))
theorem dichotomy {A : (Type U)} (n : optional A) : n = none ∨ ∃ a, n = some a
:= have pred : optional_pred A (rep n),
from P_rep n,
show n = none ∨ ∃ a, n = some a,
from or_elim pred
(assume Hl : ∀ x : A, ¬ rep n x,
have rep_n_eq : rep n = λ x, false,
from false_pred Hl,
have rep_none_eq : rep none = λ x, false,
from rep_abst (inhab A) (λ x, false) (none_pred A),
show n = none ∨ ∃ a, n = some a,
from or_introl (rep_inj (trans rep_n_eq (symm rep_none_eq)))
(∃ a, n = some a))
(assume Hr : ∃ x, rep n x ∧ ∀ y, y ≠ x → ¬ rep n y,
obtain (w : A) (Hw : rep n w ∧ ∀ y, y ≠ w → ¬ rep n y),
from Hr,
have rep_n_eq : rep n = λ x, x = w,
from singleton_pred Hw,
have rep_some_eq : rep (some w) = λ x, x = w,
from rep_abst (inhab A) (λ x, x = w) (some_pred w),
have n_eq_some : n = some w,
from rep_inj (trans rep_n_eq (symm rep_some_eq)),
show n = none ∨ ∃ a, n = some a,
from or_intror (n = none)
(exists_intro w n_eq_some))
theorem induction {A : (Type U)} {P : optional A → Bool} (H1 : P none) (H2 : ∀ x, P (some x)) : ∀ n, P n
:= take n, or_elim (dichotomy n)
(assume Heq : n = none,
show P n,
from subst H1 (symm Heq))
(assume Hex : ∃ a, n = some a,
obtain (w : A) (Hw : n = some w),
from Hex,
show P n,
from subst (H2 w) (symm Hw))
set_opaque some true
set_opaque none true
set_opaque is_some true
set_opaque value true
end
set_opaque optional true
set_opaque optional_pred true
definition optional_inhabited := optional::inhab
add_rewrite optional::is_some_some optional::not_is_some_none optional::distinct optional::value_some

64
src/builtin/proof_irrel.lean
View file

@ -1,64 +0,0 @@
import macros
definition has_fixpoint (A : Bool) : Bool
:= ∃ F : (A → A) → A, ∀ f : A → A, F f = f (F f)
theorem eq_arrow (A : Bool) : inhabited A → (A → A) = A
:= assume Hin : inhabited A,
obtain (p : A) (Hp : true), from Hin,
iff_intro
(assume Hl : A → A, p)
(assume Hr : A, (assume H : A, H))
theorem bool_fixpoint (A : Bool) : inhabited A → has_fixpoint A
:= assume Hin : inhabited A,
have Heq1 : (A → A) == A,
from (to_heq (eq_arrow A Hin)),
have Heq2 : A == (A → A),
from hsymm Heq1,
let g1 : A → (A → A) := λ x : A, cast Heq2 x,
g2 : (A → A) → A := λ x : A → A, cast Heq1 x,
Y : (A → A) → A := (λ f : A → A, (λ x : A, f (g1 x x)) (g2 (λ x : A, f (g1 x x)))) in
have R : ∀ f, g1 (g2 f) = f,
from take f : A → A,
calc g1 (g2 f) = cast Heq2 (cast Heq1 f) : refl _
... = cast (htrans Heq1 Heq2) f : cast_trans _ _ _
... = f : cast_eq _ _,
have Fix : (∀ f, Y f = f (Y f)),
from take f : A → A,
let h : A → A := λ x : A, f (g1 x x) in
have H1 : Y f = f (g1 (g2 h) (g2 h)),
from refl (Y f),
have H2 : g1 (g2 h) = h,
from R h,
have H3 : Y f = f (h (g2 h)),
from substp (λ x, Y f = f (x (g2 h))) H1 H2,
have H4 : f (Y f) = f (h (g2 h)),
from refl (f (Y f)),
trans H3 (symm H4),
@exists_intro ((A → A) → A) (λ Y, ∀ f, Y f = f (Y f)) Y Fix
theorem proof_irrel_new (A : Bool) (p1 p2 : A) : p1 = p2
:= have H1 : inhabited A,
from inhabited_intro p1,
obtain (Y : (A → A) → A) (HY : ∀ f : A → A, Y f = f (Y f)), from bool_fixpoint A H1,
let h : A → A := (λ x : A, if x = p1 then p2 else p1) in
have HYh : Y h = h (Y h),
from HY h,
or_elim (em (Y h = p1))
(assume Heq : Y h = p1,
have Heq1 : h (Y h) = p2,
from calc h (Y h) = if Y h = p1 then p2 else p1 : refl _
... = if true then p2 else p1 : { eqt_intro Heq }
... = p2 : if_true _ _,
calc p1 = Y h : symm Heq
... = h (Y h) : HYh
... = p2 : Heq1)
(assume Hne : Y h ≠ p1,
have Heq1 : h (Y h) = p1,
from calc h (Y h) = if Y h = p1 then p2 else p1 : refl _
... = if false then p2 else p1 : { eqf_intro Hne }
... = p1 : if_false _ _,
have Heq2 : Y h = p1,
from trans HYh Heq1,
absurd_elim (p1 = p2) Heq2 Hne)

118
src/builtin/quotient.lean
View file

@ -1,118 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import macros
import subtype
definition reflexive {A : Type} (r : A → A → Bool) := ∀ a, r a a
definition symmetric {A : Type} (r : A → A → Bool) := ∀ a b, r a b → r b a
definition transitive {A : Type} (r : A → A → Bool) := ∀ a b c, r a b → r b c → r a c
definition equivalence {A : Type} (r : A → A → Bool) := reflexive r ∧ symmetric r ∧ transitive r
namespace quotient
definition member {A : Type} (a : A) (S : A → Bool) := S a
infix 50 ∈ : member
definition eqc {A : Type} (a : A) (r : A → A → Bool) := λ b, r a b
theorem eqc_mem {A : Type} {a b : A} (r : A → A → Bool) : r a b → b ∈ eqc a r
:= assume H : r a b, H
theorem eqc_r {A : Type} {a b : A} (r : A → A → Bool) : b ∈ (eqc a r) → r a b
:= assume H : b ∈ (eqc a r), H
theorem eqc_eq {A : Type} {a b : A} {r : A → A → Bool} : equivalence r → r a b → (eqc a r) = (eqc b r)
:= assume (Heqv : equivalence r) (Hrab : r a b),
have Hsym : symmetric r,
from and_eliml (and_elimr Heqv),
have Htrans : transitive r,
from and_elimr (and_elimr Heqv),
funext (λ x : A,
iff_intro
(assume Hin : x ∈ (eqc a r),
have Hb : r b x,
from Htrans b a x (Hsym a b Hrab) (eqc_r r Hin),
eqc_mem r Hb)
(assume Hin : x ∈ (eqc b r),
have Ha : r a x,
from Htrans a b x Hrab (eqc_r r Hin),
eqc_mem r Ha))
definition rep_i {A : Type} (a : A) (r : A → A → Bool) : A
:= ε (inhabited_intro a) (eqc a r)
theorem r_rep {A : Type} (a : A) (r : A → A → Bool) : reflexive r → r a (rep_i a r)
:= assume R : reflexive r,
eps_ax (inhabited_intro a) a (R a)
theorem rep_eq {A : Type} {a b : A} {r : A → A → Bool} : equivalence r → r a b → rep_i a r = rep_i b r
:= assume (Heqv : equivalence r) (Hrab : r a b),
have Heq : eqc a r = eqc b r,
from eqc_eq Heqv Hrab,
have Hin : inhabited_intro a = inhabited_intro b,
from proof_irrel (inhabited_intro a) (inhabited_intro b),
calc rep_i a r = ε (inhabited_intro a) (eqc a r) : refl _
... = ε (inhabited_intro b) (eqc a r) : { Hin }
... = ε (inhabited_intro b) (eqc b r) : { Heq }
... = rep_i b r : refl _
theorem rep_rep {A : Type} (a : A) {r : A → A → Bool} : equivalence r → rep_i (rep_i a r) r = rep_i a r
:= assume Heqv : equivalence r,
have Hrefl : reflexive r,
from and_eliml Heqv,
have Hsym : symmetric r,
from and_eliml (and_elimr Heqv),
have Hr : r (rep_i a r) a,
from Hsym _ _ (r_rep a r Hrefl),
rep_eq Heqv Hr
definition quotient {A : Type} {r : A → A → Bool} (e : equivalence r)
:= subtype A (λ a, rep_i a r = a)
theorem inhab {A : Type} (Hin : inhabited A) {r : A → A → Bool} (e : equivalence r) : inhabited (quotient e)
:= obtain (a : A) (Ht : true), from Hin,
subtype::subtype_inhabited (exists_intro (rep_i a r) (rep_rep a e))
definition abst {A : Type} (a : A) {r : A → A → Bool} (e : equivalence r) : quotient e
:= subtype::abst (rep_i a r) (inhab (inhabited_intro a) e)
notation 65 [ _ ] _ : abst
definition rep {A : Type} {r : A → A → Bool} {e : equivalence r} (q : quotient e) : A
:= subtype::rep q
theorem quotient_eq {A : Type} (a b : A) {r : A → A → Bool} (e : equivalence r) : r a b → [a]e = [b]e
:= assume Hrab : r a b,
have Heq_a : [a]e = subtype::abst (rep_i a r) (inhab (inhabited_intro a) e),
from refl _,
have Heq_b : [b]e = subtype::abst (rep_i b r) (inhab (inhabited_intro b) e),
from refl _,
have Heq_r : rep_i a r = rep_i b r,
from rep_eq e Hrab,
have Heq_pr : inhabited_intro a = inhabited_intro b,
from proof_irrel _ _,
calc [a]e = subtype::abst (rep_i a r) (inhab (inhabited_intro a) e) : Heq_a
... = subtype::abst (rep_i b r) (inhab (inhabited_intro a) e) : { Heq_r }
... = subtype::abst (rep_i b r) (inhab (inhabited_intro b) e) : { Heq_pr }
... = [b]e : symm Heq_b
theorem quotient_rep {A : Type} (a : A) {r : A → A → Bool} (e : equivalence r) : r a (rep ([a]e))
:= have Heq1 : [a]e = subtype::abst (rep_i a r) (inhab (inhabited_intro a) e),
from refl ([a]e),
have Heq2 : rep ([a]e) = @rep A r e (subtype::abst (rep_i a r) (inhab (inhabited_intro a) e)),
from congr2 (λ x : quotient e, @rep A r e x) Heq1,
have Heq3 : @rep A r e (subtype::abst (rep_i a r) (inhab (inhabited_intro a) e)) = (rep_i a r),
from subtype::rep_abst (inhab (inhabited_intro a) e) (rep_i a r) (rep_rep a e),
have Heq4 : rep ([a]e) = (rep_i a r),
from trans Heq2 Heq3,
have Hr : r a (rep_i a r),
from r_rep a r (and_eliml e),
subst Hr (symm Heq4)
set_opaque eqc true
set_opaque rep_i true
set_opaque quotient true
set_opaque abst true
set_opaque rep true
end
definition quotient {A : Type} {r : A → A → Bool} (e : equivalence r) := quotient::quotient e

36
src/builtin/repl.lua
View file

@ -1,36 +0,0 @@
-- Simple read-eval-print loop for Lean Lua frontend
local function trim(s)
return s:gsub('^%s+', ''):gsub('%s+$', '')
end
local function show_results(...)
if select('#', ...) > 1 then
print(select(2, ...))
end
end
print([[Type 'exit' to exit.]])
repeat
io.write'lean > '
local s = io.read()
if s == nil then print(); break end
if trim(s) == 'exit' then break end
local f, err = loadstring(s, 'stdin')
if err then
f = loadstring('return (' .. s .. ')', 'stdin')
end
if f then
local ok, err = pcall(f)
if not ok then
if is_exception(err) then
print(err:what())
else
print(err)
end
else
if err then print(err) end
end
else
print(err)
end
until false

19
src/builtin/specialfn.lean
View file

@ -1,19 +0,0 @@
import Real.
variable exp : Real → Real.
variable log : Real → Real.
variable pi : Real.
alias π : pi.
variable sin : Real → Real.
definition cos x := sin (x - π / 2).
definition tan x := sin x / cos x.
definition cot x := cos x / sin x.
definition sec x := 1 / cos x.
definition csc x := 1 / sin x.
definition sinh x := (1 - exp (-2 * x)) / (2 * exp (- x)).
definition cosh x := (1 + exp (-2 * x)) / (2 * exp (- x)).
definition tanh x := sinh x / cosh x.
definition coth x := cosh x / sinh x.
definition sech x := 1 / cosh x.
definition csch x := 1 / sinh x.

52
src/builtin/subtype.lean
View file

@ -1,52 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import macros
-- Simulate "subtypes" using Sigma types and proof irrelevance
definition subtype (A : (Type U)) (P : A → Bool) := sig x, P x
namespace subtype
definition rep {A : (Type U)} {P : A → Bool} (a : subtype A P) : A
:= proj1 a
definition abst {A : (Type U)} {P : A → Bool} (r : A) (H : inhabited (subtype A P)) : subtype A P
:= ε H (λ a, rep a = r)
theorem subtype_inhabited {A : (Type U)} {P : A → Bool} (H : ∃ x, P x) : inhabited (subtype A P)
:= obtain (w : A) (Hw : P w), from H,
inhabited_intro (pair w Hw)
theorem P_rep {A : (Type U)} {P : A → Bool} (a : subtype A P) : P (rep a)
:= proj2 a
theorem rep_inj {A : (Type U)} {P : A → Bool} {a b : subtype A P} (H : rep a = rep b) : a = b
:= pairext _ _ H (hproof_irrel (proj2 a) (proj2 b))
theorem ex_abst {A : (Type U)} {P : A → Bool} {r : A} (H : P r) : ∃ a, rep a = r
:= exists_intro (pair r H) (refl r)
theorem abst_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) (a : subtype A P)
: abst (rep a) H = a
:= let s1 : rep (abst (rep a) H) = rep a :=
@eps_ax (subtype A P) H (λ x, rep x = rep a) a (refl (rep a))
in rep_inj s1
theorem rep_abst {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) : ∀ r, P r → rep (abst r H) = r
:= take r, assume Hl : P r,
@eps_ax (subtype A P) H (λ x, rep x = r) (pair r Hl) (refl r)
theorem abst_inj {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) {r r' : A} :
P r → P r' → abst r H = abst r' H → r = r'
:= assume Hr Hr' Heq,
calc r = rep (abst r H) : symm (rep_abst H r Hr)
... = rep (abst r' H) : { Heq }
... = r' : rep_abst H r' Hr'
theorem ex_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) :
∀ a, ∃ r, abst r H = a ∧ P r
:= take a, exists_intro (rep a) (and_intro (abst_rep H a) (proj2 a))
set_opaque rep true
set_opaque abst true
end -- namespace subtype
set_opaque subtype true

137
src/builtin/sum.lean
View file

@ -1,137 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import macros subtype optional
using subtype
using optional
-- We are encoding the (sum A B) as a subtype of (optional A) # (optional B), where
-- (proj1 n = none) ≠ (proj2 n = none)
definition sum_pred (A B : (Type U)) := λ p : (optional A) # (optional B), (proj1 p = none) ≠ (proj2 p = none)
definition sum (A B : (Type U)) := subtype ((optional A) # (optional B)) (sum_pred A B)
namespace sum
theorem inl_pred {A : (Type U)} (a : A) (B : (Type U)) : sum_pred A B (pair (some a) none)
:= not_intro
(assume N : (some a = none) = (none = (@none B)),
have eq : some a = none,
from (symm N) ◂ (refl (@none B)),
show false,
from absurd eq (distinct a))
theorem inr_pred (A : (Type U)) {B : (Type U)} (b : B) : sum_pred A B (pair none (some b))
:= not_intro
(assume N : (none = (@none A)) = (some b = none),
have eq : some b = none,
from N ◂ (refl (@none A)),
show false,
from absurd eq (distinct b))
theorem inhabl {A : (Type U)} (H : inhabited A) (B : (Type U)) : inhabited (sum A B)
:= inhabited_elim H (take w : A,
subtype_inhabited (exists_intro (pair (some w) none) (inl_pred w B)))
theorem inhabr (A : (Type U)) {B : (Type U)} (H : inhabited B) : inhabited (sum A B)
:= inhabited_elim H (take w : B,
subtype_inhabited (exists_intro (pair none (some w)) (inr_pred A w)))
definition inl {A : (Type U)} (a : A) (B : (Type U)) : sum A B
:= abst (pair (some a) none) (inhabl (inhabited_intro a) B)
definition inr (A : (Type U)) {B : (Type U)} (b : B) : sum A B
:= abst (pair none (some b)) (inhabr A (inhabited_intro b))
theorem inl_inj {A B : (Type U)} {a1 a2 : A} : inl a1 B = inl a2 B → a1 = a2
:= assume Heq : inl a1 B = inl a2 B,
have eq1 : inl a1 B = abst (pair (some a1) none) (inhabl (inhabited_intro a1) B),
from refl (inl a1 B),
have eq2 : inl a2 B = abst (pair (some a2) none) (inhabl (inhabited_intro a1) B),
from subst (refl (inl a2 B)) (proof_irrel (inhabl (inhabited_intro a2) B) (inhabl (inhabited_intro a1) B)),
have rep_eq : (pair (some a1) none) = (pair (some a2) none),
from abst_inj (inhabl (inhabited_intro a1) B) (inl_pred a1 B) (inl_pred a2 B) (trans (trans (symm eq1) Heq) eq2),
show a1 = a2,
from optional::injectivity
(calc some a1 = proj1 (pair (some a1) (@none B)) : refl (some a1)
... = proj1 (pair (some a2) (@none B)) : proj1_congr rep_eq
... = some a2 : refl (some a2))
theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
:= assume Heq : inr A b1 = inr A b2,
have eq1 : inr A b1 = abst (pair none (some b1)) (inhabr A (inhabited_intro b1)),
from refl (inr A b1),
have eq2 : inr A b2 = abst (pair none (some b2)) (inhabr A (inhabited_intro b1)),
from subst (refl (inr A b2)) (proof_irrel (inhabr A (inhabited_intro b2)) (inhabr A (inhabited_intro b1))),
have rep_eq : (pair none (some b1)) = (pair none (some b2)),
from abst_inj (inhabr A (inhabited_intro b1)) (inr_pred A b1) (inr_pred A b2) (trans (trans (symm eq1) Heq) eq2),
show b1 = b2,
from optional::injectivity
(calc some b1 = proj2 (pair (@none A) (some b1)) : refl (some b1)
... = proj2 (pair (@none A) (some b2)) : proj2_congr rep_eq
... = some b2 : refl (some b2))
theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
:= not_intro (assume N : inl a B = inr A b,
have eq1 : inl a B = abst (pair (some a) none) (inhabl (inhabited_intro a) B),
from refl (inl a B),
have eq2 : inr A b = abst (pair none (some b)) (inhabl (inhabited_intro a) B),
from subst (refl (inr A b)) (proof_irrel (inhabr A (inhabited_intro b)) (inhabl (inhabited_intro a) B)),
have rep_eq : (pair (some a) none) = (pair none (some b)),
from abst_inj (inhabl (inhabited_intro a) B) (inl_pred a B) (inr_pred A b) (trans (trans (symm eq1) N) eq2),
show false,
from absurd (proj1_congr rep_eq) (optional::distinct a))
theorem dichotomy {A B : (Type U)} (n : sum A B) : (∃ a, n = inl a B) ∨ (∃ b, n = inr A b)
:= let pred : (proj1 (rep n) = none) ≠ (proj2 (rep n) = none) := P_rep n
in or_elim (em (proj1 (rep n) = none))
(assume Heq : proj1 (rep n) = none,
have neq_none : ¬ proj2 (rep n) = (@none B),
from (symm (not_iff_elim (ne_symm pred))) ◂ Heq,
have ex_some : ∃ b, proj2 (rep n) = some b,
from resolve1 (optional::dichotomy (proj2 (rep n))) neq_none,
obtain (b : B) (Hb : proj2 (rep n) = some b),
from ex_some,
show (∃ a, n = inl a B) ∨ (∃ b, n = inr A b),
from or_intror (∃ a, n = inl a B)
(have rep_eq : rep n = pair none (some b),
from pairext_proj Heq Hb,
have rep_inr : rep (inr A b) = pair none (some b),
from rep_abst (inhabr A (inhabited_intro b)) (pair none (some b)) (inr_pred A b),
have n_eq_inr : n = inr A b,
from rep_inj (trans rep_eq (symm rep_inr)),
show (∃ b, n = inr A b),
from exists_intro b n_eq_inr))
(assume Hne : ¬ proj1 (rep n) = none,
have eq_none : proj2 (rep n) = (@none B),
from (not_iff_elim pred) ◂ Hne,
have ex_some : ∃ a, proj1 (rep n) = some a,
from resolve1 (optional::dichotomy (proj1 (rep n))) Hne,
obtain (a : A) (Ha : proj1 (rep n) = some a),
from ex_some,
show (∃ a, n = inl a B) ∨ (∃ b, n = inr A b),
from or_introl
(have rep_eq : rep n = pair (some a) none,
from pairext_proj Ha eq_none,
have rep_inl : rep (inl a B) = pair (some a) none,
from rep_abst (inhabl (inhabited_intro a) B) (pair (some a) none) (inl_pred a B),
have n_eq_inl : n = inl a B,
from rep_inj (trans rep_eq (symm rep_inl)),
show ∃ a, n = inl a B,
from exists_intro a n_eq_inl)
(∃ b, n = inr A b))
theorem induction {A B : (Type U)} {P : sum A B → Bool} (H1 : ∀ a, P (inl a B)) (H2 : ∀ b, P (inr A b)) : ∀ n, P n
:= take n, or_elim (sum::dichotomy n)
(assume Hex : ∃ a, n = inl a B,
obtain (a : A) (Ha : n = inl a B), from Hex,
show P n,
from subst (H1 a) (symm Ha))
(assume Hex : ∃ b, n = inr A b,
obtain (b : B) (Hb : n = inr A b), from Hex,
show P n,
from subst (H2 b) (symm Hb))
set_opaque inl true
set_opaque inr true
end
set_opaque sum_pred true
set_opaque sum true

91
src/builtin/sum2.lean
View file

@ -1,91 +0,0 @@
import macros tactic
namespace sum
definition sum (A B : Type) := sig b : Bool, if b then A else B
theorem sum_if_l (A B : Type) : A == if true then A else B
:= by simp
theorem sum_if_r (A B : Type) : B == if false then A else B
:= by simp
definition inl {A : Type} (a : A) (B : Type) : sum A B
:= pair true (cast (sum_if_l A B) a)
definition inr (A : Type) {B : Type} (b : B) : sum A B
:= pair false (cast (sum_if_r A B) b)
theorem cast_eq_cast {A B1 B2 : Type} {H1 : A == B1} {H2 : A == B2} {a1 a2 : A} (H : cast H1 a1 == cast H2 a2) : a1 = a2
:= have S1 : cast H1 a1 == a1,
from cast_heq H1 a1,
have S2 : cast H2 a2 == a2,
from cast_heq H2 a2,
to_eq (htrans (htrans (hsymm S1) H) S2)
theorem inl_inj {A B : Type} {a1 a2 : A} : inl a1 B = inl a2 B → a1 = a2
:= assume H : inl a1 B = inl a2 B,
have H1 : (cast _ a1) == (cast _ a2),
from hproj2_congr H,
cast_eq_cast H1
theorem inr_inj {A B : Type} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
:= assume H : inr A b1 = inr A b2,
have H1 : (cast _ b1) == (cast _ b2),
from hproj2_congr H,
cast_eq_cast H1
theorem distinct {A B : Type} (a : A) (b : B) : inl a B ≠ inr A b
:= not_intro (assume N : inl a B = inr A b,
absurd (proj1_congr N) true_ne_false)
theorem dichotomy {A B : Type} (n : sum A B) : (∃ a, n = inl a B) ∨ (∃ b, n = inr A b)
:= or_elim (em (proj1 n))
(assume H : proj1 n,
have H1n : proj1 n = true,
from eqt_intro H,
have Haux : (if (proj1 n) then A else B) = A,
from calc (if (proj1 n) then A else B) = if true then A else B : { H1n }
... = A : if_true _ _,
let a : A := cast (to_heq Haux) (proj2 n) in
have H1i : proj1 (inl a B) = true,
from refl _,
have H2n : proj2 n == a,
from hsymm (cast_heq (to_heq Haux) (proj2 n)),
have H2i : proj2 (inl a B) == a,
from cast_heq (sum_if_l A B) a,
have Heq : n = (inl a B),
from pairext n (inl a B) (trans H1n (symm H1i)) (htrans H2n (hsymm H2i)),
or_introl (exists_intro a Heq) (∃ b, n = inr A b))
(assume H : ¬ proj1 n,
have H1n : proj1 n = false,
from eqf_intro H,
have Haux : (if (proj1 n) then A else B) = B,
from calc (if (proj1 n) then A else B) = if false then A else B : { H1n }
... = B : if_false _ _,
let b : B := cast (to_heq Haux) (proj2 n) in
have H1i : proj1 (inr A b) = false,
from refl _,
have H2n : proj2 n == b,
from hsymm (cast_heq (to_heq Haux) (proj2 n)),
have H2i : proj2 (inr A b) == b,
from cast_heq (sum_if_r A B) b,
have Heq : n = (inr A b),
from pairext n (inr A b) (trans H1n (symm H1i)) (htrans H2n (hsymm H2i)),
or_intror (∃ a, n = inl a B) (exists_intro b Heq))
theorem induction {A B : Type} {P : sum A B → Bool} (H1 : ∀ a, P (inl a B)) (H2 : ∀ b, P (inr A b)) : ∀ n, P n
:= take n, or_elim (dichotomy n)
(assume Hex : ∃ a, n = inl a B,
obtain (a : A) (Ha : n = inl a B), from Hex,
show P n,
from subst (H1 a) (symm Ha))
(assume Hex : ∃ b, n = inr A b,
obtain (b : B) (Hb : n = inr A b), from Hex,
show P n,
from subst (H2 b) (symm Hb))
set_opaque inl true
set_opaque inr true
set_opaque sum true
end
definition sum := sum::sum

59
src/builtin/tactic.lua
View file

@ -1,59 +0,0 @@
-- Define macros for simplifying Tactic creation
local unary_combinator = function (name, fn) tactic_macro(name, { macro_arg.Tactic }, function (env, t) return fn(t) end) end
local nary_combinator = function (name, fn) tactic_macro(name, { macro_arg.Tactics }, function (env, ts) return fn(unpack(ts)) end) end
local const_tactic = function (name, fn) tactic_macro(name, {}, function (env) return fn() end) end
unary_combinator("Repeat", Repeat)
unary_combinator("Try", Try)
nary_combinator("Then", Then)
nary_combinator("OrElse", OrElse)
const_tactic("exact", assumption_tac)
const_tactic("trivial", trivial_tac)
const_tactic("id", id_tac)
const_tactic("absurd", absurd_tac)
const_tactic("conj_hyp", conj_hyp_tac)
const_tactic("disj_hyp", disj_hyp_tac)
const_tactic("unfold_all", unfold_tac)
const_tactic("beta", beta_tac)
tactic_macro("apply", { macro_arg.Expr }, function (env, e) return apply_tac(e) end)
tactic_macro("unfold", { macro_arg.Id }, function (env, id) return unfold_tac(id) end)
tactic_macro("simp", { macro_arg.Ids },
function (env, ids)
if #ids == 0 then
ids[1] = "default"
end
return simp_tac(ids)
end
)
tactic_macro("simp_no_assump", { macro_arg.Ids },
function (env, ids)
if #ids == 0 then
ids[1] = "default"
end
return simp_tac(ids, options({"simp_tac", "assumptions"}, false))
end
)
-- Create a 'bogus' tactic that consume all goals, but it does not create a valid proof.
-- This tactic is useful for momentarily ignoring/skipping a "hole" in a big proof.
-- Remark: the kernel will not accept a proof built using this tactic.
skip_tac = tactic(function (env, ios, s)
local gs = s:goals()
local pb = s:proof_builder()
local buggy_pr = mk_constant("invalid proof built using skip tactic")
local new_pb =
function(m, a)
-- We provide a "fake/incorrect" proof for all goals in gs
local new_m = proof_map(m) -- Copy proof map m
for n, g in gs:pairs() do
new_m:insert(n, buggy_pr)
end
return pb(new_m, a)
end
local new_gs = {}
return proof_state(s, goals(new_gs), proof_builder(new_pb))
end)
const_tactic("skip", function() return skip_tac end)

31
src/builtin/template.lua
View file

@ -1,31 +0,0 @@
-- Parse a template expression string 'str'.
-- The string 'str' may contain placeholders of the form '% i', where 'i' is a numeral.
-- The placeholders are replaced with values from the array 'arg_array'.
local arg_array = {}
-- We implement this feature using macros available in Lean.
macro("%",
{ macro_arg.Int },
function (env, i)
if i <= 0 then
error("invalid template argument reference %" .. i .. ", first argument is 1")
elseif i > #arg_array then
error("invalid template argument reference %" .. i .. ", only " .. tostring(#arg_array) .. " argument(s) were provided")
else
return arg_array[i]
end
end
)
-- Parse a template.
-- Example:
-- r = parse_template("%1 + %2 + %1", {Const("a"), Const("b")})
-- print(r)
-- >> a + b + a
function parse_template(str, args, env, opts, fmt)
assert(type(str) == "string")
assert(type(args) == "table")
assert(env == nil or is_environment(env))
arg_array = args
return parse_lean(str, env, opts, fmt)
end

16
src/builtin/util.lua
View file

@ -1,16 +0,0 @@
-- Extra useful functions
-- Create sequence of expressions.
-- Examples:
-- local a, b, c = Consts("a,b,c")
-- We can use ';', ' ', ',', tabs ad line breaks for separating the constant names
-- local a, b, c = Consts("a b c")
function Consts(s)
local r = {}
local i = 1
for c in string.gmatch(s, '[^ ,;\t\n]+') do
r[i] = Const(c)
i = i + 1
end
return unpack(r)
end