diff options
Diffstat (limited to 'test/examples')
| -rw-r--r-- | test/examples/abbr.tex | 45 | ||||
| -rw-r--r-- | test/examples/byRef.tex | 25 | ||||
| -rw-r--r-- | test/examples/calc.tex | 33 | ||||
| -rw-r--r-- | test/examples/coord.tex | 37 | ||||
| -rw-r--r-- | test/examples/finite-set-terms.tex | 11 | ||||
| -rw-r--r-- | test/examples/formula.tex | 7 | ||||
| -rw-r--r-- | test/examples/geometry.tex | 132 | ||||
| -rw-r--r-- | test/examples/indefinite-terms.tex | 7 | ||||
| -rw-r--r-- | test/examples/inductive.tex | 74 | ||||
| -rw-r--r-- | test/examples/no-reflexive-set.tex | 11 | ||||
| -rw-r--r-- | test/examples/proofassume.tex | 16 | ||||
| -rw-r--r-- | test/examples/proofdefinefunction.tex | 27 | ||||
| -rw-r--r-- | test/examples/prooffix.tex | 16 | ||||
| -rw-r--r-- | test/examples/relation-notation.tex | 3 | ||||
| -rw-r--r-- | test/examples/replace.tex | 27 | ||||
| -rw-r--r-- | test/examples/russell.tex | 16 | ||||
| -rw-r--r-- | test/examples/separation.tex | 3 | ||||
| -rw-r--r-- | test/examples/union.tex | 21 |
18 files changed, 511 insertions, 0 deletions
diff --git a/test/examples/abbr.tex b/test/examples/abbr.tex new file mode 100644 index 0000000..c4790bb --- /dev/null +++ b/test/examples/abbr.tex @@ -0,0 +1,45 @@ +\begin{abbreviation}\label{empty} + $x$ is empty iff there exists no $y$ such that $y\in x$. +\end{abbreviation} + +\begin{proposition}\label{dummy_abbr_test_adj} + If $x$ is empty, then $x$ is empty. +\end{proposition} + + +% Dummy abbreviation to test noun abbreviations. +\begin{abbreviation}\label{function} + $x$ is a function iff $x = x$. +\end{abbreviation} + +\begin{proposition}\label{dummy_abbr_test_noun} + $x$ is a function. + \end{proposition} + + +% Dummy abbreviation to test verb abbreviations. +\begin{abbreviation}\label{converges} + $x$ converges to $y$ iff $x = y$. +\end{abbreviation} + +\begin{proposition}\label{dummy_abbr_test_verb} + If $x$ converges to $y$, then $x = y$. + \end{proposition} + + +% Test of built-in \notin abbreviation. The two variants should produce the same TPTP atoms. +\begin{proposition}\label{abbr_test_notin} + If $x\notin y$, then $x\not\in y$. +\end{proposition} + + +% Test of built-in "element of" abbreviation. The two variants should produce the same TPTP atoms. +\begin{proposition}\label{abbr_test_elementof_is_in} + If $x$ is an element of $y$, then $x\in y$. +\end{proposition} + + +% Test of built-in "equals" abbreviation. The two variants should produce the same TPTP atoms. +\begin{proposition}\label{abbr_test_equals_is_eq} + If $x$ equals $y$, then $x = y$. +\end{proposition} diff --git a/test/examples/byRef.tex b/test/examples/byRef.tex new file mode 100644 index 0000000..c896c86 --- /dev/null +++ b/test/examples/byRef.tex @@ -0,0 +1,25 @@ +\begin{proposition}\label{first_proposition} + $a = a$. +\end{proposition} + +\begin{proposition}\label{second_proposition} + $b = b$. +\end{proposition} + +\begin{proposition}\label{third_proposition} + $c = c$. +\end{proposition} +\begin{proof} + Follows by \ref{first_proposition}. % Should filter out second_proposition +\end{proof} + +\begin{proposition}\label{fourth_proposition} + $e = e$. +\end{proposition} +\begin{proof} + For all $d$ we have $d = d$ by \ref{first_proposition}. +\end{proof} + +\begin{proposition}\label{fifth_proposition} + $f = f$. +\end{proposition} diff --git a/test/examples/calc.tex b/test/examples/calc.tex new file mode 100644 index 0000000..b0a0386 --- /dev/null +++ b/test/examples/calc.tex @@ -0,0 +1,33 @@ +\begin{proposition}\label{trivial} + $x = x$. +\end{proposition} + +\begin{proposition}\label{irrelevant} + $z = z$. +\end{proposition} + +\begin{proposition}\label{alsotrivial} + $y = y$. +\end{proposition} +\begin{proof} + \begin{align*} + y + &= y + \\ + &= y + \explanation{by \cref{trivial}} + \end{align*} +\end{proof} + +\begin{proposition}\label{trivial_biconditionals} + $y = y$. +\end{proposition} +\begin{proof} + \begin{align*} + y = y + &\iff \top + \\ + &\iff y = y + \explanation{by \cref{trivial}} + \end{align*} +\end{proof} diff --git a/test/examples/coord.tex b/test/examples/coord.tex new file mode 100644 index 0000000..6dc8d5a --- /dev/null +++ b/test/examples/coord.tex @@ -0,0 +1,37 @@ +\begin{definition}\label{bar} + $x$ is a bar iff $x = x$. +\end{definition} + +\begin{definition}\label{foo} + $x$ is foo iff $x = x$. +\end{definition} + +\begin{definition}\label{baz} + $x$ is baz iff $x = x$. +\end{definition} + +\begin{proposition}\label{nouns} + Let $x, y$ be bars. + Then $x = x$. +\end{proposition} + +\begin{proposition}\label{adj_nouns} + Let $x, y$ be foo bars. + Then $x = x$. +\end{proposition} + + +\begin{proposition}\label{nouns_suchthat} + Let $x, y$ be bars such that $x$ is foo and $y$ is baz. + Then $x = x$. +\end{proposition} + + +\begin{proposition}\label{noun_verb} + $x = y$ iff $x$ is a bar equal to $y$. +\end{proposition} + + +\begin{proposition}\label{adjs} + $x$ is foo and baz. +\end{proposition} diff --git a/test/examples/finite-set-terms.tex b/test/examples/finite-set-terms.tex new file mode 100644 index 0000000..76cc4d9 --- /dev/null +++ b/test/examples/finite-set-terms.tex @@ -0,0 +1,11 @@ +\begin{axiom}\label{cons} + $x\in \cons{y}{X}$ iff $x = y$ or $x\in X$. +\end{axiom} + +\begin{definition}\label{unit} + $\unit = \{\emptyset\}$. +\end{definition} + +\begin{proposition}\label{emptyset_in_unit} + $\emptyset\in\unit$. +\end{proposition} diff --git a/test/examples/formula.tex b/test/examples/formula.tex new file mode 100644 index 0000000..c029402 --- /dev/null +++ b/test/examples/formula.tex @@ -0,0 +1,7 @@ +\begin{proposition}\label{formula_test_forall} + $\forall x, y. x = x\land y = y$. +\end{proposition} + +\begin{proposition}\label{formula_test_exists} + $\exists x, y. x = y$. +\end{proposition} diff --git a/test/examples/geometry.tex b/test/examples/geometry.tex new file mode 100644 index 0000000..fd8df42 --- /dev/null +++ b/test/examples/geometry.tex @@ -0,0 +1,132 @@ +\begin{definition}\label{collinear} + $a$ is collinear with $b$ and $c$ iff $\Betw{a}{b}{c}$ or $\Betw{b}{c}{a}$ or $\Betw{c}{a}{b}$. +\end{definition} + +\begin{axiom}[Reflexivity of congruence]\label{cong_refl_swap} % SST A1 + Let $a, b$ be points. + Then $\Cong{a}{b}{b}{a}$. +\end{axiom} + +\begin{axiom}[Pseudotransitivity of congruence]\label{cong_pseudotransitive} % SST A2 + Let $a, b, c, d$ be points. + If $\Cong{c}{d}{a}{b}$ and $\Cong{c}{d}{e}{f}$ then $\Cong{a}{b}{e}{f}$. +\end{axiom} + +\begin{axiom}[Identity of congruence]\label{cong_id} % SST A3 + Let $a, b, c$ be points. + If $\Cong{a}{b}{c}{c}$ then $a = b$. +\end{axiom} + + +\begin{axiom}[Segment construction]\label{segment_construction} % SST A4 + There exists a point $c$ such that $\Betw{a}{b}{c}$ and $\Cong{b}{c}{d}{e}$. +\end{axiom} + + +\begin{definition}\label{ofs} + Let $x,y,z,r,u,v,w,p$ be points. + $\OFS{x}{y}{z}{r}{u}{v}{w}{p}$ if and only if + $\Betw{x}{y}{z} + \land \Betw{u}{v}{w}$ + and + $\Cong{x}{y}{u}{v} + \land \Cong{y}{z}{v}{w} + \land \Cong{x}{r}{u}{p} + \land \Cong{y}{r}{v}{p}$. +\end{definition} + + +\begin{axiom}[Five segment axiom]\label{five_segment} % SST A5 + Let $a,b,c,d,a',b',c',d'$ be points. + If $\OFS{a}{b}{c}{d}{a'}{b'}{c'}{d'}$ and + $a \neq b$ then $\Cong{c}{d}{c'}{d'}$. +\end{axiom} + + +\begin{axiom}[Identity of betweenness]\label{betw_id} + Let $a,b$ be points. + If $\Betw{a}{b}{a}$ then $a = b$. +\end{axiom} + + +\begin{axiom}[Inner Pasch]\label{innerpasch} % SST A7 + Let $x,y,z,u,v,w$ be points. + If $\Betw{x}{u}{z}$ and $\Betw{y}{v}{z}$ then there exists a point $w$ + such that $\Betw{u}{w}{y}$ and $\Betw{v}{w}{x}$. +\end{axiom} + + +% \begin{axiom}[Lower dimension] % SST A8 +% %There exist points $a, b, c$ such that +% There exists $a, b, c$ such that $a,b,c$ are points and +% $a$ is not collinear with $b$ and $c$. +% \end{axiom} + + +\begin{axiom}[Upper dimension]\label{upperdim} % SST A9 + Let $x,y,z,u,v$ be points. + If $\Cong{x}{u}{x}{v}$ and $\Cong{y}{u}{y}{v}$ + and $\Cong{z}{u}{z}{v}$ and $u \neq v$ + then $x$ is collinear with $y$ and $z$. +\end{axiom} + + +% \begin{axiom}[Euclid] +% Assume $x \neq r$. +% If $\Betw{x}{r}{v}$ and $\Betw{y}{r}{z}$ +% then there exist points $s,t$ such that +% $\Betw{x}{y}{s}$ and $\Betw{x}{z}{t}$ and $\Betw{s}{v}{t}$. +% \end{axiom} + + +\begin{lemma}[Reflexivity of congruence]\label{cong_refl} % Satz 2.1 + Let $a, b$ be points. + Then $\Cong{a}{b}{a}{b}$. +\end{lemma} + + +\begin{lemma}[Symmetry of congruence]\label{cong_sym} % Satz 2.2 + Let $a, b, c, d$ be points. + Suppose $\Cong{a}{b}{c}{d}$. + Then $\Cong{c}{d}{a}{b}$. +\end{lemma} + + +\begin{lemma}[Transitivity of congruence]\label{cong_transitive} % Satz 2.3 + Let $a, b, c, d, e, f$ be points. + If $\Cong{a}{b}{c}{d}$ and $\Cong{c}{d}{e}{f}$ + then $\Cong{a}{b}{e}{f}$. +\end{lemma} + + +\begin{lemma}\label{cong_shuffle_left} % Satz 2.4 + Let $a, b, c, d$ be points. + If $\Cong{a}{b}{c}{d}$ + then $\Cong{b}{a}{c}{d}$. +\end{lemma} + + +\begin{lemma}\label{cong_shuffle_right} % Satz 2.5 + Let $a, b, c, d$ be points. + If $\Cong{a}{b}{c}{d}$ + then $\Cong{b}{a}{d}{c}$. +\end{lemma} + + +\begin{lemma}[Zero segments are congruent]\label{cong_zero} % Satz 2.8 + Let $a,b$ be points. + Then $\Cong{a}{a}{b}{b}$. +\end{lemma} + +% Somewhat slow for now. +%\begin{lemma}[Concatenation of segments]\label{segment_concat} % Satz 2.11 +% Assume $\Betw{x}{y}{z}$ and $\Betw{r}{v}{w}$. +% Assume $\Cong{x}{y}{r}{v}$ and $\Cong{y}{z}{v}{w}$. +% Then $\Cong{x}{z}{r}{w}$. +%\end{lemma} +%\begin{proof} +% % We have +% $\OFS{x}{y}{z}{x}{r}{v}{w}{r}$. % By previous results and assumption. +% If $x = y$ then $r = v$. % Axiom A3 gives this implication. +% If $x \neq y$ then $\Cong{x}{z}{r}{w}$. % Axiom A5 completes the proof. +%\end{proof} diff --git a/test/examples/indefinite-terms.tex b/test/examples/indefinite-terms.tex new file mode 100644 index 0000000..25d4fcd --- /dev/null +++ b/test/examples/indefinite-terms.tex @@ -0,0 +1,7 @@ +\begin{theorem}\label{indefinite_test_forall} + Every set is a set. +\end{theorem} + +\begin{theorem}\label{indefinite_test_exists} + Some set is a set. +\end{theorem} diff --git a/test/examples/inductive.tex b/test/examples/inductive.tex new file mode 100644 index 0000000..2f83f35 --- /dev/null +++ b/test/examples/inductive.tex @@ -0,0 +1,74 @@ +% Dummy setup to test the syntax and the generated proof tasks + +\begin{definition}\label{subseteq} + $A\subseteq B$ iff $A = B$. +\end{definition} + +\begin{definition}\label{pow} + $\pow{A} = \emptyset$. +\end{definition} + +\begin{definition}\label{cons} + $\cons{a}{B} = \emptyset$. +\end{definition} + +\begin{definition}\label{times} + $A\times B = \emptyset$. +\end{definition} + +\begin{definition}\label{fld} + $\fld{R} = \emptyset$. +\end{definition} + +\begin{definition}\label{preimg} + $\preimg{R}{A} = \emptyset$. +\end{definition} + +\begin{axiom}\label{lmao} + $x\in\emptyset$. +\end{axiom} + +\begin{inductive}\label{fin} + Define $\fin{A}\subseteq\pow{A}$ inductively as follows. + \begin{enumerate} + \item $\emptyset \in\fin{A}$. + \item If $a\in A$ and $B\in\fin{A}$, then $\cons{a}{B}\in\fin{A}$. + \end{enumerate} +\end{inductive} + +\begin{lemma}\label{fin_mono} + Let $A, B$ be sets. + Suppose $A\subseteq B$. + Then $\fin{A}\subseteq\fin{B}$. +\end{lemma} + +\begin{inductive}\label{tracl} + Define $\tracl{R}\subseteq\fld{R}\times\fld{R}$ inductively as follows. + \begin{enumerate} + \item If $w\in R$, then $w\in\tracl{R}$. + \item If $(a, b)\in\tracl{R}$ and $(b,c)\in R$, then $(a,c)\in\tracl{R}$. + \end{enumerate} +\end{inductive} + +\begin{inductive}\label{quasirefltracl} + Define $\qrefltracl{R}\subseteq\fld{R}\times\fld{R}$ inductively as follows. + \begin{enumerate} + \item If $a\in\fld{R}$, then $(a,a)\in\qrefltracl{R}$. + \item If $(a, b)\in\qrefltracl{R}$ and $(b,c)\in R$, then $(a,c)\in\qrefltracl{R}$. + \end{enumerate} +\end{inductive} + +\begin{inductive}\label{refltracl} + Define $\refltracl{A}{R}\subseteq A\times A$ inductively as follows. + \begin{enumerate} + \item If $a\in A$, then $(a,a)\in\refltracl{A}{R}$. + \item If $(a, b)\in\refltracl{A}{R}$ and $(b,c)\in R$, then $(a,c)\in\refltracl{A}{R}$. + \end{enumerate} +\end{inductive} + +\begin{inductive}\label{acc} + Define $\acc{R}\subseteq \fld{R}$ inductively as follows. + \begin{enumerate} + \item If $a\in\fld{R}$ and $\preimg{R}{\{a\}}\in\pow{\acc{R}}$, then $a\in\acc{R}$. + \end{enumerate} +\end{inductive} diff --git a/test/examples/no-reflexive-set.tex b/test/examples/no-reflexive-set.tex new file mode 100644 index 0000000..78bd07c --- /dev/null +++ b/test/examples/no-reflexive-set.tex @@ -0,0 +1,11 @@ +\begin{proposition}\label{in_irrefl} + For all sets $A$ we have $A\not\in A$. +\end{proposition} +\begin{proof}[Proof by \in-induction] + %Let $B$ be a set. + %Suppose $b\notin b$ for all $b\in B$. + %Suppose $B\in B$. + %But then + % $B\notin B$. + Straightforward. +\end{proof} diff --git a/test/examples/proofassume.tex b/test/examples/proofassume.tex new file mode 100644 index 0000000..ab37198 --- /dev/null +++ b/test/examples/proofassume.tex @@ -0,0 +1,16 @@ +\begin{proposition}\label{assumetest} + If $x\in y$, then $x\in y$. +\end{proposition} +\begin{proof} + Assume $x\in y$. + Then $x\in y$. +\end{proof} + +\begin{proposition}\label{assumetesttwo} + If $x\in y$ and $a\in b$, then $x\in y$. +\end{proposition} +\begin{proof} + Assume $a\in b$. + Assume $x\in y$. + Then $x\in y$. +\end{proof} diff --git a/test/examples/proofdefinefunction.tex b/test/examples/proofdefinefunction.tex new file mode 100644 index 0000000..ac17d0b --- /dev/null +++ b/test/examples/proofdefinefunction.tex @@ -0,0 +1,27 @@ +% The builtin "-(-)" notation desugars to "\apply{-}{-}". +% This is just a dummy definition. +\begin{definition}\label{apply} + $\apply{f}{x} = x$. +\end{definition} + +% Dummy definition for the domain +\begin{definition}\label{dom} + $\dom{f} = f$. +\end{definition} + +% Dummy definition for right-uniqueness +\begin{definition}\label{rightunique} + $f$ is right-unique iff $f=f$. +\end{definition} + +% Dummy definition for relations +\begin{definition}\label{relation} + $f$ is a relation iff $f=f$. +\end{definition} + +\begin{proposition}\label{definefunctiontest} + If $x\in y$, then $x\in y$. +\end{proposition} +\begin{proof} + Let $f(z) = z$ for $z\in x$. +\end{proof} diff --git a/test/examples/prooffix.tex b/test/examples/prooffix.tex new file mode 100644 index 0000000..7201eee --- /dev/null +++ b/test/examples/prooffix.tex @@ -0,0 +1,16 @@ +\begin{proposition}\label{assumetest} + For all $x$ we have $x = x$. +\end{proposition} +\begin{proof} + Fix $x$. + Then $x = x$. +\end{proof} + +%\begin{proposition}\label{assumetesttwo} +% For all $x,y,z$ we have $z = z$. +%\end{proposition} +%\begin{proof} +% Fix $y$. +% Fix $x,z$. +% Then $z = z$. +%\end{proof} diff --git a/test/examples/relation-notation.tex b/test/examples/relation-notation.tex new file mode 100644 index 0000000..7cc94fc --- /dev/null +++ b/test/examples/relation-notation.tex @@ -0,0 +1,3 @@ +\begin{proposition}\label{mathrel_notation_test} + If $x\mathrel{R} y$, then $x\mathrel{R} y$. +\end{proposition} diff --git a/test/examples/replace.tex b/test/examples/replace.tex new file mode 100644 index 0000000..66fae16 --- /dev/null +++ b/test/examples/replace.tex @@ -0,0 +1,27 @@ +\begin{axiom}\label{cons} + $x\in \cons{y}{X}$ iff $x = y$ or $x\in X$. +\end{axiom} + +\begin{definition}\label{times} + $A\times B = \{ (a,b) \mid a\in A, b\in B\}$. +\end{definition} + +\begin{definition}\label{unit} + $\unit = \{\emptyset\}$. +\end{definition} + +\begin{proposition}\label{pair_emptyset_in_times_unit} + $(\emptyset,\emptyset)\in \unit\times\unit$. +\end{proposition} + + +% Indirect definition of the Zermelo successor operation to test primitive replacement. +\begin{definition}\label{suc} + $\suc{a} = \{ y \mid \exists x\in a. y = \{x\} \}$. +\end{definition} + + +% Dummy proposition to test unrolling of functional replacement in equations. +\begin{proposition}\label{times_replacement_test} + $A\times B = \{ (a,b) \mid a\in A, b\in B\}$. +\end{proposition} diff --git a/test/examples/russell.tex b/test/examples/russell.tex new file mode 100644 index 0000000..4c2a8f2 --- /dev/null +++ b/test/examples/russell.tex @@ -0,0 +1,16 @@ +\begin{definition}\label{universal_set} + A set $V$ is universal iff + %every set is an element of $V$. + for all sets $x$ we have $x\in V$. +\end{definition} + +\begin{theorem}\label{no_universal_set} + There exists no universal set. +\end{theorem} +\begin{proof} + Suppose not. + Take a universal set $V$. + Let $R = \{ x\in V \mid x\not\in x \}$. + Then $R\in R$ iff $R\not\in R$. + Contradiction. +\end{proof} diff --git a/test/examples/separation.tex b/test/examples/separation.tex new file mode 100644 index 0000000..0bea2a2 --- /dev/null +++ b/test/examples/separation.tex @@ -0,0 +1,3 @@ +\begin{proposition}\label{sep_test} + $X = \{ x\in X\mid x = x\}$. +\end{proposition} diff --git a/test/examples/union.tex b/test/examples/union.tex new file mode 100644 index 0000000..b5c5783 --- /dev/null +++ b/test/examples/union.tex @@ -0,0 +1,21 @@ +\begin{axiom}[Extensionality]\label{ext} + Suppose for all $a$ we have $a\in A$ iff $a\in B$. + Then $A = B$. +\end{axiom} + +\begin{axiom}\label{union_defn} + Let $A, B$ be sets. + $a\in A\union B$ iff $a\in A$ or $a\in B$. +\end{axiom} + +\begin{proposition}\label{union_comm} + $A\union B = B\union A$. +\end{proposition} + +\begin{proposition}\label{union_assoc} + $(A\union B)\union C = A\union (B\union C)$. +\end{proposition} +\begin{proof} + For all $a$ we have if $a\in (A\union B)\union C$, then $a\in A\union (B\union C)$. + For all $a$ we have if $a\in A\union (B\union C)$, then $a\in (A\union B)\union C$. +\end{proof} |