diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7efd69f9e..8c3c3c506 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -237,7 +237,6 @@ endif() set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage") set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS}) add_subdirectory(shell) -# add_subdirectory(builtin) add_subdirectory(emacs) add_subdirectory(tests/util) diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt deleted file mode 100644 index 6e6c97b62..000000000 --- a/src/builtin/CMakeLists.txt +++ /dev/null @@ -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" "") diff --git a/src/builtin/Int.lean b/src/builtin/Int.lean deleted file mode 100644 index fe533c68e..000000000 --- a/src/builtin/Int.lean +++ /dev/null @@ -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 \ No newline at end of file diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean deleted file mode 100644 index 94c540df3..000000000 --- a/src/builtin/Nat.lean +++ /dev/null @@ -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 \ No newline at end of file diff --git a/src/builtin/README.md b/src/builtin/README.md deleted file mode 100644 index c5ab6025c..000000000 --- a/src/builtin/README.md +++ /dev/null @@ -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. - - diff --git a/src/builtin/Real.lean b/src/builtin/Real.lean deleted file mode 100644 index 45981271f..000000000 --- a/src/builtin/Real.lean +++ /dev/null @@ -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 diff --git a/src/builtin/bin.lean b/src/builtin/bin.lean deleted file mode 100644 index a2fbb8edb..000000000 --- a/src/builtin/bin.lean +++ /dev/null @@ -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 diff --git a/src/builtin/builtin.cpp b/src/builtin/builtin.cpp deleted file mode 100644 index 0fc8b1a7c..000000000 --- a/src/builtin/builtin.cpp +++ /dev/null @@ -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() {} -} diff --git a/src/builtin/dia.lean b/src/builtin/dia.lean deleted file mode 100644 index 5d22841ed..000000000 --- a/src/builtin/dia.lean +++ /dev/null @@ -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)) \ No newline at end of file diff --git a/src/builtin/find.lua b/src/builtin/find.lua deleted file mode 100644 index 8814ec37e..000000000 --- a/src/builtin/find.lua +++ /dev/null @@ -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 -) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean deleted file mode 100644 index 7e06e7a93..000000000 --- a/src/builtin/kernel.lean +++ /dev/null @@ -1,1083 +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 tactic - -universe U ≥ 1 -definition TypeU := (Type U) - --- create default rewrite rule set -(* mk_rewrite_rule_set() *) - -variable Bool : Type - --- Reflexivity for heterogeneous equality --- We use universe U+1 in heterogeneous equality axioms because we want to be able --- to state the equality between A and B of (Type U) -axiom hrefl {A : (Type U+1)} (a : A) : a == a - --- Homogeneous equality -definition eq {A : (Type U)} (a b : A) := a == b -infix 50 = : eq - -theorem refl {A : (Type U)} (a : A) : a = a -:= hrefl a - -theorem heq_eq {A : (Type U)} (a b : A) : (a == b) = (a = b) -:= refl (a == b) - -definition true : Bool -:= (λ x : Bool, x) = (λ x : Bool, x) - -theorem trivial : true -:= refl (λ x : Bool, x) - -set_opaque true true - -definition false : Bool -:= ∀ x : Bool, x - -alias ⊤ : true -alias ⊥ : false - -definition not (a : Bool) := a → false -notation 40 ¬ _ : not - -definition or (a b : Bool) -:= ∀ c : Bool, (a → c) → (b → c) → c -infixr 30 || : or -infixr 30 \/ : or -infixr 30 ∨ : or - -definition and (a b : Bool) -:= ∀ c : Bool, (a → b → c) → c -infixr 35 && : and -infixr 35 /\ : and -infixr 35 ∧ : and - -definition implies (a b : Bool) := a → b - -definition neq {A : (Type U)} (a b : A) := ¬ (a = b) -infix 50 ≠ : neq - -theorem a_neq_a_elim {A : (Type U)} {a : A} (H : a ≠ a) : false -:= H (refl a) - -definition iff (a b : Bool) := a = b -infixr 25 <-> : iff -infixr 25 ↔ : iff - -theorem not_intro {a : Bool} (H : a → false) : ¬ a -:= H - -theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false -:= H2 H1 - --- The Lean parser has special treatment for the constant exists. --- It allows us to write --- exists x y : A, P x y and ∃ x y : A, P x y --- as syntax sugar for --- exists A (fun x : A, exists A (fun y : A, P x y)) --- That is, it treats the exists as an extra binder such as fun and forall. --- It also provides an alias (Exists) that should be used when we --- want to treat exists as a constant. -definition Exists (A : (Type U)) (P : A → Bool) -:= ¬ (∀ x, ¬ (P x)) - -definition exists_unique {A : (Type U)} (p : A → Bool) -:= ∃ x, p x ∧ ∀ y, y ≠ x → ¬ p y - -theorem false_elim (a : Bool) (H : false) : a -:= H a - -set_opaque false true - -theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a -:= assume Ha : a, absurd (H1 Ha) H2 - -theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a -:= assume Hnb : ¬ b, mt H Hnb - -theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b -:= false_elim b (absurd H1 H2) - -theorem or_introl {a : Bool} (H : a) (b : Bool) : a ∨ b -:= take c : Bool, - assume (H1 : a → c) (H2 : b → c), - H1 H - -theorem or_intror {b : Bool} (a : Bool) (H : b) : a ∨ b -:= take c : Bool, - assume (H1 : a → c) (H2 : b → c), - H2 H - -theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c -:= H1 c H2 H3 - -theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b -:= H1 b (assume Ha : a, absurd_elim b Ha H2) (assume Hb : b, Hb) - -theorem resolve2 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ b) : a -:= H1 a (assume Ha : a, Ha) (assume Hb : b, absurd_elim a Hb H2) - -theorem or_flip {a b : Bool} (H : a ∨ b) : b ∨ a -:= take c : Bool, - assume (H1 : b → c) (H2 : a → c), - H c H2 H1 - -theorem and_intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b -:= take c : Bool, - assume H : a → b → c, - H H1 H2 - -theorem and_eliml {a b : Bool} (H : a ∧ b) : a -:= H a (assume (Ha : a) (Hb : b), Ha) - -theorem and_elimr {a b : Bool} (H : a ∧ b) : b -:= H b (assume (Ha : a) (Hb : b), Hb) - -axiom subst {A : (Type U)} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b - --- Alias for subst where we provide P explicitly, but keep A,a,b implicit -theorem substp {A : (Type U)} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b -:= subst H1 H2 - -theorem symm {A : (Type U)} {a b : A} (H : a = b) : b = a -:= subst (refl a) H - -theorem trans {A : (Type U)} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c -:= subst H1 H2 - -theorem hcongr1 {A : (Type U)} {B : A → (Type U)} {f g : ∀ x, B x} (H : f = g) (a : A) : f a = g a -:= substp (fun h, f a = h a) (refl (f a)) H - -theorem congr1 {A B : (Type U)} {f g : A → B} (H : f = g) (a : A) : f a = g a -:= hcongr1 H a - -theorem congr2 {A B : (Type U)} {a b : A} (f : A → B) (H : a = b) : f a = f b -:= substp (fun x : A, f a = f x) (refl (f a)) H - -theorem congr {A B : (Type U)} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b -:= subst (congr2 f H2) (congr1 H1 b) - -theorem true_ne_false : ¬ true = false -:= assume H : true = false, - subst trivial H - -theorem absurd_not_true (H : ¬ true) : false -:= absurd trivial H - -theorem not_false_trivial : ¬ false -:= assume H : false, H - --- "equality modus pones" -theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b -:= subst H2 H1 - -infixl 100 <| : eqmp -infixl 100 ◂ : eqmp - -theorem eqmpr {a b : Bool} (H1 : a = b) (H2 : b) : a -:= (symm H1) ◂ H2 - -theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c -:= assume Ha, H2 (H1 Ha) - -theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c -:= assume Ha, H2 ◂ (H1 Ha) - -theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c -:= assume Ha, H2 (H1 ◂ Ha) - -theorem to_eq {A : (Type U)} {a b : A} (H : a == b) : a = b -:= (heq_eq a b) ◂ H - -theorem to_heq {A : (Type U)} {a b : A} (H : a = b) : a == b -:= (symm (heq_eq a b)) ◂ H - -theorem iff_eliml {a b : Bool} (H : a ↔ b) : a → b -:= (λ Ha : a, eqmp H Ha) - -theorem iff_elimr {a b : Bool} (H : a ↔ b) : b → a -:= (λ Hb : b, eqmpr H Hb) - -theorem ne_symm {A : (Type U)} {a b : A} (H : a ≠ b) : b ≠ a -:= assume H1 : b = a, H (symm H1) - -theorem eq_ne_trans {A : (Type U)} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c -:= subst H2 (symm H1) - -theorem ne_eq_trans {A : (Type U)} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c -:= subst H1 H2 - -theorem eqt_elim {a : Bool} (H : a = true) : a -:= (symm H) ◂ trivial - -theorem eqf_elim {a : Bool} (H : a = false) : ¬ a -:= not_intro (λ Ha : a, H ◂ Ha) - -theorem heqt_elim {a : Bool} (H : a == true) : a -:= eqt_elim (to_eq H) - -axiom boolcomplete (a : Bool) : a = true ∨ a = false - -theorem case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a -:= or_elim (boolcomplete a) - (assume Ht : a = true, subst H1 (symm Ht)) - (assume Hf : a = false, subst H2 (symm Hf)) - -theorem em (a : Bool) : a ∨ ¬ a -:= or_elim (boolcomplete a) - (assume Ht : a = true, or_introl (eqt_elim Ht) (¬ a)) - (assume Hf : a = false, or_intror a (eqf_elim Hf)) - -theorem boolcomplete_swapped (a : Bool) : a = false ∨ a = true -:= case (λ x, x = false ∨ x = true) - (or_intror (true = false) (refl true)) - (or_introl (refl false) (false = true)) - a - -theorem not_true : (¬ true) = false -:= let aux : ¬ (¬ true) = true - := assume H : (¬ true) = true, - absurd_not_true (subst trivial (symm H)) - in resolve1 (boolcomplete (¬ true)) aux - -theorem not_false : (¬ false) = true -:= let aux : ¬ (¬ false) = false - := assume H : (¬ false) = false, - subst not_false_trivial H - in resolve1 (boolcomplete_swapped (¬ false)) aux - -add_rewrite not_true not_false - -theorem not_not_eq (a : Bool) : (¬ ¬ a) = a -:= case (λ x, (¬ ¬ x) = x) - (calc (¬ ¬ true) = (¬ false) : { not_true } - ... = true : not_false) - (calc (¬ ¬ false) = (¬ true) : { not_false } - ... = false : not_true) - a - -add_rewrite not_not_eq - -theorem not_neq {A : (Type U)} (a b : A) : ¬ (a ≠ b) ↔ a = b -:= not_not_eq (a = b) - -add_rewrite not_neq - -theorem not_neq_elim {A : (Type U)} {a b : A} (H : ¬ (a ≠ b)) : a = b -:= (not_neq a b) ◂ H - -theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a -:= (not_not_eq a) ◂ H - -theorem not_imp_eliml {a b : Bool} (Hnab : ¬ (a → b)) : a -:= not_not_elim - (show ¬ ¬ a, - from assume Hna : ¬ a, absurd (assume Ha : a, absurd_elim b Ha Hna) - Hnab) - -theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b -:= assume Hb : b, absurd (assume Ha : a, Hb) - H - -theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b -:= or_elim (boolcomplete a) - (λ Hat : a = true, or_elim (boolcomplete b) - (λ Hbt : b = true, trans Hat (symm Hbt)) - (λ Hbf : b = false, false_elim (a = b) (subst (Hab (eqt_elim Hat)) Hbf))) - (λ Haf : a = false, or_elim (boolcomplete b) - (λ Hbt : b = true, false_elim (a = b) (subst (Hba (eqt_elim Hbt)) Haf)) - (λ Hbf : b = false, trans Haf (symm Hbf))) - --- Another name for boolext -theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a ↔ b -:= boolext Hab Hba - -theorem eqt_intro {a : Bool} (H : a) : a = true -:= boolext (assume H1 : a, trivial) - (assume H2 : true, H) - -theorem eqf_intro {a : Bool} (H : ¬ a) : a = false -:= boolext (assume H1 : a, absurd H1 H) - (assume H2 : false, false_elim a H2) - -theorem by_contradiction {a : Bool} (H : ¬ a → false) : a -:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1)) - -theorem a_neq_a {A : (Type U)} (a : A) : (a ≠ a) ↔ false -:= boolext (assume H, a_neq_a_elim H) - (assume H, false_elim (a ≠ a) H) - -theorem eq_id {A : (Type U)} (a : A) : (a = a) ↔ true -:= eqt_intro (refl a) - -theorem iff_id (a : Bool) : (a ↔ a) ↔ true -:= eqt_intro (refl a) - -theorem heq_id (A : (Type U+1)) (a : A) : (a == a) ↔ true -:= eqt_intro (hrefl a) - -theorem neq_elim {A : (Type U)} {a b : A} (H : a ≠ b) : a = b ↔ false -:= eqf_intro H - -theorem neq_to_not_eq {A : (Type U)} {a b : A} : a ≠ b ↔ ¬ a = b -:= refl (a ≠ b) - -add_rewrite eq_id iff_id neq_to_not_eq - --- Remark: ordered rewriting + assoc + comm + left_comm sorts a term lexicographically -theorem left_comm {A : (Type U)} {R : A -> A -> A} (comm : ∀ x y, R x y = R y x) (assoc : ∀ x y z, R (R x y) z = R x (R y z)) : - ∀ x y z, R x (R y z) = R y (R x z) -:= take x y z, calc R x (R y z) = R (R x y) z : symm (assoc x y z) - ... = R (R y x) z : { comm x y } - ... = R y (R x z) : assoc y x z - -theorem or_comm (a b : Bool) : (a ∨ b) = (b ∨ a) -:= boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a)) - (assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b)) - -theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) -:= boolext (assume H : (a ∨ b) ∨ c, - or_elim H (λ H1 : a ∨ b, or_elim H1 (λ Ha : a, or_introl Ha (b ∨ c)) - (λ Hb : b, or_intror a (or_introl Hb c))) - (λ Hc : c, or_intror a (or_intror b Hc))) - (assume H : a ∨ (b ∨ c), - or_elim H (λ Ha : a, (or_introl (or_introl Ha b) c)) - (λ H1 : b ∨ c, or_elim H1 (λ Hb : b, or_introl (or_intror a Hb) c) - (λ Hc : c, or_intror (a ∨ b) Hc))) - -theorem or_id (a : Bool) : a ∨ a ↔ a -:= boolext (assume H, or_elim H (λ H1, H1) (λ H2, H2)) - (assume H, or_introl H a) - -theorem or_falsel (a : Bool) : a ∨ false ↔ a -:= boolext (assume H, or_elim H (λ H1, H1) (λ H2, false_elim a H2)) - (assume H, or_introl H false) - -theorem or_falser (a : Bool) : false ∨ a ↔ a -:= trans (or_comm false a) (or_falsel a) - -theorem or_truel (a : Bool) : true ∨ a ↔ true -:= boolext (assume H : true ∨ a, trivial) - (assume H : true, or_introl trivial a) - -theorem or_truer (a : Bool) : a ∨ true ↔ true -:= trans (or_comm a true) (or_truel a) - -theorem or_tauto (a : Bool) : a ∨ ¬ a ↔ true -:= eqt_intro (em a) - -theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) -:= left_comm or_comm or_assoc a b c - -add_rewrite or_comm or_assoc or_id or_falsel or_falser or_truel or_truer or_tauto or_left_comm - -theorem and_comm (a b : Bool) : a ∧ b ↔ b ∧ a -:= boolext (assume H, and_intro (and_elimr H) (and_eliml H)) - (assume H, and_intro (and_elimr H) (and_eliml H)) - -theorem and_id (a : Bool) : a ∧ a ↔ a -:= boolext (assume H, and_eliml H) - (assume H, and_intro H H) - -theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) -:= boolext (assume H, and_intro (and_eliml (and_eliml H)) (and_intro (and_elimr (and_eliml H)) (and_elimr H))) - (assume H, and_intro (and_intro (and_eliml H) (and_eliml (and_elimr H))) (and_elimr (and_elimr H))) - -theorem and_truer (a : Bool) : a ∧ true ↔ a -:= boolext (assume H : a ∧ true, and_eliml H) - (assume H : a, and_intro H trivial) - -theorem and_truel (a : Bool) : true ∧ a ↔ a -:= trans (and_comm true a) (and_truer a) - -theorem and_falsel (a : Bool) : a ∧ false ↔ false -:= boolext (assume H, and_elimr H) - (assume H, false_elim (a ∧ false) H) - -theorem and_falser (a : Bool) : false ∧ a ↔ false -:= trans (and_comm false a) (and_falsel a) - -theorem and_absurd (a : Bool) : a ∧ ¬ a ↔ false -:= boolext (assume H, absurd (and_eliml H) (and_elimr H)) - (assume H, false_elim (a ∧ ¬ a) H) - -theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) -:= left_comm and_comm and_assoc a b c - -add_rewrite and_comm and_assoc and_id and_falsel and_falser and_truel and_truer and_absurd and_left_comm - -theorem imp_truer (a : Bool) : (a → true) ↔ true -:= boolext (assume H, trivial) - (assume H Ha, trivial) - -theorem imp_truel (a : Bool) : (true → a) ↔ a -:= boolext (assume H : true → a, H trivial) - (assume Ha H, Ha) - -theorem imp_falser (a : Bool) : (a → false) ↔ ¬ a -:= refl _ - -theorem imp_falsel (a : Bool) : (false → a) ↔ true -:= boolext (assume H, trivial) - (assume H Hf, false_elim a Hf) - -theorem imp_id (a : Bool) : (a → a) ↔ true -:= eqt_intro (λ H : a, H) - -add_rewrite imp_truer imp_truel imp_falser imp_falsel imp_id - -theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b -:= boolext - (assume H : a → b, - (or_elim (em a) - (λ Ha : a, or_intror (¬ a) (H Ha)) - (λ Hna : ¬ a, or_introl Hna b))) - (assume H : ¬ a ∨ b, - assume Ha : a, - resolve1 H ((symm (not_not_eq a)) ◂ Ha)) - -theorem or_imp (a b : Bool) : a ∨ b ↔ (¬ a → b) -:= boolext - (assume H : a ∨ b, - (or_elim H - (assume (Ha : a) (Hna : ¬ a), absurd_elim b Ha Hna) - (assume (Hb : b) (Hna : ¬ a), Hb))) - (assume H : ¬ a → b, - (or_elim (em a) - (assume Ha : a, or_introl Ha b) - (assume Hna : ¬ a, or_intror a (H Hna)))) - -theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b -:= congr2 not H - --- Recall that exists is defined as ¬ ∀ x : A, ¬ P x -theorem exists_elim {A : (Type U)} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B -:= by_contradiction (assume R : ¬ B, - absurd (take a : A, mt (assume H : P a, H2 a H) R) - H1) - -theorem exists_intro {A : (Type U)} {P : A → Bool} (a : A) (H : P a) : Exists A P -:= assume H1 : (∀ x : A, ¬ P x), - absurd H (H1 a) - -theorem not_exists (A : (Type U)) (P : A → Bool) : ¬ (∃ x : A, P x) ↔ (∀ x : A, ¬ P x) -:= calc (¬ ∃ x : A, P x) = ¬ ¬ ∀ x : A, ¬ P x : refl (¬ ∃ x : A, P x) - ... = ∀ x : A, ¬ P x : not_not_eq (∀ x : A, ¬ P x) - -theorem not_exists_elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x -:= (not_exists A P) ◂ H - -theorem exists_unfold1 {A : (Type U)} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x) -:= exists_elim H - (λ (w : A) (H1 : P w), - or_elim (em (w = a)) - (λ Heq : w = a, or_introl (subst H1 Heq) (∃ x : A, x ≠ a ∧ P x)) - (λ Hne : w ≠ a, or_intror (P a) (exists_intro w (and_intro Hne H1)))) - -theorem exists_unfold2 {A : (Type U)} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x -:= or_elim H - (λ H1 : P a, exists_intro a H1) - (λ H2 : (∃ x : A, x ≠ a ∧ P x), - exists_elim H2 - (λ (w : A) (Hw : w ≠ a ∧ P w), - exists_intro w (and_elimr Hw))) - -theorem exists_unfold {A : (Type U)} (P : A → Bool) (a : A) : (∃ x : A, P x) ↔ (P a ∨ (∃ x : A, x ≠ a ∧ P x)) -:= boolext (assume H : (∃ x : A, P x), exists_unfold1 a H) - (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists_unfold2 a H) - -definition inhabited (A : (Type U)) -:= ∃ x : A, true - --- If we have an element of type A, then A is inhabited -theorem inhabited_intro {A : (Type U)} (a : A) : inhabited A -:= assume H : (∀ x, ¬ true), absurd_not_true (H a) - -theorem inhabited_elim {A : (Type U)} (H1 : inhabited A) {B : Bool} (H2 : A → B) : B -:= obtain (w : A) (Hw : true), from H1, - H2 w - -theorem inhabited_ex_intro {A : (Type U)} {P : A → Bool} (H : ∃ x, P x) : inhabited A -:= obtain (w : A) (Hw : P w), from H, - exists_intro w trivial - --- If a function space is non-empty, then for every 'a' in the domain, the range (B a) is not empty -theorem inhabited_range {A : (Type U)} {B : A → (Type U)} (H : inhabited (∀ x, B x)) (a : A) : inhabited (B a) -:= by_contradiction (assume N : ¬ inhabited (B a), - let s1 : ¬ ∃ x : B a, true := N, - s2 : ∀ x : B a, false := take x : B a, absurd_not_true (not_exists_elim s1 x), - s3 : ∃ y : (∀ x, B x), true := H - in obtain (w : (∀ x, B x)) (Hw : true), from s3, - let s4 : B a := w a - in s2 s4) - -theorem exists_rem {A : (Type U)} (H : inhabited A) (p : Bool) : (∃ x : A, p) ↔ p -:= iff_intro - (assume Hl : (∃ x : A, p), - obtain (w : A) (Hw : p), from Hl, - Hw) - (assume Hr : p, - inhabited_elim H (λ w, exists_intro w Hr)) - -theorem forall_rem {A : (Type U)} (H : inhabited A) (p : Bool) : (∀ x : A, p) ↔ p -:= iff_intro - (assume Hl : (∀ x : A, p), - inhabited_elim H (λ w, Hl w)) - (assume Hr : p, - take x, Hr) - - -theorem not_and (a b : Bool) : ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b -:= boolext (assume H, or_elim (em a) - (assume Ha, or_elim (em b) - (assume Hb, absurd_elim (¬ a ∨ ¬ b) (and_intro Ha Hb) H) - (assume Hnb, or_intror (¬ a) Hnb)) - (assume Hna, or_introl Hna (¬ b))) - (assume (H : ¬ a ∨ ¬ b) (N : a ∧ b), - or_elim H - (assume Hna, absurd (and_eliml N) Hna) - (assume Hnb, absurd (and_elimr N) Hnb)) - -theorem not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b -:= (not_and a b) ◂ H - -theorem not_or (a b : Bool) : ¬ (a ∨ b) ↔ ¬ a ∧ ¬ b -:= boolext (assume H, or_elim (em a) - (assume Ha, absurd_elim (¬ a ∧ ¬ b) (or_introl Ha b) H) - (assume Hna, or_elim (em b) - (assume Hb, absurd_elim (¬ a ∧ ¬ b) (or_intror a Hb) H) - (assume Hnb, and_intro Hna Hnb))) - (assume (H : ¬ a ∧ ¬ b) (N : a ∨ b), - or_elim N - (assume Ha, absurd Ha (and_eliml H)) - (assume Hb, absurd Hb (and_elimr H))) - -theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b -:= (not_or a b) ◂ H - -theorem not_implies (a b : Bool) : ¬ (a → b) ↔ a ∧ ¬ b -:= calc (¬ (a → b)) = ¬ (¬ a ∨ b) : { imp_or a b } - ... = ¬ ¬ a ∧ ¬ b : not_or (¬ a) b - ... = a ∧ ¬ b : congr2 (λ x, x ∧ ¬ b) (not_not_eq a) - -theorem and_imp (a b : Bool) : a ∧ b ↔ ¬ (a → ¬ b) -:= have H1 : a ∧ ¬ ¬ b ↔ ¬ (a → ¬ b), - from symm (not_implies a (¬ b)), - subst H1 (not_not_eq b) - -theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b -:= (not_implies a b) ◂ H - -theorem a_eq_not_a (a : Bool) : (a = ¬ a) ↔ false -:= boolext (λ H, or_elim (em a) - (λ Ha, absurd Ha (subst Ha H)) - (λ Hna, absurd (subst Hna (symm H)) Hna)) - (λ H, false_elim (a = ¬ a) H) - -theorem a_iff_not_a (a : Bool) : (a ↔ ¬ a) ↔ false -:= a_eq_not_a a - -theorem true_eq_false : (true = false) ↔ false -:= subst (a_eq_not_a true) not_true - -theorem true_iff_false : (true ↔ false) ↔ false -:= true_eq_false - -theorem false_eq_true : (false = true) ↔ false -:= subst (a_eq_not_a false) not_false - -theorem false_iff_true : (false ↔ true) ↔ false -:= false_eq_true - -theorem a_iff_true (a : Bool) : (a ↔ true) ↔ a -:= boolext (λ H, eqt_elim H) - (λ H, eqt_intro H) - -theorem a_iff_false (a : Bool) : (a ↔ false) ↔ ¬ a -:= boolext (λ H, eqf_elim H) - (λ H, eqf_intro H) - -add_rewrite a_eq_not_a a_iff_not_a true_eq_false true_iff_false false_eq_true false_iff_true a_iff_true a_iff_false - -theorem not_iff (a b : Bool) : ¬ (a ↔ b) ↔ (¬ a ↔ b) -:= or_elim (em b) - (λ Hb, calc (¬ (a ↔ b)) = (¬ (a ↔ true)) : { eqt_intro Hb } - ... = ¬ a : { a_iff_true a } - ... = ¬ a ↔ true : { symm (a_iff_true (¬ a)) } - ... = ¬ a ↔ b : { symm (eqt_intro Hb) }) - (λ Hnb, calc (¬ (a ↔ b)) = (¬ (a ↔ false)) : { eqf_intro Hnb } - ... = ¬ ¬ a : { a_iff_false a } - ... = ¬ a ↔ false : { symm (a_iff_false (¬ a)) } - ... = ¬ a ↔ b : { symm (eqf_intro Hnb) }) - -theorem not_iff_elim {a b : Bool} (H : ¬ (a ↔ b)) : (¬ a) ↔ b -:= (not_iff a b) ◂ H - - --- Congruence theorems for contextual simplification - --- Simplify a → b, by first simplifying a to c using the fact that ¬ b is true, and then --- b to d using the fact that c is true -theorem imp_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d) -:= or_elim (em b) - (λ H_b : b, - or_elim (em c) - (λ H_c : c, - calc (a → b) = (a → true) : { eqt_intro H_b } - ... = true : imp_truer a - ... = (c → true) : symm (imp_truer c) - ... = (c → b) : { symm (eqt_intro H_b) } - ... = (c → d) : { H_bd H_c }) - (λ H_nc : ¬ c, - calc (a → b) = (a → true) : { eqt_intro H_b } - ... = true : imp_truer a - ... = (false → d) : symm (imp_falsel d) - ... = (c → d) : { symm (eqf_intro H_nc) })) - (λ H_nb : ¬ b, - or_elim (em c) - (λ H_c : c, - calc (a → b) = (c → b) : { H_ac H_nb } - ... = (c → d) : { H_bd H_c }) - (λ H_nc : ¬ c, - calc (a → b) = (c → b) : { H_ac H_nb } - ... = (false → b) : { eqf_intro H_nc } - ... = true : imp_falsel b - ... = (false → d) : symm (imp_falsel d) - ... = (c → d) : { symm (eqf_intro H_nc) })) - - --- Simplify a → b, by first simplifying b to d using the fact that a is true, and then --- b to d using the fact that ¬ d is true. --- This kind of congruence seems to be useful in very rare cases. -theorem imp_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H_nd : ¬ d), a = c) : (a → b) = (c → d) -:= or_elim (em a) - (λ H_a : a, - or_elim (em d) - (λ H_d : d, - calc (a → b) = (a → d) : { H_bd H_a } - ... = (a → true) : { eqt_intro H_d } - ... = true : imp_truer a - ... = (c → true) : symm (imp_truer c) - ... = (c → d) : { symm (eqt_intro H_d) }) - (λ H_nd : ¬ d, - calc (a → b) = (c → b) : { H_ac H_nd } - ... = (c → d) : { H_bd H_a })) - (λ H_na : ¬ a, - or_elim (em d) - (λ H_d : d, - calc (a → b) = (false → b) : { eqf_intro H_na } - ... = true : imp_falsel b - ... = (c → true) : symm (imp_truer c) - ... = (c → d) : { symm (eqt_intro H_d) }) - (λ H_nd : ¬ d, - calc (a → b) = (false → b) : { eqf_intro H_na } - ... = true : imp_falsel b - ... = (false → d) : symm (imp_falsel d) - ... = (a → d) : { symm (eqf_intro H_na) } - ... = (c → d) : { H_ac H_nd })) - --- (Common case) simplify a to c, and then b to d using the fact that c is true -theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d) -:= imp_congrr (λ H, H_ac) H_bd - -theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ↔ c ∨ d -:= have H1 : (¬ a → b) ↔ (¬ c → d), - from imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd, - calc (a ∨ b) = (¬ a → b) : or_imp _ _ - ... = (¬ c → d) : H1 - ... = c ∨ d : symm (or_imp _ _) - -theorem or_congrl {a b c d : Bool} (H_bd : ∀ (H_na : ¬ a), b = d) (H_ac : ∀ (H_nd : ¬ d), a = c) : a ∨ b ↔ c ∨ d -:= have H1 : (¬ a → b) ↔ (¬ c → d), - from imp_congrl H_bd (λ H_nd : ¬ d, congr2 not (H_ac H_nd)), - calc (a ∨ b) = (¬ a → b) : or_imp _ _ - ... = (¬ c → d) : H1 - ... = c ∨ d : symm (or_imp _ _) --- (Common case) simplify a to c, and then b to d using the fact that ¬ c is true -theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ↔ c ∨ d -:= or_congrr (λ H, H_ac) H_bd - -theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d -:= have H1 : ¬ (a → ¬ b) ↔ ¬ (c → ¬ d), - from congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c))), - calc (a ∧ b) = ¬ (a → ¬ b) : and_imp _ _ - ... = ¬ (c → ¬ d) : H1 - ... = c ∧ d : symm (and_imp _ _) - -theorem and_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H_d : d), a = c) : a ∧ b ↔ c ∧ d -:= have H1 : ¬ (a → ¬ b) ↔ ¬ (c → ¬ d), - from congr2 not (imp_congrl (λ H_a : a, congr2 not (H_bd H_a)) (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd))), - calc (a ∧ b) = ¬ (a → ¬ b) : and_imp _ _ - ... = ¬ (c → ¬ d) : H1 - ... = c ∧ d : symm (and_imp _ _) - --- (Common case) simplify a to c, and then b to d using the fact that c is true -theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d -:= and_congrr (λ H, H_ac) H_bd - -theorem forall_or_distributer {A : (Type U)} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x) -:= boolext - (assume H : (∀ x, p ∨ φ x), - or_elim (em p) - (λ Hp : p, or_introl Hp (∀ x, φ x)) - (λ Hnp : ¬ p, or_intror p (take x, - resolve1 (H x) Hnp))) - (assume H : (p ∨ ∀ x, φ x), - take x, - or_elim H - (λ H1 : p, or_introl H1 (φ x)) - (λ H2 : (∀ x, φ x), or_intror p (H2 x))) - -theorem forall_or_distributel {A : Type} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) = ((∀ x, φ x) ∨ p) -:= boolext - (assume H : (∀ x, φ x ∨ p), - or_elim (em p) - (λ Hp : p, or_intror (∀ x, φ x) Hp) - (λ Hnp : ¬ p, or_introl (take x, resolve2 (H x) Hnp) p)) - (assume H : (∀ x, φ x) ∨ p, - take x, - or_elim H - (λ H1 : (∀ x, φ x), or_introl (H1 x) p) - (λ H2 : p, or_intror (φ x) H2)) - -theorem forall_and_distribute {A : (Type U)} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ↔ (∀ x, φ x) ∧ (∀ x, ψ x) -:= boolext - (assume H : (∀ x, φ x ∧ ψ x), - and_intro (take x, and_eliml (H x)) (take x, and_elimr (H x))) - (assume H : (∀ x, φ x) ∧ (∀ x, ψ x), - take x, and_intro (and_eliml H x) (and_elimr H x)) - -theorem exists_and_distributer {A : (Type U)} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) ↔ p ∧ ∃ x, φ x -:= boolext - (assume H : (∃ x, p ∧ φ x), - obtain (w : A) (Hw : p ∧ φ w), from H, - and_intro (and_eliml Hw) (exists_intro w (and_elimr Hw))) - (assume H : (p ∧ ∃ x, φ x), - obtain (w : A) (Hw : φ w), from (and_elimr H), - exists_intro w (and_intro (and_eliml H) Hw)) - - -theorem exists_or_distribute {A : (Type U)} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) ↔ (∃ x, φ x) ∨ (∃ x, ψ x) -:= boolext - (assume H : (∃ x, φ x ∨ ψ x), - obtain (w : A) (Hw : φ w ∨ ψ w), from H, - or_elim Hw - (λ Hw1 : φ w, or_introl (exists_intro w Hw1) (∃ x, ψ x)) - (λ Hw2 : ψ w, or_intror (∃ x, φ x) (exists_intro w Hw2))) - (assume H : (∃ x, φ x) ∨ (∃ x, ψ x), - or_elim H - (λ H1 : (∃ x, φ x), - obtain (w : A) (Hw : φ w), from H1, - exists_intro w (or_introl Hw (ψ w))) - (λ H2 : (∃ x, ψ x), - obtain (w : A) (Hw : ψ w), from H2, - exists_intro w (or_intror (φ w) Hw))) - -theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x ↔ Q x) : (∃ x : A, P x) ↔ (∃ x : A, Q x) -:= boolext - (assume Hex, obtain w Pw, from Hex, exists_intro w ((H w) ◂ Pw)) - (assume Hex, obtain w Qw, from Hex, exists_intro w ((symm (H w)) ◂ Qw)) - -theorem not_forall (A : (Type U)) (P : A → Bool) : ¬ (∀ x : A, P x) ↔ (∃ x : A, ¬ P x) -:= boolext - (assume H, by_contradiction (assume N : ¬ (∃ x, ¬ P x), - absurd (take x, not_not_elim (not_exists_elim N x)) H)) - (assume (H : ∃ x, ¬ P x) (N : ∀ x, P x), - obtain w Hw, from H, - absurd (N w) Hw) - -theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x -:= (not_forall A P) ◂ H - -theorem exists_and_distributel {A : (Type U)} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) ↔ (∃ x, φ x) ∧ p -:= calc (∃ x, φ x ∧ p) = (∃ x, p ∧ φ x) : eq_exists_intro (λ x, and_comm (φ x) p) - ... = (p ∧ (∃ x, φ x)) : exists_and_distributer p φ - ... = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x) - -theorem exists_imp_distribute {A : (Type U)} (φ ψ : A → Bool) : (∃ x, φ x → ψ x) ↔ ((∀ x, φ x) → (∃ x, ψ x)) -:= calc (∃ x, φ x → ψ x) = (∃ x, ¬ φ x ∨ ψ x) : eq_exists_intro (λ x, imp_or (φ x) (ψ x)) - ... = (∃ x, ¬ φ x) ∨ (∃ x, ψ x) : exists_or_distribute _ _ - ... = ¬ (∀ x, φ x) ∨ (∃ x, ψ x) : { symm (not_forall A φ) } - ... = (∀ x, φ x) → (∃ x, ψ x) : symm (imp_or _ _) - -theorem forall_uninhabited {A : (Type U)} {B : A → Bool} (H : ¬ inhabited A) : ∀ x, B x -:= by_contradiction (assume N : ¬ (∀ x, B x), - obtain w Hw, from not_forall_elim N, - absurd (inhabited_intro w) H) - -theorem allext {A : (Type U)} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x) -:= boolext - (assume Hl, take x, (H x) ◂ (Hl x)) - (assume Hr, take x, (symm (H x)) ◂ (Hr x)) - -theorem proj1_congr {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj1 a = proj1 b -:= subst (refl (proj1 a)) H - -theorem proj2_congr {A B : (Type U)} {a b : A # B} (H : a = b) : proj2 a = proj2 b -:= subst (refl (proj2 a)) H - -theorem hproj2_congr {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj2 a == proj2 b -:= subst (hrefl (proj2 a)) H - --- Up to this point, we proved all theorems using just reflexivity, substitution and case (proof by cases) - --- Function extensionality -axiom funext {A : (Type U)} {B : A → (Type U)} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g - --- Eta is a consequence of function extensionality -theorem eta {A : (Type U)} {B : A → (Type U)} (f : ∀ x : A, B x) : (λ x : A, f x) = f -:= funext (λ x : A, refl (f x)) - --- Epsilon (Hilbert's operator) -variable eps {A : (Type U)} (H : inhabited A) (P : A → Bool) : A -alias ε : eps -axiom eps_ax {A : (Type U)} (H : inhabited A) {P : A → Bool} (a : A) : P a → P (ε H P) - -theorem eps_th {A : (Type U)} {P : A → Bool} (a : A) : P a → P (ε (inhabited_intro a) P) -:= assume H : P a, @eps_ax A (inhabited_intro a) P a H - -theorem eps_singleton {A : (Type U)} (H : inhabited A) (a : A) : ε H (λ x, x = a) = a -:= let P := λ x, x = a, - Ha : P a := refl a - in eps_ax H a Ha - --- A function space (∀ x : A, B x) is inhabited if forall a : A, we have inhabited (B a) -theorem inhabited_dfun {A : (Type U)} {B : A → (Type U)} (Hn : ∀ a, inhabited (B a)) : inhabited (∀ x, B x) -:= inhabited_intro (λ x, ε (Hn x) (λ y, true)) - -theorem inhabited_fun (A : (Type U)) {B : (Type U)} (H : inhabited B) : inhabited (A → B) -:= inhabited_intro (λ x, ε H (λ y, true)) - -theorem exists_to_eps {A : (Type U)} {P : A → Bool} (H : ∃ x, P x) : P (ε (inhabited_ex_intro H) P) -:= obtain (w : A) (Hw : P w), from H, - @eps_ax _ (inhabited_ex_intro H) P w Hw - -theorem axiom_of_choice {A : (Type U)} {B : A → (Type U)} {R : ∀ x : A, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x) -:= exists_intro - (λ x, ε (inhabited_ex_intro (H x)) (λ y, R x y)) -- witness for f - (λ x, exists_to_eps (H x)) -- proof that witness satisfies ∀ x, R x (f x) - -theorem skolem_th {A : (Type U)} {B : A → (Type U)} {P : ∀ x : A, B x → Bool} : - (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) -:= iff_intro - (λ H : (∀ x, ∃ y, P x y), @axiom_of_choice _ _ P H) - (λ H : (∃ f, (∀ x, P x (f x))), - take x, obtain (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)), from H, - exists_intro (fw x) (Hw x)) - --- if-then-else expression, we define it using Hilbert's operator -definition ite {A : (Type U)} (c : Bool) (a b : A) : A -:= ε (inhabited_intro a) (λ r, (c → r = a) ∧ (¬ c → r = b)) -notation 45 if _ then _ else _ : ite - -theorem if_true {A : (Type U)} (a b : A) : (if true then a else b) = a -:= calc (if true then a else b) = ε (inhabited_intro a) (λ r, (true → r = a) ∧ (¬ true → r = b)) : refl (if true then a else b) - ... = ε (inhabited_intro a) (λ r, r = a) : by simp - ... = a : eps_singleton (inhabited_intro a) a - -theorem if_false {A : (Type U)} (a b : A) : (if false then a else b) = b -:= calc (if false then a else b) = ε (inhabited_intro a) (λ r, (false → r = a) ∧ (¬ false → r = b)) : refl (if false then a else b) - ... = ε (inhabited_intro a) (λ r, r = b) : by simp - ... = b : eps_singleton (inhabited_intro a) b - -theorem if_a_a {A : (Type U)} (c : Bool) (a: A) : (if c then a else a) = a -:= or_elim (em c) - (λ H : c, calc (if c then a else a) = (if true then a else a) : { eqt_intro H } - ... = a : if_true a a) - (λ H : ¬ c, calc (if c then a else a) = (if false then a else a) : { eqf_intro H } - ... = a : if_false a a) - -add_rewrite if_true if_false if_a_a - -theorem if_congr {A : (Type U)} {b c : Bool} {x y u v : A} (H_bc : b = c) - (H_xu : ∀ (H_c : c), x = u) (H_yv : ∀ (H_nc : ¬ c), y = v) : - (if b then x else y) = if c then u else v -:= or_elim (em c) - (λ H_c : c, calc - (if b then x else y) = if c then x else y : { H_bc } - ... = if true then x else y : { eqt_intro H_c } - ... = x : if_true _ _ - ... = u : H_xu H_c - ... = if true then u else v : symm (if_true _ _) - ... = if c then u else v : { symm (eqt_intro H_c) }) - (λ H_nc : ¬ c, calc - (if b then x else y) = if c then x else y : { H_bc } - ... = if false then x else y : { eqf_intro H_nc } - ... = y : if_false _ _ - ... = v : H_yv H_nc - ... = if false then u else v : symm (if_false _ _) - ... = if c then u else v : { symm (eqf_intro H_nc) }) - -theorem if_imp_then {a b c : Bool} (H : if a then b else c) : a → b -:= assume Ha : a, eqt_elim (calc b = if true then b else c : symm (if_true b c) - ... = if a then b else c : { symm (eqt_intro Ha) } - ... = true : eqt_intro H) - -theorem if_imp_else {a b c : Bool} (H : if a then b else c) : ¬ a → c -:= assume Hna : ¬ a, eqt_elim (calc c = if false then b else c : symm (if_false b c) - ... = if a then b else c : { symm (eqf_intro Hna) } - ... = true : eqt_intro H) - -theorem app_if_distribute {A B : (Type U)} (c : Bool) (f : A → B) (a b : A) : f (if c then a else b) = if c then f a else f b -:= or_elim (em c) - (λ Hc : c , calc - f (if c then a else b) = f (if true then a else b) : { eqt_intro Hc } - ... = f a : { if_true a b } - ... = if true then f a else f b : symm (if_true (f a) (f b)) - ... = if c then f a else f b : { symm (eqt_intro Hc) }) - (λ Hnc : ¬ c, calc - f (if c then a else b) = f (if false then a else b) : { eqf_intro Hnc } - ... = f b : { if_false a b } - ... = if false then f a else f b : symm (if_false (f a) (f b)) - ... = if c then f a else f b : { symm (eqf_intro Hnc) }) - -theorem eq_if_distributer {A : (Type U)} (c : Bool) (a b v : A) : (v = (if c then a else b)) = if c then v = a else v = b -:= app_if_distribute c (eq v) a b - -theorem eq_if_distributel {A : (Type U)} (c : Bool) (a b v : A) : ((if c then a else b) = v) = if c then a = v else b = v -:= app_if_distribute c (λ x, x = v) a b - -set_opaque exists true -set_opaque not true -set_opaque or true -set_opaque and true -set_opaque implies true -set_opaque ite true -set_opaque eq true - -definition injective {A B : (Type U)} (f : A → B) := ∀ x1 x2, f x1 = f x2 → x1 = x2 -definition non_surjective {A B : (Type U)} (f : A → B) := ∃ y, ∀ x, ¬ f x = y - --- The set of individuals, we need to assert the existence of one infinite set -variable ind : Type --- ind is infinite, i.e., there is a function f s.t. f is injective, and not surjective -axiom infinity : ∃ f : ind → ind, injective f ∧ non_surjective f - --- Pair extensionality -axiom pairext {A : (Type U)} {B : A → (Type U)} (a b : sig x, B x) - (H1 : proj1 a = proj1 b) (H2 : proj2 a == proj2 b) - : a = b - -theorem pair_proj_eq {A : (Type U)} {B : A → (Type U)} (a : sig x, B x) : pair (proj1 a) (proj2 a) = a -:= have Heq1 : proj1 (pair (proj1 a) (proj2 a)) = proj1 a, - from refl (proj1 a), - have Heq2 : proj2 (pair (proj1 a) (proj2 a)) == proj2 a, - from hrefl (proj2 a), - show pair (proj1 a) (proj2 a) = a, - from pairext (pair (proj1 a) (proj2 a)) a Heq1 Heq2 - -theorem pair_congr {A : (Type U)} {B : A → (Type U)} {a a' : A} {b : B a} {b' : B a'} (Ha : a = a') (Hb : b == b') - : (pair a b) = (pair a' b') -:= have Heq1 : proj1 (pair a b) = proj1 (pair a' b'), - from Ha, - have Heq2 : proj2 (pair a b) == proj2 (pair a' b'), - from Hb, - show (pair a b) = (pair a' b'), - from pairext (pair a b) (pair a' b') Heq1 Heq2 - -theorem pairext_proj {A B : (Type U)} {p : A # B} {a : A} {b : B} (H1 : proj1 p = a) (H2 : proj2 p = b) : p = (pair a b) -:= pairext p (pair a b) H1 (to_heq H2) - -theorem hpairext_proj {A : (Type U)} {B : A → (Type U)} {p : sig x, B x} {a : A} {b : B a} - (H1 : proj1 p = a) (H2 : proj2 p == b) : p = (pair a b) -:= pairext p (pair a b) H1 H2 - --- Heterogeneous equality axioms and theorems - --- We can "type-cast" an A expression into a B expression, if we can prove that A == B --- Remark: we use A == B instead of A = B, because A = B would be type incorrect. --- A = B is actually (@eq (Type U) A B), which is type incorrect because --- the first argument of eq must have type (Type U) and the type of (Type U) is (Type U+1) -variable cast {A B : (Type U+1)} : A == B → A → B - -axiom cast_heq {A B : (Type U+1)} (H : A == B) (a : A) : cast H a == a - --- Heterogeneous equality satisfies the usual properties: symmetry, transitivity, congruence, function extensionality, ... - --- Heterogeneous version of subst -axiom hsubst {A B : (Type U+1)} {a : A} {b : B} (P : ∀ T : (Type U+1), T → Bool) : P A a → a == b → P B b - -theorem hsymm {A B : (Type U+1)} {a : A} {b : B} (H : a == b) : b == a -:= hsubst (λ (T : (Type U+1)) (x : T), x == a) (hrefl a) H - -theorem htrans {A B C : (Type U+1)} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c -:= hsubst (λ (T : (Type U+1)) (x : T), a == x) H1 H2 - -axiom hcongr {A A' : (Type U+1)} {B : A → (Type U+1)} {B' : A' → (Type U+1)} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} : - f == f' → a == a' → f a == f' a' - -axiom hfunext {A A' : (Type U+1)} {B : A → (Type U+1)} {B' : A' → (Type U+1)} {f : ∀ x, B x} {f' : ∀ x, B' x} : - A == A' → (∀ x x', x == x' → f x == f' x') → f == f' - -axiom hpiext {A A' : (Type U+1)} {B : A → (Type U+1)} {B' : A' → (Type U+1)} : - A == A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) - -axiom hsigext {A A' : (Type U+1)} {B : A → (Type U+1)} {B' : A' → (Type U+1)} : - A == A' → (∀ x x', x == x' → B x == B' x') → (sig x, B x) == (sig x, B' x) - --- Heterogeneous version of the allext theorem -theorem hallext {A A' : (Type U+1)} {B : A → Bool} {B' : A' → Bool} - (Ha : A == A') (Hb : ∀ x x', x == x' → B x = B' x') : (∀ x, B x) = (∀ x, B' x) -:= to_eq (hpiext Ha (λ x x' Heq, to_heq (Hb x x' Heq))) - --- Simpler version of hfunext axiom, we use it to build proofs -theorem hsfunext {A : (Type U)} {B B' : A → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} : - (∀ x, f x == f' x) → f == f' -:= λ Hb, - hfunext (hrefl A) (λ (x x' : A) (Heq : x == x'), - let s1 : f x == f' x := Hb x, - s2 : f' x == f' x' := hcongr (hrefl f') Heq - in htrans s1 s2) - -theorem heq_congr {A B : (Type U)} {a a' : A} {b b' : B} (H1 : a = a') (H2 : b = b') : (a == b) = (a' == b') -:= calc (a == b) = (a' == b) : { H1 } - ... = (a' == b') : { H2 } - -theorem hheq_congr {A A' B B' : (Type U+1)} {a : A} {a' : A'} {b : B} {b' : B'} (H1 : a == a') (H2 : b == b') : (a == b) = (a' == b') -:= have Heq1 : (a == b) = (a' == b), - from (hsubst (λ (T : (Type U+1)) (x : T), (a == b) = (x == b)) (refl (a == b)) H1), - have Heq2 : (a' == b) = (a' == b'), - from (hsubst (λ (T : (Type U+1)) (x : T), (a' == b) = (a' == x)) (refl (a' == b)) H2), - show (a == b) = (a' == b'), - from trans Heq1 Heq2 - -theorem type_eq {A B : (Type U)} {a : A} {b : B} (H : a == b) : A == B -:= hsubst (λ (T : (Type U+1)) (x : T), A == T) (hrefl A) H - --- Some theorems that are useful for applying simplifications. -theorem cast_eq {A : (Type U)} (H : A == A) (a : A) : cast H a = a -:= to_eq (cast_heq H a) - -theorem cast_trans {A B C : (Type U)} (Hab : A == B) (Hbc : B == C) (a : A) : cast Hbc (cast Hab a) = cast (htrans Hab Hbc) a -:= have Heq1 : cast Hbc (cast Hab a) == cast Hab a, - from cast_heq Hbc (cast Hab a), - have Heq2 : cast Hab a == a, - from cast_heq Hab a, - have Heq3 : cast (htrans Hab Hbc) a == a, - from cast_heq (htrans Hab Hbc) a, - show cast Hbc (cast Hab a) = cast (htrans Hab Hbc) a, - from to_eq (htrans (htrans Heq1 Heq2) (hsymm Heq3)) - -theorem cast_pull {A : (Type U)} {B B' : A → (Type U)} - (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) == (∀ x, B' x)) (Hba : (B a) == (B' a)) : - cast Hb f a = cast Hba (f a) -:= have s1 : cast Hb f a == f a, - from hcongr (cast_heq Hb f) (hrefl a), - have s2 : cast Hba (f a) == f a, - from cast_heq Hba (f a), - show cast Hb f a = cast Hba (f a), - from to_eq (htrans s1 (hsymm s2)) - --- Proof irrelevance is true in the set theoretic model we have for Lean. -axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2 - --- A more general version of proof_irrel that can be be derived using proof_irrel, heq axioms and boolext/iff_intro -theorem hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2 -:= let Hab : a == b := to_heq (iff_intro (assume Ha, H2) (assume Hb, H1)), - H1b : b := cast Hab H1, - H1_eq_H1b : H1 == H1b := hsymm (cast_heq Hab H1), - H1b_eq_H2 : H1b == H2 := to_heq (proof_irrel H1b H2) - in htrans H1_eq_H1b H1b_eq_H2 diff --git a/src/builtin/lean2cpp.lean b/src/builtin/lean2cpp.lean deleted file mode 100644 index 0da5c219b..000000000 --- a/src/builtin/lean2cpp.lean +++ /dev/null @@ -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('}') -*) diff --git a/src/builtin/lean2cpp.sh b/src/builtin/lean2cpp.sh deleted file mode 100755 index 01bc9aaa3..000000000 --- a/src/builtin/lean2cpp.sh +++ /dev/null @@ -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 diff --git a/src/builtin/lean2h.lean b/src/builtin/lean2h.lean deleted file mode 100644 index 6752ce425..000000000 --- a/src/builtin/lean2h.lean +++ /dev/null @@ -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('}') - -*) diff --git a/src/builtin/lean2h.sh b/src/builtin/lean2h.sh deleted file mode 100755 index 2b9ac419d..000000000 --- a/src/builtin/lean2h.sh +++ /dev/null @@ -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 diff --git a/src/builtin/list.lean b/src/builtin/list.lean deleted file mode 100644 index a950aeeb7..000000000 --- a/src/builtin/list.lean +++ /dev/null @@ -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 \ No newline at end of file diff --git a/src/builtin/macros.lua b/src/builtin/macros.lua deleted file mode 100644 index d87b57587..000000000 --- a/src/builtin/macros.lua +++ /dev/null @@ -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) diff --git a/src/builtin/name_conv.lua b/src/builtin/name_conv.lua deleted file mode 100644 index 3a31c7e29..000000000 --- a/src/builtin/name_conv.lua +++ /dev/null @@ -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 diff --git a/src/builtin/num.lean b/src/builtin/num.lean deleted file mode 100644 index 646dfc650..000000000 --- a/src/builtin/num.lean +++ /dev/null @@ -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 diff --git a/src/builtin/obj/Int.olean b/src/builtin/obj/Int.olean deleted file mode 100644 index e1a16bf66..000000000 Binary files a/src/builtin/obj/Int.olean and /dev/null differ diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean deleted file mode 100644 index 8c23f25d8..000000000 Binary files a/src/builtin/obj/Nat.olean and /dev/null differ diff --git a/src/builtin/obj/Real.olean b/src/builtin/obj/Real.olean deleted file mode 100644 index dc0f82cea..000000000 Binary files a/src/builtin/obj/Real.olean and /dev/null differ diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean deleted file mode 100644 index 898289060..000000000 Binary files a/src/builtin/obj/kernel.olean and /dev/null differ diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean deleted file mode 100644 index 429a425e1..000000000 Binary files a/src/builtin/obj/num.olean and /dev/null differ diff --git a/src/builtin/obj/optional.olean b/src/builtin/obj/optional.olean deleted file mode 100644 index d961bd392..000000000 Binary files a/src/builtin/obj/optional.olean and /dev/null differ diff --git a/src/builtin/obj/specialfn.olean b/src/builtin/obj/specialfn.olean deleted file mode 100644 index c2c9170a5..000000000 Binary files a/src/builtin/obj/specialfn.olean and /dev/null differ diff --git a/src/builtin/obj/subtype.olean b/src/builtin/obj/subtype.olean deleted file mode 100644 index fbadac036..000000000 Binary files a/src/builtin/obj/subtype.olean and /dev/null differ diff --git a/src/builtin/obj/sum.olean b/src/builtin/obj/sum.olean deleted file mode 100644 index 31758cfe8..000000000 Binary files a/src/builtin/obj/sum.olean and /dev/null differ diff --git a/src/builtin/optional.lean b/src/builtin/optional.lean deleted file mode 100644 index aa7b685fc..000000000 --- a/src/builtin/optional.lean +++ /dev/null @@ -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 diff --git a/src/builtin/proof_irrel.lean b/src/builtin/proof_irrel.lean deleted file mode 100644 index 018c00c5c..000000000 --- a/src/builtin/proof_irrel.lean +++ /dev/null @@ -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) diff --git a/src/builtin/quotient.lean b/src/builtin/quotient.lean deleted file mode 100644 index 7d5162297..000000000 --- a/src/builtin/quotient.lean +++ /dev/null @@ -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 diff --git a/src/builtin/repl.lua b/src/builtin/repl.lua deleted file mode 100644 index cfaaeb188..000000000 --- a/src/builtin/repl.lua +++ /dev/null @@ -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 diff --git a/src/builtin/specialfn.lean b/src/builtin/specialfn.lean deleted file mode 100644 index 95f4e4e71..000000000 --- a/src/builtin/specialfn.lean +++ /dev/null @@ -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. diff --git a/src/builtin/subtype.lean b/src/builtin/subtype.lean deleted file mode 100644 index 505b92b69..000000000 --- a/src/builtin/subtype.lean +++ /dev/null @@ -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 diff --git a/src/builtin/sum.lean b/src/builtin/sum.lean deleted file mode 100644 index abfc2e50f..000000000 --- a/src/builtin/sum.lean +++ /dev/null @@ -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 diff --git a/src/builtin/sum2.lean b/src/builtin/sum2.lean deleted file mode 100644 index d57843fa3..000000000 --- a/src/builtin/sum2.lean +++ /dev/null @@ -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 \ No newline at end of file diff --git a/src/builtin/tactic.lua b/src/builtin/tactic.lua deleted file mode 100644 index c7f852e3b..000000000 --- a/src/builtin/tactic.lua +++ /dev/null @@ -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) diff --git a/src/builtin/template.lua b/src/builtin/template.lua deleted file mode 100644 index 5054253b2..000000000 --- a/src/builtin/template.lua +++ /dev/null @@ -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 diff --git a/src/builtin/util.lua b/src/builtin/util.lua deleted file mode 100644 index b33168820..000000000 --- a/src/builtin/util.lua +++ /dev/null @@ -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