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