Commit 312b3fe75b0828204f710669fbdcee3837b42535 - Eqthy

+0

-1

.reuse/dep5 less more

3	3	.gitignore
4	4	bin/eqthy
5	5	src/eqthy/__init__.py
6		test.sh
7	6	Copyright: The authors of these works have dedicated them to the public domain.
8	7	License: Unlicense

+1

-0

README.md less more

43	43	* in [Propositional Algebra](eg/propositional-algebra.eqthy.md);
44	44	* of De Morgan's laws in [Boolean Algebra](eg/boolean-algebra.eqthy.md);
45	45	* in [Combinatory Logic](eg/combinatory-logic.eqthy.md),
	46	* of some properties of [set difference](eg/set-difference.eqthy.md),
46	47
47	48	with hopefully more to come in the future.
48	49

+0

-57

~~eg/further-develop/set-difference.eqthy.md~~ less more

0		Set Difference
1		==============
2
3		<!--
4		SPDX-FileCopyrightText: The authors of this work have dedicated it to the public domain.
5		For more information, please refer to <https://unlicense.org/>
6		SPDX-License-Identifier: Unlicense
7		-->
8
9		Some theorems about set difference.
10
11		Using the [Algebra of sets (Wikipedia)](https://en.wikipedia.org/wiki/Algebra_of_sets)
12		as a basis.
13
14		Include [../algebra-of-sets.eqthy.md](../algebra-of-sets.eqthy.md) before this file!
15
16		axiom (#union-de-morg) comp(inter(A, B)) = union(comp(A), comp(B))
17		axiom (#inter-de-morg) comp(union(A, B)) = inter(comp(A), comp(B))
18
19		Definition of set difference.
20
21		axiom (#diff) diff(A, B) = inter(A, comp(B))
22
23		A theorem about set difference: difference distributes over union.
24
25		theorem (#diff-union-distrib)
26		union(diff(A, C), diff(B, C)) = diff(union(A, B), C)
27		proof
28		union(diff(A, C), diff(B, C)) = union(diff(A, C), diff(B, C))
29		union(diff(A, C), diff(B, C)) = union(diff(A, C), inter(B, comp(C)))
30		union(diff(A, C), diff(B, C)) = union(inter(A, comp(C)), inter(B, comp(C)))
31		union(diff(A, C), diff(B, C)) = union(inter(A, comp(C)), inter(comp(C), B))
32		union(diff(A, C), diff(B, C)) = union(inter(comp(C), A), inter(comp(C), B))
33		union(diff(A, C), diff(B, C)) = inter(comp(C), union(A, B))
34		union(diff(A, C), diff(B, C)) = inter(union(A, B), comp(C))
35		union(diff(A, C), diff(B, C)) = diff(union(A, B), C)
36		qed
37
38		Another theorem about set difference. This one uses De Morgan's law, which
39		has been added as an axiom above. For a working-out of it, see the
40		Boolean algebra document.
41
42		theorem (#diff-of-inter-is-diff)
43		diff(A, B) = diff(A, inter(A, B))
44		proof
45		diff(A, B) = diff(A, B)
46		diff(A, B) = inter(A, comp(B))
47		diff(A, B) = union(inter(A, comp(B)), e)
48		diff(A, B) = union(e, inter(A, comp(B)))
49		diff(A, B) = union(inter(A, comp(A)), inter(A, comp(B)))
50		diff(A, B) = inter(A, union(comp(A), comp(B)))
51		diff(A, B) = inter(A, comp(inter(A, B)))
52		diff(A, B) = diff(A, inter(A, B))
53		qed
54
55		Both of these theorems were adapted from
56		[this presentation by Mustafa Jarrar](http://www.jarrar.info/courses/DMath/Jarrar.LectureNotes.6.3%20Algebric%20Proofs.pdf).

+57

-0

eg/set-difference.eqthy.md less more

	0	Set Difference
	1	==============
	2
	3	<!--
	4	SPDX-FileCopyrightText: The authors of this work have dedicated it to the public domain.
	5	For more information, please refer to <https://unlicense.org/>
	6	SPDX-License-Identifier: Unlicense
	7	-->
	8
	9	Some theorems about set difference.
	10
	11	Using the [Algebra of sets (Wikipedia)](https://en.wikipedia.org/wiki/Algebra_of_sets)
	12	as a basis.
	13
	14	Include [../algebra-of-sets.eqthy.md](../algebra-of-sets.eqthy.md) before this file!
	15
	16	axiom (#union-de-morg) comp(inter(A, B)) = union(comp(A), comp(B))
	17	axiom (#inter-de-morg) comp(union(A, B)) = inter(comp(A), comp(B))
	18
	19	Definition of set difference.
	20
	21	axiom (#diff) diff(A, B) = inter(A, comp(B))
	22
	23	A theorem about set difference: difference distributes over union.
	24
	25	theorem (#diff-union-distrib)
	26	union(diff(A, C), diff(B, C)) = diff(union(A, B), C)
	27	proof
	28	union(diff(A, C), diff(B, C)) = union(diff(A, C), diff(B, C))
	29	union(diff(A, C), diff(B, C)) = union(diff(A, C), inter(B, comp(C)))
	30	union(diff(A, C), diff(B, C)) = union(inter(A, comp(C)), inter(B, comp(C)))
	31	union(diff(A, C), diff(B, C)) = union(inter(A, comp(C)), inter(comp(C), B))
	32	union(diff(A, C), diff(B, C)) = union(inter(comp(C), A), inter(comp(C), B))
	33	union(diff(A, C), diff(B, C)) = inter(comp(C), union(A, B))
	34	union(diff(A, C), diff(B, C)) = inter(union(A, B), comp(C))
	35	union(diff(A, C), diff(B, C)) = diff(union(A, B), C)
	36	qed
	37
	38	Another theorem about set difference. This one uses De Morgan's law, which
	39	has been added as an axiom above. For a working-out of it, see the
	40	Boolean algebra document.
	41
	42	theorem (#diff-of-inter-is-diff)
	43	diff(A, B) = diff(A, inter(A, B))
	44	proof
	45	diff(A, B) = diff(A, B)
	46	diff(A, B) = inter(A, comp(B))
	47	diff(A, B) = union(inter(A, comp(B)), e)
	48	diff(A, B) = union(e, inter(A, comp(B)))
	49	diff(A, B) = union(inter(A, comp(A)), inter(A, comp(B)))
	50	diff(A, B) = inter(A, union(comp(A), comp(B)))
	51	diff(A, B) = inter(A, comp(inter(A, B)))
	52	diff(A, B) = diff(A, inter(A, B))
	53	qed
	54
	55	Both of these theorems were adapted from
	56	[this presentation by Mustafa Jarrar](http://www.jarrar.info/courses/DMath/Jarrar.LectureNotes.6.3%20Algebric%20Proofs.pdf).

+16

-3

test.sh less more

0	0	#!/bin/sh -e
	1
	2	# SPDX-FileCopyrightText: The authors of this work have dedicated it to the public domain.
	3	# For more information, please refer to <https://unlicense.org/>
	4	# SPDX-License-Identifier: Unlicense
1	5
2	6	if command -v flake8 > /dev/null; then
3	7	echo "flake8 --ignore=E501 src"

14	18	fi
15	19
16	20	if command -v reuse > /dev/null; then
17		reuse lint
	21	echo "reuse lint --quiet"
	22	reuse lint --quiet \|\| reuse lint
18	23	else
19	24	echo "reuse not found, skipping check"
20	25	fi
21	26
22	27	falderal doc/*.md \|\| exit 1
23	28	for F in eg/*.eqthy.md; do
24		echo "./bin/eqthy $F"
25		./bin/eqthy --traceback $F \|\| exit 1
	29	case "$F" in
	30	set-difference)
	31	echo "./bin/eqthy eg/algebra-of-sets.eqthy.md $F"
	32	./bin/eqthy --traceback eg/algebra-of-sets.eqthy.md $F \|\| exit 1
	33	;;
	34	*)
	35	echo "./bin/eqthy $F"
	36	./bin/eqthy --traceback $F \|\| exit 1
	37	;;
	38	esac
26	39	done
27	40	for F in eg/incorrect/*.eqthy.md; do
28	41	echo $F