diff --git a/Binary.pf b/Binary.pf index f6b4bbb..d6b5cbe 100644 --- a/Binary.pf +++ b/Binary.pf @@ -100,7 +100,7 @@ proof = from_binary(node(true,empty)) by definition inc ... = suc(2 * 0) by definition {from_binary, from_binary} ... = 1 by rewrite mult_zero[2] - ... ={ suc(from_binary(empty)) } by definition from_binary + ... =# suc(from_binary(empty)) # by definition from_binary } case node(b, bs') suppose IH: from_binary(inc(bs')) = suc(from_binary(bs')) { switch b { @@ -115,15 +115,15 @@ proof by definition operator+ ... = suc(suc(from_binary(bs') + from_binary(bs'))) by rewrite add_suc[from_binary(bs')][from_binary(bs')] - ... ={ suc(suc(2 * from_binary(bs'))) } by rewrite two_mult[from_binary(bs')] - ... ={ suc(from_binary(node(true,bs'))) } by definition {from_binary} + ... =# suc(suc(2 * from_binary(bs'))) # by rewrite two_mult[from_binary(bs')] + ... =# suc(from_binary(node(true,bs'))) # by definition {from_binary} } case false { equations from_binary(inc(node(false,bs'))) = from_binary(node(true,bs')) by definition inc ... = suc(2 * from_binary(bs')) by definition from_binary - ... ={ suc(from_binary(node(false,bs'))) } by definition from_binary + ... =# suc(from_binary(node(false,bs'))) # by definition from_binary } } } diff --git a/Deduce.lark b/Deduce.lark index 43008ec..afef7ba 100644 --- a/Deduce.lark +++ b/Deduce.lark @@ -95,7 +95,7 @@ ident: IDENT -> ident | "─" -> omitted_term | "(" term ")" -> paren | "[" term_list "]" -> list_literal - | "{" term "}" -> mark + | "#" term "#" -> mark | "%" type ?term_list: -> empty diff --git a/List.pf b/List.pf index 5c5311c..9689504 100644 --- a/List.pf +++ b/List.pf @@ -296,7 +296,7 @@ proof length(map(node(x,ls'),f)) = 1 + length(map(ls',f)) by definition {map, length} ... = 1 + length(ls') by rewrite IH - ... ={ length(node(x,ls')) } by definition {length} + ... =# length(node(x,ls')) # by definition {length} } end @@ -331,8 +331,8 @@ proof equations map(@empty ++ ys, f) = map(ys, f) by definition operator++ - ... ={ @empty ++ map(ys, f) } by definition operator++ - ... ={ map(@empty, f) ++ map(ys, f) } by definition map + ... =# @empty ++ map(ys, f) # by definition operator++ + ... =# map(@empty, f) ++ map(ys, f) # by definition map } case node(x, xs') suppose IH: map(xs' ++ ys, f) = map(xs',f) ++ map(ys, f) @@ -397,7 +397,7 @@ proof by rewrite IH[ys'] ... = node(pair(f(x), g(y)), map(zip(xs', ys'), λp{pair(f(first(p)), g(second(p)))})) by definition pairfun - ... ={ map(zip(node(x,xs'),node(y,ys')), pairfun(f,g)) } + ... =# map(zip(node(x,xs'),node(y,ys')), pairfun(f,g)) # by definition {pairfun, first, second} } } @@ -817,7 +817,7 @@ proof equations rev_app(xs', node(x,ys)) = reverse(xs') ++ node(x,ys) by IH[node(x,ys)] - ... = reverse(xs') ++ { (node(x,empty) ++ ys) } + ... = reverse(xs') ++ # (node(x,empty) ++ ys) # by definition {operator++,operator++} ... = (reverse(xs') ++ node(x,empty)) ++ ys by symmetric append_assoc[reverse(xs')][node(x,empty),ys] @@ -861,7 +861,7 @@ proof arbitrary xs:List, b:T, f:fn T,T->T equations foldl(xs, b, f) - ={ foldl(xs,foldr(@empty, b, flip(f)), flip(flip(f))) } + =# foldl(xs,foldr(@empty, b, flip(f)), flip(flip(f))) # by definition foldr and rewrite flip_flip[f] ... = foldr(rev_app(xs,empty),b,flip(f)) by symmetric foldr_rev_app_foldl[xs][empty,b,flip(f)] @@ -904,7 +904,7 @@ proof equations head(node(x,xs) ++ R) = just(x) by definition {operator++,head} - ... ={ head(node(x,xs)) } by definition head + ... =# head(node(x,xs)) # by definition head } end diff --git a/Makefile b/Makefile index f9c08d8..c6da451 100644 --- a/Makefile +++ b/Makefile @@ -3,9 +3,14 @@ PYTHON = $(shell command -v python3.11) TEST_PASS_DIR = ./test/should-pass TEST_ERROR_DIR = ./test/should-error -default: tests check_docs tests-lib +default: tests tests-lib # check_docs -check_docs: check_README check_fun check_intro check_ref +# Problem regarding the docs: github pages markdown is not compatible +# with using entangled, so the entangled syntax is currently commented +# out. We need a way to automatically put the entangled syntax back in +# and then run deduce on these files. -Jeremy + +check_docs: check_index check_fun check_intro check_ref tests-should-pass: $(PYTHON) ./deduce.py --recursive-descent $(TEST_PASS_DIR) @@ -23,10 +28,10 @@ tests-lib: tests: tests-should-pass tests-should-error -check_README: +check_index: /Users/jsiek/Library/Python/3.11/bin/entangled tangle - $(PYTHON) ./deduce.py --recursive-descent README.pf - $(PYTHON) ./deduce.py --lalr README.pf + $(PYTHON) ./deduce.py --recursive-descent index.pf + $(PYTHON) ./deduce.py --lalr index.pf check_fun: /Users/jsiek/Library/Python/3.11/bin/entangled tangle @@ -46,5 +51,5 @@ check_ref: $(PYTHON) ./deduce.py --lalr Reference.pf clean: - rm -f README.pf FunctionalProgramming.pf ProofIntro.pf + rm -f index.pf FunctionalProgramming.pf ProofIntro.pf rm -rf .entangled diff --git a/Nat.pf b/Nat.pf index f399fad..261d574 100644 --- a/Nat.pf +++ b/Nat.pf @@ -182,7 +182,7 @@ theorem suc_one_add: all n:Nat. proof arbitrary n:Nat equations - suc(n) ={ suc(0 + n) } by definition operator+ + suc(n) =# suc(0 + n) # by definition operator+ ... = suc(0) + n by symmetric suc_add[0, n] end @@ -448,7 +448,7 @@ proof by definition {operator*, operator+} equations suc(n + m' * suc(n)) = suc(n + (m' + m' * n)) by rewrite IH[n] - ... = suc( {(n + m') + m' * n} ) by rewrite add_assoc[n][m', m' * n] + ... = suc( #(n + m') + m' * n# ) by rewrite add_assoc[n][m', m' * n] ... = suc((m' + n) + m' * n) by rewrite add_commute[n][m'] ... = suc(m' + (n + m' * n)) by rewrite add_assoc[m'][n, m' * n] } @@ -507,7 +507,7 @@ proof equations 0 * (x + y) = 0 by zero_mult[x+y] ... = 0 + 0 by symmetric add_zero[0] - ... ={ 0 * x + 0 * y } by rewrite zero_mult[x] | zero_mult[y] + ... =# 0 * x + 0 * y # by rewrite zero_mult[x] | zero_mult[y] } case suc(a') suppose IH { arbitrary x:Nat, y:Nat @@ -553,7 +553,7 @@ proof = (n + m' * n) * o by definition operator* ... = n * o + (m' * n) * o by dist_mult_add_right[n, m'*n, o] ... = n * o + m' * (n * o) by rewrite IH[n,o] - ... = {suc(m') * (n * o)} by definition operator* + ... =# suc(m') * (n * o) # by definition operator* } end @@ -1411,10 +1411,10 @@ proof } case suc(x') suppose IH { equations - {max(suc(suc(x')),suc(x'))} = suc(max(suc(x'),x')) + # max(suc(suc(x')),suc(x')) #= suc(max(suc(x'),x')) by definition max ... = suc(suc(max(x',x'))) by rewrite IH - ... = {suc(max(suc(x'),suc(x')))} by definition max + ... =# suc(max(suc(x'),suc(x'))) # by definition max } end @@ -2213,7 +2213,7 @@ proof ... = suc(M) * ((n + M * n) + M) + M by rewrite mult_commute[((n + M * n) + M)][suc(M)] ... = (((n + M * n) + M) + M * ((n + M * n) + M)) + M by definition operator* - ... = ({n + M * n + M} + M * ((n + M * n) + M)) + M + ... = (#n + M * n + M# + M * ((n + M * n) + M)) + M by rewrite symmetric add_assoc[n][M*n,M] ... = (n + (M * n + M)) + (M * ((n + M * n) + M) + M) by rewrite add_assoc[(n + M * n + M)][M * ((n + M * n) + M),M] diff --git a/Nat.thm b/Nat.thm index 71de5b0..4a4ed98 100644 --- a/Nat.thm +++ b/Nat.thm @@ -1,6 +1,6 @@ This file was automatically generated by Deduce. This file summarizes the theorems proved in the file: - Nat.pf + ./Nat.pf zero_add: (all n:Nat. 0 + n = n) diff --git a/Reference.md b/Reference.md index c9f8e31..4f3d49d 100644 --- a/Reference.md +++ b/Reference.md @@ -1047,10 +1047,10 @@ define list_example = node(3, node(8, node(4, empty))) ## Mark ``` -term ::= "{" term "}" +term ::= "#" term "#" ``` -Marking a subterm with curly-braces restricts a `rewrite` or `definition` +Marking a subterm with hash symbols restricts a `rewrite` or `definition` proof to only apply to that subterm. @@ -1060,9 +1060,9 @@ proof arbitrary x:Nat suppose: x = 1 equations - {x} + x + x = 1 + x + x by rewrite recall x = 1 - $ 1 + {x} + x = 1 + 1 + x by rewrite recall x = 1 - $ 1 + 1 + {x} = 1 + 1 + 1 by rewrite recall x = 1 + #x# + x + x = 1 + x + x by rewrite recall x = 1 + $ 1 + #x# + x = 1 + 1 + x by rewrite recall x = 1 + $ 1 + 1 + #x# = 1 + 1 + 1 by rewrite recall x = 1 ... = 3 by definition {operator+,operator+} end ``` @@ -1121,6 +1121,13 @@ Example: assert 2 * 3 = 6 ``` +## MultiSet (Type) + +The `MultiSet` type represents the standard mathematical notion of +a multiset, which is a set that may contain duplicates of an +element. The `MultiSet` type is defined in `MultiSet.pf`. + + ## Not ``` @@ -1286,6 +1293,16 @@ proof ::= reflexive The proof `reflexive` proves that `a = a` for any term `a`. +## Set (Type) + +The `Set` type defined in `Set.pf` represents the standard +mathematical notion of a set. The empty set is written `∅` and the +usual set operations such as union `∪`, intersection `∩`, membership +`∈`, and subset-or-equal `⊆` are all defined in `Set.pf`. The +`Set.thm` file provides a summary of the many theorems about sets that +are proved in `Set.pf`. + + ## Some (Existential Quantifier) ``` diff --git a/index.md b/index.md index 00a142d..441c9d2 100644 --- a/index.md +++ b/index.md @@ -191,7 +191,7 @@ you can use instead. - +