From 1da2e5d100bfea95211174e871a63bc80e2d1d57 Mon Sep 17 00:00:00 2001 From: "Jeremy G. Siek" Date: Wed, 16 Oct 2024 12:39:25 -0400 Subject: [PATCH] moved library files to lib directory --- Base.thm | 18 --- Binary.thm | 44 ------- FunctionalProgramming.thm | 4 - List.thm | 82 ------------ ListTests.thm | 4 - Log.thm | 8 -- Makefile | 25 ++-- Maps.thm | 14 --- MultiSet.thm | 22 ---- Nat.thm | 210 ------------------------------- NatTests.thm | 4 - Option.thm | 4 - Pair.thm | 4 - ProofIntro.thm | 50 -------- README.thm | 6 - Set.thm | 28 ----- Base.pf => lib/Base.pf | 0 Binary.pf => lib/Binary.pf | 0 List.pf => lib/List.pf | 0 ListTests.pf => lib/ListTests.pf | 0 Log.pf => lib/Log.pf | 0 Maps.pf => lib/Maps.pf | 0 MultiSet.pf => lib/MultiSet.pf | 0 Nat.pf => lib/Nat.pf | 0 NatTests.pf => lib/NatTests.pf | 0 Option.pf => lib/Option.pf | 0 Pair.pf => lib/Pair.pf | 0 Set.pf => lib/Set.pf | 0 sums.pf => lib/sums.pf | 0 29 files changed, 13 insertions(+), 514 deletions(-) delete mode 100644 Base.thm delete mode 100644 Binary.thm delete mode 100644 FunctionalProgramming.thm delete mode 100644 List.thm delete mode 100644 ListTests.thm delete mode 100644 Log.thm delete mode 100644 Maps.thm delete mode 100644 MultiSet.thm delete mode 100644 Nat.thm delete mode 100644 NatTests.thm delete mode 100644 Option.thm delete mode 100644 Pair.thm delete mode 100644 ProofIntro.thm delete mode 100644 README.thm delete mode 100644 Set.thm rename Base.pf => lib/Base.pf (100%) rename Binary.pf => lib/Binary.pf (100%) rename List.pf => lib/List.pf (100%) rename ListTests.pf => lib/ListTests.pf (100%) rename Log.pf => lib/Log.pf (100%) rename Maps.pf => lib/Maps.pf (100%) rename MultiSet.pf => lib/MultiSet.pf (100%) rename Nat.pf => lib/Nat.pf (100%) rename NatTests.pf => lib/NatTests.pf (100%) rename Option.pf => lib/Option.pf (100%) rename Pair.pf => lib/Pair.pf (100%) rename Set.pf => lib/Set.pf (100%) rename sums.pf => lib/sums.pf (100%) diff --git a/Base.thm b/Base.thm deleted file mode 100644 index 5e42d30..0000000 --- a/Base.thm +++ /dev/null @@ -1,18 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./Base.pf - -or_not: (all P:bool, Q:bool. (if ((P or Q) and not (P)) then Q)) - -ex_mid: (all b:bool. (b or not (b))) - -or_sym: (all P:bool, Q:bool. (P or Q) = (Q or P)) - -and_sym: (all P:bool, Q:bool. (P and Q) = (Q and P)) - -eq_true: (all P:bool. (if P then P = true)) - -eq_false: (all P:bool. (if not (P) then P = false)) - -iff_equal: (all P:bool, Q:bool. (if (P ⇔ Q) then P = Q)) - diff --git a/Binary.thm b/Binary.thm deleted file mode 100644 index 213929f..0000000 --- a/Binary.thm +++ /dev/null @@ -1,44 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./Binary.pf - -from_inc: (all bs:List. from_binary(inc(bs)) = suc(from_binary(bs))) - -from_to_binary: (all n:Nat. from_binary(to_binary(n)) = n) - -length_inc: (all b:List. 0 < length(inc(b))) - -add_nb_inc: (all m:Nat. (all bs:List. add_nb(m, inc(bs)) = inc(add_nb(m, bs)))) - -add_suc_to: (all m:Nat, n:Nat. add_nb(suc(m), to_binary(n)) = add_nb(m, to_binary(suc(n)))) - -add_nb_shift: (all m:Nat, bs:List. add_nb(m, inc(bs)) = add_nb(suc(m), bs)) - -to_binary_add: (all m:Nat. (all n:Nat. to_binary(m + n) = add_nb(m, to_binary(n)))) - -to_binary_2: (all n:Nat. to_binary(2 * n) = add_nb(n, to_binary(n))) - -binary_times_2: (all bs:List. from_binary(dub(bs)) = 2 * from_binary(bs)) - -length_dub: (all bs:List. length(dub(bs)) = 1 + length(bs)) - -length_iter_dub: (all n:Nat. (all bs:List. length(iter_dub(n, bs)) = n + length(bs))) - -length_iter_dub: (all n:Nat. length(iter_dub(n, to_binary(1))) = suc(n)) - -iter_dub_times2: (all n:Nat. (all bs:List. from_binary(iter_dub(n, bs)) = iter_times2(n, from_binary(bs)))) - -iter_times2_pow2: (all n:Nat. iter_times2(n, 1) = pow2(n)) - -iter_dub_pow2: (all n:Nat. from_binary(iter_dub(n, to_binary(1))) = pow2(n)) - -dv2_dub: (all bs:List. dv2(dub(bs)) = bs) - -iter_dv2_dub: (all n:Nat. (all bs:List. iter_dv2(n, iter_dub(n, bs)) = bs)) - -from_dub: (all bs:List. from_binary(dub(bs)) = 2 * from_binary(bs)) - -from_dv2: (all bs:List. from_binary(dv2(bs)) = div2(from_binary(bs))) - -blah: (all n:Nat. length(dub(to_binary(n))) = 1 + length(to_binary(n))) - diff --git a/FunctionalProgramming.thm b/FunctionalProgramming.thm deleted file mode 100644 index c288d7e..0000000 --- a/FunctionalProgramming.thm +++ /dev/null @@ -1,4 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./FunctionalProgramming.pf - diff --git a/List.thm b/List.thm deleted file mode 100644 index c3ff360..0000000 --- a/List.thm +++ /dev/null @@ -1,82 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./List.pf - -length_one_nat: (all x:Nat. length(node(x, [])) = 1) - -length_one: (all U:type. (all x:U. length(node(x, [])) = 1)) - -length_zero_empty: (all T:type. (all xs:List. (if length(xs) = 0 then xs = []))) - -length_append: (all U:type. (all xs:List. (all ys:List. length(xs ++ ys) = length(xs) + length(ys)))) - -append_assoc: (all U:type. (all xs:List. (all ys:List, zs:List. (xs ++ ys) ++ zs = xs ++ (ys ++ zs)))) - -append_empty: (all U:type. (all xs:List. xs ++ [] = xs)) - -length_reverse: (all U:type. (all xs:List. length(reverse(xs)) = length(xs))) - -length_map: (all T:type. (all f:(fn T -> T). (all xs:List. length(map(xs, f)) = length(xs)))) - -map_id: (all T:type. (all f:(fn T -> T). (if (all x:T. f(x) = x) then (all xs:List. map(xs, f) = xs)))) - -map_append: (all T:type. (all f:(fn T -> T), ys:List. (all xs:List. map(xs ++ ys, f) = map(xs, f) ++ map(ys, f)))) - -map_compose: (all T:type, U:type, V:type. (all f:(fn T -> U), g:(fn U -> V). (all ls:List. map(map(ls, f), g) = map(ls, g ∘ f)))) - -zip_id_right: (all T:type, U:type. (all xs:List. zip(xs, []) = [])) - -zip_map: (all T1:type, T2:type, U1:type, U2:type. (all f:(fn T1 -> T2), g:(fn U1 -> U2). (all xs:List. (all ys:List. zip(map(xs, f), map(ys, g)) = map(zip(xs, ys), pairfun(f, g)))))) - -filter_all: (all T:type. (all P:(fn T -> bool). (all xs:List. (if all_elements(xs, P) then filter(xs, P) = xs)))) - -all_elements_implies_member: (all T:type. (all xs:List. (all P:(fn T -> bool). (if all_elements(xs, P) then (all x:T. (if x ∈ set_of(xs) then P(x))))))) - -member_implies_all_elements: (all T:type. (all xs:List. (all P:(fn T -> bool). (if (all x:T. (if x ∈ set_of(xs) then P(x))) then all_elements(xs, P))))) - -all_elements_eq_member: (all T:type. (all xs:List, P:(fn T -> bool). all_elements(xs, P) = (all x:T. (if x ∈ set_of(xs) then P(x))))) - -all_elements_implies: (all T:type. (all xs:List. (all P:(fn T -> bool), Q:(fn T -> bool). (if (all_elements(xs, P) and (all z:T. (if P(z) then Q(z)))) then all_elements(xs, Q))))) - -set_of_empty: (all T:type. (all xs:List. (if set_of(xs) = char_fun(λ_{false}) then xs = []))) - -mset_of_empty: (all T:type. (all xs:List. (if mset_of(xs) = m_fun(λx{0}) then xs = []))) - -som_mset_eq_set: (all T:type. (all xs:List. set_of_mset(mset_of(xs)) = set_of(xs))) - -remove_all_absent: (all T:type. (all xs:List. (all y:T. not (y ∈ set_of(remove_all(xs, y)))))) - -all_elements_member: (all T:type. (all ys:List. (all x:T, P:(fn T -> bool). (if (all_elements(ys, P) and x ∈ set_of(ys)) then P(x))))) - -all_elements_set_of: (all T:type. (all xs:List, ys:List, P:(fn T -> bool). (if set_of(xs) = set_of(ys) then all_elements(xs, P) = all_elements(ys, P)))) - -set_of_append: (all T:type. (all xs:List. (all ys:List. set_of(xs ++ ys) = set_of(xs) ∪ set_of(ys)))) - -all_elements_append: (all T:type. (all xs:List. (all ys:List, P:(fn T -> bool). (if (all_elements(xs, P) and all_elements(ys, P)) then all_elements(xs ++ ys, P))))) - -take_append: (all E:type. (all xs:List. (all ys:List. take(length(xs), xs ++ ys) = xs))) - -nth_drop: (all T:type. (all n:Nat. (all xs:List, i:Nat, d:T. nth(drop(n, xs), d)(i) = nth(xs, d)(n + i)))) - -nth_append_front: (all T:type. (all xs:List. (all ys:List, i:Nat, d:T. (if i < length(xs) then nth(xs ++ ys, d)(i) = nth(xs, d)(i))))) - -nth_append_back: (all T:type. (all xs:List. (all ys:List, i:Nat, d:T. nth(xs ++ ys, d)(length(xs) + i) = nth(ys, d)(i)))) - -rev_app_reverse_append: (all T:type. (all xs:List. (all ys:List. rev_app(xs, ys) = reverse(xs) ++ ys))) - -foldr_rev_app_foldl: (all T:type. (all xs:List. (all ys:List, b:T, f:(fn T, T -> T). foldr(rev_app(xs, ys), b, f) = foldl(xs, foldr(ys, b, f), flip(f))))) - -flip_flip: (all T:type. (all f:(fn T, T -> T). flip(flip(f)) = f)) - -foldl_foldr: (all T:type. (all xs:List, b:T, f:(fn T, T -> T). foldl(xs, b, f) = foldr(reverse(xs), b, flip(f)))) - -mset_equal_implies_set_equal: (all T:type. (all xs:List, ys:List. (if mset_of(xs) = mset_of(ys) then set_of(xs) = set_of(ys)))) - -head_append: (all E:type. (all L:List. (all R:List. (if 0 < length(L) then head(L ++ R) = head(L))))) - -tail_append: (all E:type. (all L:List. (all R:List. (if 0 < length(L) then tail(L ++ R) = tail(L) ++ R)))) - -left_2list_identity: (all T:type. (all z:ListZipper. zip2list(z) = zip2list(zip_left(z)))) - -right_2list_identity: (all T:type. (all z:ListZipper. zip2list(z) = zip2list(zip_right(z)))) - diff --git a/ListTests.thm b/ListTests.thm deleted file mode 100644 index dd4ffee..0000000 --- a/ListTests.thm +++ /dev/null @@ -1,4 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./ListTests.pf - diff --git a/Log.thm b/Log.thm deleted file mode 100644 index eb79ce8..0000000 --- a/Log.thm +++ /dev/null @@ -1,8 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./Log.pf - -add_less_equal_pow_find_log: (all m:Nat. (all n:Nat, l:Nat. (if n ≤ pow2(l) then m + n ≤ pow2(find_log(m, n, l))))) - -less_equal_pow_log: (all n:Nat. n ≤ pow2(log(n))) - diff --git a/Makefile b/Makefile index c6da451..a4a7eb4 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,6 @@ PYTHON = $(shell command -v python3.11) +LIB_DIR = ./lib TEST_PASS_DIR = ./test/should-pass TEST_ERROR_DIR = ./test/should-error @@ -13,16 +14,16 @@ default: tests tests-lib # check_docs check_docs: check_index check_fun check_intro check_ref tests-should-pass: - $(PYTHON) ./deduce.py --recursive-descent $(TEST_PASS_DIR) - $(PYTHON) ./deduce.py --lalr $(TEST_PASS_DIR) + $(PYTHON) ./deduce.py --recursive-descent $(TEST_PASS_DIR) --dir $(LIB_DIR) + $(PYTHON) ./deduce.py --lalr $(TEST_PASS_DIR) --dir $(LIB_DIR) tests-should-error: - $(PYTHON) ./deduce.py --recursive-descent $(TEST_ERROR_DIR) --error - $(PYTHON) ./deduce.py --lalr $(TEST_ERROR_DIR) --error + $(PYTHON) ./deduce.py --recursive-descent $(TEST_ERROR_DIR) --error --dir $(LIB_DIR) + $(PYTHON) ./deduce.py --lalr $(TEST_ERROR_DIR) --error --dir $(LIB_DIR) tests-lib: - $(PYTHON) ./deduce.py . --recursive-descent + $(PYTHON) ./deduce.py ./lib --recursive-descent --dir $(LIB_DIR) # List parsing needs to be updated in Deduce.lark # $(PYTHON) ./deduce.py . --lalr @@ -30,25 +31,25 @@ tests: tests-should-pass tests-should-error check_index: /Users/jsiek/Library/Python/3.11/bin/entangled tangle - $(PYTHON) ./deduce.py --recursive-descent index.pf - $(PYTHON) ./deduce.py --lalr index.pf + $(PYTHON) ./deduce.py --recursive-descent index.pf --dir $(LIB_DIR) + $(PYTHON) ./deduce.py --lalr index.pf --dir $(LIB_DIR) check_fun: /Users/jsiek/Library/Python/3.11/bin/entangled tangle - $(PYTHON) ./deduce.py --recursive-descent FunctionalProgramming.pf + $(PYTHON) ./deduce.py --recursive-descent FunctionalProgramming.pf --dir $(LIB_DIR) # List parsing needs to be updated in Deduce.lark # $(PYTHON) ./deduce.py --lalr FunctionalProgramming.pf check_intro: /Users/jsiek/Library/Python/3.11/bin/entangled tangle - $(PYTHON) ./deduce.py --recursive-descent ProofIntro.pf + $(PYTHON) ./deduce.py --recursive-descent ProofIntro.pf --dir $(LIB_DIR) # List parsing needs to be updated in Deduce.lark -# $(PYTHON) ./deduce.py --lalr ProofIntro.pf +# $(PYTHON) ./deduce.py --lalr ProofIntro.pf --dir $(LIB_DIR) check_ref: /Users/jsiek/Library/Python/3.11/bin/entangled tangle - $(PYTHON) ./deduce.py --recursive-descent Reference.pf - $(PYTHON) ./deduce.py --lalr Reference.pf + $(PYTHON) ./deduce.py --recursive-descent Reference.pf --dir $(LIB_DIR) + $(PYTHON) ./deduce.py --lalr Reference.pf --dir $(LIB_DIR) clean: rm -f index.pf FunctionalProgramming.pf ProofIntro.pf diff --git a/Maps.thm b/Maps.thm deleted file mode 100644 index c768c5f..0000000 --- a/Maps.thm +++ /dev/null @@ -1,14 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./Maps.pf - -update_eq: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U. update(f, x, v)(x) = v)) - -update_not_eq: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U, y:T. (if not (x = y) then update(f, x, v)(y) = f(y)))) - -update_shadow: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U, w:U. update(update(f, x, v), x, w) = update(f, x, w))) - -update_permute: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U, w:U, y:T. (if not (x = y) then update(update(f, x, v), y, w) = update(update(f, y, w), x, v)))) - -restrict_domain: (all T:type, U:type. (all f:(fn T -> Option), P:Set. domain(restrict(f, P)) ⊆ P)) - diff --git a/MultiSet.thm b/MultiSet.thm deleted file mode 100644 index 62f6c45..0000000 --- a/MultiSet.thm +++ /dev/null @@ -1,22 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./MultiSet.pf - -m_one_cnt: (all T:type. (all x:T. cnt(m_one(x))(x) = 1)) - -m_empty_zero: (all T:type. (all x:T. cnt(m_fun(λy:T{0}))(x) = 0)) - -cnt_sum: (all T:type. (all A:MultiSet, B:MultiSet, x:T. cnt(A ⨄ B)(x) = cnt(A)(x) + cnt(B)(x))) - -m_sum_empty: (all T:type. (all A:MultiSet. A ⨄ m_fun(λy:T{0}) = A)) - -empty_m_sum: (all T:type. (all A:MultiSet. m_fun(λx:T{0}) ⨄ A = A)) - -m_sum_commutes: (all T:type. (all A:MultiSet, B:MultiSet. A ⨄ B = B ⨄ A)) - -m_sum_assoc: (all T:type. (all A:MultiSet, B:MultiSet, C:MultiSet. (A ⨄ B) ⨄ C = A ⨄ (B ⨄ C))) - -som_one_single: (all T:type. (all x:T. set_of_mset(m_one(x)) = single(x))) - -som_union: (all T:type. (all A:MultiSet, B:MultiSet. set_of_mset(A ⨄ B) = set_of_mset(A) ∪ set_of_mset(B))) - diff --git a/Nat.thm b/Nat.thm deleted file mode 100644 index 4a4ed98..0000000 --- a/Nat.thm +++ /dev/null @@ -1,210 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./Nat.pf - -zero_add: (all n:Nat. 0 + n = n) - -add_zero: (all n:Nat. n + 0 = n) - -suc_add: (all m:Nat, n:Nat. suc(m) + n = suc(m + n)) - -suc_one_add: (all n:Nat. suc(n) = 1 + n) - -one_add_suc: (all n:Nat. 1 + n = suc(n)) - -not_one_add_zero: (all n:Nat. not (1 + n = 0)) - -add_suc: (all m:Nat. (all n:Nat. m + suc(n) = suc(m + n))) - -add_commute: (all n:Nat. (all m:Nat. n + m = m + n)) - -one_add: (all m:Nat. 1 + m = suc(m)) - -add_one: (all m:Nat. m + 1 = suc(m)) - -add_assoc: (all m:Nat. (all n:Nat, o:Nat. (m + n) + o = m + (n + o))) - -left_cancel: (all x:Nat. (all y:Nat, z:Nat. (if x + y = x + z then y = z))) - -add_to_zero: (all n:Nat. (all m:Nat. (if n + m = 0 then (n = 0 and m = 0)))) - -pred_one: pred(1) = 0 - -sub_cancel: (all n:Nat. n - n = 0) - -sub_zero: (all n:Nat. n - 0 = n) - -add_sub_identity: (all m:Nat. (all n:Nat. (m + n) - m = n)) - -sub_sub_eq_sub_add: (all x:Nat. (all y:Nat. (all z:Nat. (x - y) - z = x - (y + z)))) - -zero_mult: (all n:Nat. 0 * n = 0) - -mult_zero: (all n:Nat. n * 0 = 0) - -suc_mult: (all m:Nat, n:Nat. suc(m) * n = n + m * n) - -mult_suc: (all m:Nat. (all n:Nat. m * suc(n) = m + m * n)) - -mult_commute: (all m:Nat. (all n:Nat. m * n = n * m)) - -one_mult: (all n:Nat. 1 * n = n) - -mult_one: (all n:Nat. n * 1 = n) - -two_mult: (all n:Nat. 2 * n = n + n) - -dist_mult_add: (all a:Nat. (all x:Nat, y:Nat. a * (x + y) = a * x + a * y)) - -dist_mult_add_right: (all x:Nat, y:Nat, a:Nat. (x + y) * a = x * a + y * a) - -mult_assoc: (all m:Nat. (all n:Nat, o:Nat. (m * n) * o = m * (n * o))) - -suc_less_equal_iff_less_equal_suc: (all x:Nat, y:Nat. (x ≤ y ⇔ suc(x) ≤ suc(y))) - -less_suc_iff_suc_less: (all x:Nat, y:Nat. (x < y ⇔ suc(x) < suc(y))) - -less_equal_implies_less_or_equal: (all x:Nat. (all y:Nat. (if x ≤ y then (x < y or x = y)))) - -less_implies_less_equal: (all x:Nat. (all y:Nat. (if x < y then x ≤ y))) - -less_equal_refl: (all n:Nat. n ≤ n) - -equal_implies_less_equal: (all x:Nat, y:Nat. (if x = y then x ≤ y)) - -less_equal_antisymmetric: (all x:Nat. (all y:Nat. (if (x ≤ y and y ≤ x) then x = y))) - -less_equal_trans: (all m:Nat. (all n:Nat, o:Nat. (if (m ≤ n and n ≤ o) then m ≤ o))) - -not_less_less_equal: (all x:Nat. (all y:Nat. (if not (x < y) then y ≤ x))) - -less_irreflexive: (all x:Nat. not (x < x)) - -less_not_equal: (all x:Nat, y:Nat. (if x < y then not (x = y))) - -greater_not_equal: (all x:Nat, y:Nat. (if x > y then not (x = y))) - -trichotomy: (all x:Nat. (all y:Nat. (x < y or x = y or y < x))) - -trichotomy2: (all y:Nat, x:Nat. (if (not (x = y) and not (x < y)) then y < x)) - -positive_1_and_2: (0 ≤ 1 and 0 ≤ 2) - -positive_2: 0 ≤ 2 - -less_implies_less_equal: (all x:Nat. (all y:Nat. (if x < y then x ≤ y))) - -dichotomy: (all x:Nat, y:Nat. (x ≤ y or y < x)) - -zero_or_positive: (all x:Nat. (x = 0 or 0 < x)) - -zero_le_zero: (all x:Nat. (if x ≤ 0 then x = 0)) - -not_less_equal_iff_greater: (all x:Nat, y:Nat. (not (x ≤ y) ⇔ y < x)) - -less_implies_not_greater: (all x:Nat. (all y:Nat. (if x < y then not (y < x)))) - -not_less_equal_less_equal: (all x:Nat, y:Nat. (if not (x ≤ y) then y ≤ x)) - -not_zero_suc: (all n:Nat. (if not (n = 0) then some n':Nat. n = suc(n'))) - -positive_suc: (all n:Nat. (if 0 < n then some n':Nat. n = suc(n'))) - -less_equal_add: (all x:Nat. (all y:Nat. x ≤ x + y)) - -less_equal_add_left: (all x:Nat, y:Nat. y ≤ x + y) - -less_equal_suc: (all n:Nat. n ≤ suc(n)) - -less_trans: (all m:Nat, n:Nat, o:Nat. (if (m < n and n < o) then m < o)) - -less_one_add: (all n:Nat. 0 < 1 + n) - -greater_any_zero: (all x:Nat, y:Nat. (if x < y then 0 < y)) - -less_equal_left_cancel: (all x:Nat. (all y:Nat, z:Nat. (x + y ≤ x + z ⇔ y ≤ z))) - -less_left_cancel: (all x:Nat, y:Nat, z:Nat. (x + y < x + z ⇔ y < z)) - -mult_mono_le: (all n:Nat. (all x:Nat, y:Nat. (if x ≤ y then n * x ≤ n * y))) - -sub_add_assoc: (all n:Nat. (all l:Nat, m:Nat. (if m ≤ n then l + (n - m) = (l + n) - m))) - -sub_add_identity: (all n:Nat. (all m:Nat. (if m ≤ n then m + (n - m) = n))) - -less_equal_add_sub: (all m:Nat. (all n:Nat, o:Nat. (if (n ≤ m and m ≤ n + o) then m - n ≤ o))) - -sub_less_zero: (all x:Nat. (all y:Nat. (if x ≤ y then x - y = 0))) - -dist_mult_sub: (all x:Nat. (all y:Nat, z:Nat. x * (y - z) = x * y - x * z)) - -max_same: (all x:Nat. max(x, x) = x) - -max_suc: (all x:Nat. max(suc(x), x) = suc(max(x, x))) - -max_suc2: (all x:Nat, y:Nat. max(suc(x), suc(y)) = suc(max(x, y))) - -max_greater_right: (all y:Nat. (all x:Nat. y ≤ max(x, y))) - -max_greater_left: (all x:Nat. (all y:Nat. x ≤ max(x, y))) - -max_is_left_or_right: (all x:Nat. (all y:Nat. (max(x, y) = x or max(x, y) = y))) - -zero_max: (all x:Nat. max(0, x) = x) - -max_zero: (all x:Nat. max(x, 0) = x) - -max_symmetric: (all x:Nat. (all y:Nat. max(x, y) = max(y, x))) - -max_assoc: (all x:Nat. (all y:Nat, z:Nat. max(max(x, y), z) = max(x, max(y, z)))) - -max_equal_greater_right: (all x:Nat. (all y:Nat. (if x ≤ y then max(x, y) = y))) - -max_equal_greater_left: (all x:Nat. (all y:Nat. (if y ≤ x then max(x, y) = x))) - -max_less_equal: (all x:Nat. (all y:Nat, z:Nat. (if (x ≤ z and y ≤ z) then max(x, y) ≤ z))) - -addition_of_evens: (all x:Nat, y:Nat. (if (Even(x) and Even(y)) then Even(x + y))) - -is_even_odd: (all n:Nat. ((if is_even(n) then Even(n)) and (if is_odd(n) then Odd(n)))) - -summation_cong: (all k:Nat. (all f:(fn Nat -> Nat), g:(fn Nat -> Nat), s:Nat, t:Nat. (if (all i:Nat. (if i < k then f(s + i) = g(t + i))) then summation(k, s, f) = summation(k, t, g)))) - -summation_cong4: (all k:Nat. (all f:(fn Nat -> Nat), g:(fn Nat -> Nat), s:Nat. (if (all i:Nat. (if (s ≤ i and i < s + k) then f(i) = g(i))) then summation(k, s, f) = summation(k, s, g)))) - -summation_suc: (all k:Nat. (all f:(fn Nat -> Nat), g:(fn Nat -> Nat), s:Nat. (if (all i:Nat. f(i) = g(suc(i))) then summation(k, s, f) = summation(k, suc(s), g)))) - -summation_cong3: (all k:Nat. (all f:(fn Nat -> Nat), g:(fn Nat -> Nat), s:Nat, t:Nat. (if (all i:Nat. f(s + i) = g(t + i)) then summation(k, s, f) = summation(k, t, g)))) - -summation_add: (all a:Nat. (all b:Nat, s:Nat, t:Nat, f:(fn Nat -> Nat), g:(fn Nat -> Nat), h:(fn Nat -> Nat). (if ((all i:Nat. (if i < a then g(s + i) = f(s + i))) and (all i:Nat. (if i < b then h(t + i) = f(s + (a + i))))) then summation(a + b, s, f) = summation(a, s, g) + summation(b, t, h)))) - -equal_refl: (all n:Nat. equal(n, n)) - -equal_complete_sound: (all m:Nat. (all n:Nat. (m = n ⇔ equal(m, n)))) - -not_equal_not_eq: (all m:Nat, n:Nat. (if not (equal(m, n)) then not (m = n))) - -div2_add_2: (all n:Nat. div2(suc(suc(n))) = suc(div2(n))) - -div2_double: (all n:Nat. div2(n + n) = n) - -div2_times2: (all n:Nat. div2(2 * n) = n) - -div2_suc_double: (all n:Nat. div2(suc(n + n)) = n) - -div2_suc_times2: (all n:Nat. div2(suc(2 * n)) = n) - -pos_positive: (all p:Pos. 0 < pos2nat(p)) - -pow_positive: (all n:Nat. 0 < pow2(n)) - -find_quotient_correct: (all u:Nat. (all q:Nat, n:Nat, m:Pos. (if (q * pos2nat(m) ≤ n and n < u * pos2nat(m)) then some r:Nat. (find_quotient(u, n, m, q) * pos2nat(m) + r = n and r < pos2nat(m))))) - -mod_def: (all n:Nat, m:Pos. n % m = n - (n / m) * pos2nat(m)) - -division: (all n:Nat, m:Pos. some r:Nat. ((n / m) * pos2nat(m) + r = n and r < pos2nat(m))) - -division_remainder: (all n:Nat, m:Pos. (n / m) * pos2nat(m) + n % m = n) - -remainder_less_divisor: (all n:Nat, m:Pos. n % m < pos2nat(m)) - diff --git a/NatTests.thm b/NatTests.thm deleted file mode 100644 index 482d681..0000000 --- a/NatTests.thm +++ /dev/null @@ -1,4 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./NatTests.pf - diff --git a/Option.thm b/Option.thm deleted file mode 100644 index 4fa4bc1..0000000 --- a/Option.thm +++ /dev/null @@ -1,4 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./Option.pf - diff --git a/Pair.thm b/Pair.thm deleted file mode 100644 index 2c17bba..0000000 --- a/Pair.thm +++ /dev/null @@ -1,4 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./Pair.pf - diff --git a/ProofIntro.thm b/ProofIntro.thm deleted file mode 100644 index 851cf84..0000000 --- a/ProofIntro.thm +++ /dev/null @@ -1,50 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./ProofIntro.pf - -length_nat_empty: length([]) = 0 - -length_node42: length(node(42, [])) = 1 - -append_12: node(1, []) ++ node(2, []) = node(1, node(2, [])) - -length_one_nat: (all x:Nat. length(node(x, [])) = 1) - -length_node42_again: length(node(42, [])) = 1 - -length_one: (all U:type. (all x:U. length(node(x, [])) = 1)) - -length_one_equal: (all U:type. (all x:U, y:U. length(node(x, [])) = length(node(y, [])))) - -less_max: (all x:Nat, y:Nat. x ≤ max'(x, y)) - -append_empty: (all U:type. (all xs:List. xs ++ [] = xs)) - -xyz_zyx: (all x:Nat, y:Nat, z:Nat. x + (y + z) = z + (y + x)) - -xyz_zyx_eqn: (all x:Nat, y:Nat, z:Nat. x + (y + z) = z + (y + x)) - -positive_1_and_2: (0 ≤ 1 and 0 ≤ 2) - -positive_2: 0 ≤ 2 - -dichotomy: (all x:Nat, y:Nat. (x ≤ y or y < x)) - -length_zero_empty: (all T:type. (all xs:List. (if length(xs) = 0 then xs = []))) - -length_append_zero_empty: (all T:type. (all xs:List, ys:List. (if length(xs ++ ys) = 0 then (xs = [] and ys = [])))) - -really_trivial: true - -contra_false: (all a:bool, b:bool. not ((a = b and a = true and b = false))) - -false_any: (all x:bool, y:bool. (if false then x = y)) - -less_irreflexive: (all x:Nat. not (x < x)) - -less_not_equal: (all x:Nat, y:Nat. (if x < y then not (x = y))) - -zero_or_positive: (all x:Nat. (x = 0 or 0 < x)) - -addition_of_evens: (all x:Nat, y:Nat. (if (Even(x) and Even(y)) then Even(x + y))) - diff --git a/README.thm b/README.thm deleted file mode 100644 index 07907a8..0000000 --- a/README.thm +++ /dev/null @@ -1,6 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./README.pf - -search_take: (all xs:List. (all y:Nat. not (y ∈ set_of(take(search(xs, y), xs))))) - diff --git a/Set.thm b/Set.thm deleted file mode 100644 index 3c61815..0000000 --- a/Set.thm +++ /dev/null @@ -1,28 +0,0 @@ -This file was automatically generated by Deduce. -This file summarizes the theorems proved in the file: - ./Set.pf - -single_member: (all T:type. (all x:T. x ∈ single(x))) - -single_equal: (all T:type. (all x:T, y:T. (if y ∈ single(x) then x = y))) - -empty_no_members: (all T:type. (all x:T. not (x ∈ char_fun(λ_{false})))) - -union_member: (all T:type. (all x:T, A:Set, B:Set. (if (x ∈ A or x ∈ B) then x ∈ A ∪ B))) - -member_union: (all T:type. (all x:T, A:Set, B:Set. (if x ∈ A ∪ B then (x ∈ A or x ∈ B)))) - -union_empty: (all T:type. (all A:Set. A ∪ char_fun(λ_{false}) = A)) - -empty_union: (all T:type. (all A:Set. ∅ ∪ A = A)) - -union_sym: (all T:type. (all A:Set, B:Set. A ∪ B = B ∪ A)) - -union_assoc: (all T:type. (all A:Set, B:Set, C:Set. A ∪ B ∪ C = A ∪ B ∪ C)) - -in_left_union: (all T:type. (all B:Set. (all x:T, A:Set. (if x ∈ A then x ∈ A ∪ B)))) - -in_right_union: (all T:type. (all A:Set. (all x:T, B:Set. (if x ∈ B then x ∈ A ∪ B)))) - -subset_equal: (all T:type. (all A:Set, B:Set. (if (A ⊆ B and B ⊆ A) then A = B))) - diff --git a/Base.pf b/lib/Base.pf similarity index 100% rename from Base.pf rename to lib/Base.pf diff --git a/Binary.pf b/lib/Binary.pf similarity index 100% rename from Binary.pf rename to lib/Binary.pf diff --git a/List.pf b/lib/List.pf similarity index 100% rename from List.pf rename to lib/List.pf diff --git a/ListTests.pf b/lib/ListTests.pf similarity index 100% rename from ListTests.pf rename to lib/ListTests.pf diff --git a/Log.pf b/lib/Log.pf similarity index 100% rename from Log.pf rename to lib/Log.pf diff --git a/Maps.pf b/lib/Maps.pf similarity index 100% rename from Maps.pf rename to lib/Maps.pf diff --git a/MultiSet.pf b/lib/MultiSet.pf similarity index 100% rename from MultiSet.pf rename to lib/MultiSet.pf diff --git a/Nat.pf b/lib/Nat.pf similarity index 100% rename from Nat.pf rename to lib/Nat.pf diff --git a/NatTests.pf b/lib/NatTests.pf similarity index 100% rename from NatTests.pf rename to lib/NatTests.pf diff --git a/Option.pf b/lib/Option.pf similarity index 100% rename from Option.pf rename to lib/Option.pf diff --git a/Pair.pf b/lib/Pair.pf similarity index 100% rename from Pair.pf rename to lib/Pair.pf diff --git a/Set.pf b/lib/Set.pf similarity index 100% rename from Set.pf rename to lib/Set.pf diff --git a/sums.pf b/lib/sums.pf similarity index 100% rename from sums.pf rename to lib/sums.pf