diff options
Diffstat (limited to 'test')
68 files changed, 1545 insertions, 245 deletions
diff --git a/test/examples/coord.tex b/test/examples/coord.tex index 9987506..32d3fa1 100644 --- a/test/examples/coord.tex +++ b/test/examples/coord.tex @@ -30,11 +30,17 @@ \begin{proposition}\label{noun_verb} $x = y$ iff $x$ is a bar equal to $y$. \end{proposition} +\begin{proof} + Follows by \cref{bar}. +\end{proof} \begin{proposition}\label{adjs} $x$ is foo and baz. \end{proposition} +\begin{proof} + Follows by \cref{foo,baz}. +\end{proof} \begin{proposition}\label{are_nouns} Let $x, y$ be foo bars. diff --git a/test/examples/datatype.tex b/test/examples/datatype.tex index 3ea9161..09d014d 100644 --- a/test/examples/datatype.tex +++ b/test/examples/datatype.tex @@ -3,26 +3,43 @@ Define $\propform$ inductively as follows. \begin{enumerate} \item $\propbot \in \propform$. - \item $\propvar{n} \in \propform$ for $n \in \{\emptyset\}$. + \item $\propvar{n} \in \propform$ for + $n \in \{\emptyset\}$. \item $(p \propto q) \in \propform$ for $p \in \propform$ and $q \in \propform$. \end{enumerate} \end{datatype} \begin{proposition}\label{propform_bot_test} $\propbot \in \propform$. \end{proposition} +\begin{proof} + Follows by \cref{propform_propbot_intro}. +\end{proof} \begin{proposition}\label{propform_var_test} - If $\emptyset \in \{\emptyset\}$, then $\propvar{\emptyset} \in \propform$. + If $\emptyset \in \{\emptyset\}$, then + $\propvar{\emptyset} \in \propform$. \end{proposition} +\begin{proof} + Follows by \cref{propform_propvar_intro}. +\end{proof} \begin{proposition}\label{propform_imp_test} $(\propbot \propto \propbot) \in \propform$. \end{proposition} +\begin{proof} + Follows by \cref{propform_propbot_intro,propform_propto_intro}. +\end{proof} \begin{proposition}\label{propform_distinct_test} $\propbot \neq (\propbot \propto \propbot)$. \end{proposition} +\begin{proof} + Follows by \cref{propform_propbot_propto_distinct}. +\end{proof} \begin{proposition}\label{propform_injective_test} If $\propvar{x} = \propvar{y}$, then $x = y$. \end{proposition} +\begin{proof} + Follows by \cref{propform_propvar_injective}. +\end{proof} diff --git a/test/examples/finite-set-terms.tex b/test/examples/finite-set-terms.tex index 76cc4d9..4aa7ba6 100644 --- a/test/examples/finite-set-terms.tex +++ b/test/examples/finite-set-terms.tex @@ -1,3 +1,7 @@ +\begin{signature}\label{example_cons} + $\cons{y}{X}$ is a set. +\end{signature} + \begin{axiom}\label{cons} $x\in \cons{y}{X}$ iff $x = y$ or $x\in X$. \end{axiom} diff --git a/test/examples/proofdefinefunction.tex b/test/examples/proofdefinefunction.tex index ac17d0b..0367a0d 100644 --- a/test/examples/proofdefinefunction.tex +++ b/test/examples/proofdefinefunction.tex @@ -1,3 +1,7 @@ +\begin{signature}\label{example_pair} + $(x,y)$ is a set. +\end{signature} + % The builtin "-(-)" notation desugars to "\apply{-}{-}". % This is just a dummy definition. \begin{definition}\label{apply} diff --git a/test/examples/relation-notation.tex b/test/examples/relation-notation.tex index 7cc94fc..0eff5d0 100644 --- a/test/examples/relation-notation.tex +++ b/test/examples/relation-notation.tex @@ -1,3 +1,7 @@ +\begin{signature}\label{example_pair} + $(x,y)$ is a set. +\end{signature} + \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 index 66fae16..8737af3 100644 --- a/test/examples/replace.tex +++ b/test/examples/replace.tex @@ -1,3 +1,11 @@ +\begin{signature}\label{example_cons} + $\cons{y}{X}$ is a set. +\end{signature} + +\begin{signature}\label{example_pair} + $(x,y)$ is a set. +\end{signature} + \begin{axiom}\label{cons} $x\in \cons{y}{X}$ iff $x = y$ or $x\in X$. \end{axiom} @@ -25,3 +33,6 @@ \begin{proposition}\label{times_replacement_test} $A\times B = \{ (a,b) \mid a\in A, b\in B\}$. \end{proposition} +\begin{proof} + Follows by \cref{times}. +\end{proof} diff --git a/test/examples/russell.tex b/test/examples/russell.tex index 4c2a8f2..dacd723 100644 --- a/test/examples/russell.tex +++ b/test/examples/russell.tex @@ -11,6 +11,6 @@ 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$. + $R\in V$ by \cref{universal_set}. Contradiction. \end{proof} diff --git a/test/examples/union.tex b/test/examples/union.tex index b5c5783..cae5935 100644 --- a/test/examples/union.tex +++ b/test/examples/union.tex @@ -1,3 +1,7 @@ +\begin{signature}\label{example_union} + $A\union B$ is a set. +\end{signature} + \begin{axiom}[Extensionality]\label{ext} Suppose for all $a$ we have $a\in A$ iff $a\in B$. Then $A = B$. diff --git a/test/golden/coord/parsing.golden b/test/golden/coord/parsing.golden index 2c1ca80..f148da6 100644 --- a/test/golden/coord/parsing.golden +++ b/test/golden/coord/parsing.golden @@ -485,12 +485,38 @@ } ) ) -, BlockClaim Proposition +, BlockProof + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 33 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 34 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "bar" :| [] ) + ) + ) ( Location { locFile = "test/examples/coord.tex" , locLine = 35 , locColumn = 1 } + ) +, BlockClaim Proposition + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 38 + , locColumn = 1 + } ) Nothing ( Marker "adjs" ) ( Claim [] @@ -503,7 +529,7 @@ ( Adj ( Location { locFile = "test/examples/coord.tex" - , locLine = 36 + , locLine = 39 , locColumn = 12 } ) @@ -516,7 +542,7 @@ [ Adj ( Location { locFile = "test/examples/coord.tex" - , locLine = 36 + , locLine = 39 , locColumn = 20 } ) @@ -531,10 +557,38 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 41 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 42 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "foo" :| + [ Marker "baz" ] + ) + ) + ) + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 43 + , locColumn = 1 + } + ) , BlockClaim Proposition ( Location { locFile = "test/examples/coord.tex" - , locLine = 39 + , locLine = 45 , locColumn = 1 } ) Nothing @@ -548,7 +602,7 @@ [ AdjL ( Location { locFile = "test/examples/coord.tex" - , locLine = 40 + , locLine = 46 , locColumn = 19 } ) @@ -563,7 +617,7 @@ ( Noun ( Location { locFile = "test/examples/coord.tex" - , locLine = 40 + , locLine = 46 , locColumn = 23 } ) @@ -594,7 +648,7 @@ [ AdjL ( Location { locFile = "test/examples/coord.tex" - , locLine = 41 + , locLine = 47 , locColumn = 26 } ) @@ -609,7 +663,7 @@ ( Noun ( Location { locFile = "test/examples/coord.tex" - , locLine = 41 + , locLine = 47 , locColumn = 30 } ) diff --git a/test/golden/coord/tokenizing.golden b/test/golden/coord/tokenizing.golden index 56dac36..252d9ab 100644 --- a/test/golden/coord/tokenizing.golden +++ b/test/golden/coord/tokenizing.golden @@ -151,6 +151,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "bar" :| [] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "adjs" , BeginEnv "math" @@ -164,6 +173,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "foo" :| [ "baz" ] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "are_nouns" , Word "let" diff --git a/test/golden/datatype/parsing.golden b/test/golden/datatype/parsing.golden index d07b92c..11dd2bc 100644 --- a/test/golden/datatype/parsing.golden +++ b/test/golden/datatype/parsing.golden @@ -88,15 +88,15 @@ , ExprFiniteSet ( Location { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 + , locLine = 7 + , locColumn = 20 } ) ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 + , locLine = 7 + , locColumn = 22 } ) ( MixfixItem @@ -113,7 +113,7 @@ { datatypeClauseConstructorExpr = ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 7 + , locLine = 8 , locColumn = 17 } ) @@ -133,7 +133,7 @@ , datatypeClauseTargetExpr = ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 7 + , locLine = 8 , locColumn = 34 } ) @@ -149,7 +149,7 @@ , ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 7 + , locLine = 8 , locColumn = 56 } ) @@ -165,7 +165,7 @@ , ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 7 + , locLine = 8 , locColumn = 78 } ) @@ -184,7 +184,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/datatype.tex" - , locLine = 10 + , locLine = 11 , locColumn = 1 } ) Nothing @@ -196,7 +196,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 11 + , locLine = 12 , locColumn = 6 } ) @@ -210,7 +210,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 11 + , locLine = 12 , locColumn = 15 } ) @@ -223,7 +223,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 11 + , locLine = 12 , locColumn = 19 } ) @@ -238,12 +238,38 @@ } ) ) -, BlockClaim Proposition +, BlockProof ( Location { locFile = "test/examples/datatype.tex" , locLine = 14 , locColumn = 1 } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 15 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "propform_propbot_intro" :| [] ) + ) + ) + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 16 + , locColumn = 1 + } + ) +, BlockClaim Proposition + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 18 + , locColumn = 1 + } ) Nothing ( Marker "propform_var_test" ) ( Claim [] @@ -252,7 +278,7 @@ , mloc = Just ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 + , locLine = 19 , locColumn = 5 } ) @@ -262,7 +288,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 + , locLine = 19 , locColumn = 9 } ) @@ -276,7 +302,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 + , locLine = 19 , locColumn = 19 } ) @@ -289,14 +315,14 @@ ( ExprFiniteSet ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 + , locLine = 19 , locColumn = 23 } ) ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 + , locLine = 19 , locColumn = 25 } ) @@ -316,8 +342,8 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 45 + , locLine = 20 + , locColumn = 10 } ) ( MixfixItem @@ -332,8 +358,8 @@ [ ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 54 + , locLine = 20 + , locColumn = 19 } ) ( MixfixItem @@ -347,8 +373,8 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 65 + , locLine = 20 + , locColumn = 30 } ) ( RelationSymbol @@ -360,8 +386,8 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 69 + , locLine = 20 + , locColumn = 34 } ) ( MixfixItem @@ -376,10 +402,36 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 22 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 23 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "propform_propvar_intro" :| [] ) + ) + ) + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 24 + , locColumn = 1 + } + ) , BlockClaim Proposition ( Location { locFile = "test/examples/datatype.tex" - , locLine = 18 + , locLine = 26 , locColumn = 1 } ) Nothing @@ -391,7 +443,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 19 + , locLine = 27 , locColumn = 7 } ) @@ -406,7 +458,7 @@ [ ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 19 + , locLine = 27 , locColumn = 7 } ) @@ -419,7 +471,7 @@ , ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 19 + , locLine = 27 , locColumn = 24 } ) @@ -434,7 +486,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 19 + , locLine = 27 , locColumn = 34 } ) @@ -447,7 +499,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 19 + , locLine = 27 , locColumn = 38 } ) @@ -462,10 +514,38 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 29 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 30 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "propform_propbot_intro" :| + [ Marker "propform_propto_intro" ] + ) + ) + ) + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 31 + , locColumn = 1 + } + ) , BlockClaim Proposition ( Location { locFile = "test/examples/datatype.tex" - , locLine = 22 + , locLine = 33 , locColumn = 1 } ) Nothing @@ -477,7 +557,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 23 + , locLine = 34 , locColumn = 6 } ) @@ -491,7 +571,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 23 + , locLine = 34 , locColumn = 15 } ) @@ -504,7 +584,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 23 + , locLine = 34 , locColumn = 21 } ) @@ -519,7 +599,7 @@ [ ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 23 + , locLine = 34 , locColumn = 21 } ) @@ -532,7 +612,7 @@ , ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 23 + , locLine = 34 , locColumn = 38 } ) @@ -548,10 +628,36 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 36 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 37 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "propform_propbot_propto_distinct" :| [] ) + ) + ) + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 38 + , locColumn = 1 + } + ) , BlockClaim Proposition ( Location { locFile = "test/examples/datatype.tex" - , locLine = 26 + , locLine = 40 , locColumn = 1 } ) Nothing @@ -562,7 +668,7 @@ , mloc = Just ( Location { locFile = "test/examples/datatype.tex" - , locLine = 27 + , locLine = 41 , locColumn = 5 } ) @@ -572,7 +678,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 27 + , locLine = 41 , locColumn = 9 } ) @@ -592,7 +698,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 27 + , locLine = 41 , locColumn = 21 } ) @@ -605,7 +711,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 27 + , locLine = 41 , locColumn = 23 } ) @@ -633,7 +739,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 27 + , locLine = 41 , locColumn = 45 } ) @@ -651,4 +757,30 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 43 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 44 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "propform_propvar_injective" :| [] ) + ) + ) + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 45 + , locColumn = 1 + } + ) ]
\ No newline at end of file diff --git a/test/golden/datatype/tokenizing.golden b/test/golden/datatype/tokenizing.golden index 1827a62..90f8274 100644 --- a/test/golden/datatype/tokenizing.golden +++ b/test/golden/datatype/tokenizing.golden @@ -73,6 +73,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propbot_intro" :| [] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_var_test" , Word "if" @@ -97,6 +106,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propvar_intro" :| [] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_imp_test" , BeginEnv "math" @@ -112,6 +130,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propbot_intro" :| [ "propform_propto_intro" ] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_distinct_test" , BeginEnv "math" @@ -127,6 +154,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propbot_propto_distinct" :| [] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_injective_test" , Word "if" @@ -151,4 +187,13 @@ , Symbol "." , EndEnv "proposition" ] +, + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propvar_injective" :| [] ) + , Symbol "." + , EndEnv "proof" + ] ]
\ No newline at end of file diff --git a/test/golden/finite-set-terms/parsing.golden b/test/golden/finite-set-terms/parsing.golden index 6d031b4..d351ceb 100644 --- a/test/golden/finite-set-terms/parsing.golden +++ b/test/golden/finite-set-terms/parsing.golden @@ -1,10 +1,58 @@ -[ BlockAxiom +[ BlockSig ( Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 1 , locColumn = 1 } ) Nothing + ( Marker "example_cons" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( TokenCons + ( Command "cons" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "cons" ) NonAssoc + ) + [ NamedVar "y" + , NamedVar "X" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/finite-set-terms.tex" + , locLine = 2 + , locColumn = 24 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockAxiom + ( Location + { locFile = "test/examples/finite-set-terms.tex" + , locLine = 5 + , locColumn = 1 + } + ) Nothing ( Marker "cons" ) ( Axiom [] ( StmtConnected @@ -19,7 +67,7 @@ ( Relation ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 2 + , locLine = 6 , locColumn = 7 } ) @@ -32,7 +80,7 @@ ( ExprOp ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 2 + , locLine = 6 , locColumn = 11 } ) @@ -71,7 +119,7 @@ ( Relation ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 2 + , locLine = 6 , locColumn = 31 } ) @@ -95,7 +143,7 @@ ( Relation ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 2 + , locLine = 6 , locColumn = 41 } ) @@ -117,7 +165,7 @@ , BlockDefn ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 5 + , locLine = 9 , locColumn = 1 } ) Nothing @@ -134,14 +182,14 @@ ( ExprFiniteSet ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 6 + , locLine = 10 , locColumn = 14 } ) ( ExprOp ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 6 + , locLine = 10 , locColumn = 16 } ) @@ -157,7 +205,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 9 + , locLine = 13 , locColumn = 1 } ) Nothing @@ -169,7 +217,7 @@ ( ExprOp ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 10 + , locLine = 14 , locColumn = 6 } ) @@ -183,7 +231,7 @@ ( Relation ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 10 + , locLine = 14 , locColumn = 15 } ) @@ -196,7 +244,7 @@ ( ExprOp ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 10 + , locLine = 14 , locColumn = 18 } ) diff --git a/test/golden/finite-set-terms/scanning.golden b/test/golden/finite-set-terms/scanning.golden index 5cef8dd..66d57f7 100644 --- a/test/golden/finite-set-terms/scanning.golden +++ b/test/golden/finite-set-terms/scanning.golden @@ -1,5 +1,19 @@ [ ScanFunctionSymbol ( TokenCons + ( Command "cons" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "example_cons" ) +, ScanFunctionSymbol + ( TokenCons ( Command "unit" ) End ) ( Marker "unit" ) diff --git a/test/golden/finite-set-terms/tokenizing.golden b/test/golden/finite-set-terms/tokenizing.golden index 200e330..ebe2484 100644 --- a/test/golden/finite-set-terms/tokenizing.golden +++ b/test/golden/finite-set-terms/tokenizing.golden @@ -1,4 +1,22 @@ [ + [ BeginEnv "signature" + , Label "example_cons" + , BeginEnv "math" + , Command "cons" + , InvisibleBraceL + , Variable "y" + , InvisibleBraceR + , InvisibleBraceL + , Variable "X" + , InvisibleBraceR + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, [ BeginEnv "axiom" , Label "cons" , BeginEnv "math" diff --git a/test/golden/proofdefinefunction/parsing.golden b/test/golden/proofdefinefunction/parsing.golden index 1089d8f..60110a5 100644 --- a/test/golden/proofdefinefunction/parsing.golden +++ b/test/golden/proofdefinefunction/parsing.golden @@ -1,7 +1,55 @@ -[ BlockDefn +[ BlockSig ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 3 + , locLine = 1 + , locColumn = 1 + } + ) Nothing + ( Marker "example_pair" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( TokenCons + ( Command "pair" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "pair" ) NonAssoc + ) + [ NamedVar "x" + , NamedVar "y" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/proofdefinefunction.tex" + , locLine = 2 + , locColumn = 18 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockDefn + ( Location + { locFile = "test/examples/proofdefinefunction.tex" + , locLine = 7 , locColumn = 1 } ) Nothing @@ -34,7 +82,7 @@ , BlockDefn ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 8 + , locLine = 12 , locColumn = 1 } ) Nothing @@ -59,7 +107,7 @@ , BlockDefn ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 13 + , locLine = 17 , locColumn = 1 } ) Nothing @@ -70,7 +118,7 @@ ( Adj ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 14 + , locLine = 18 , locColumn = 12 } ) @@ -91,7 +139,7 @@ ( Relation ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 14 + , locLine = 18 , locColumn = 31 } ) @@ -111,7 +159,7 @@ , BlockDefn ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 18 + , locLine = 22 , locColumn = 1 } ) Nothing @@ -122,7 +170,7 @@ ( Noun ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 19 + , locLine = 23 , locColumn = 14 } ) @@ -147,7 +195,7 @@ ( Relation ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 19 + , locLine = 23 , locColumn = 29 } ) @@ -167,7 +215,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 22 + , locLine = 26 , locColumn = 1 } ) Nothing @@ -178,7 +226,7 @@ , mloc = Just ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 23 + , locLine = 27 , locColumn = 5 } ) @@ -191,7 +239,7 @@ ( Relation ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 23 + , locLine = 27 , locColumn = 10 } ) @@ -215,7 +263,7 @@ ( Relation ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 23 + , locLine = 27 , locColumn = 25 } ) @@ -236,14 +284,14 @@ , BlockProof ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 25 + , locLine = 29 , locColumn = 1 } ) ( DefineFunction ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 26 + , locLine = 30 , locColumn = 5 } ) @@ -259,7 +307,7 @@ ) ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 27 + , locLine = 31 , locColumn = 1 } ) diff --git a/test/golden/proofdefinefunction/scanning.golden b/test/golden/proofdefinefunction/scanning.golden index fd20405..c49d8f9 100644 --- a/test/golden/proofdefinefunction/scanning.golden +++ b/test/golden/proofdefinefunction/scanning.golden @@ -1,4 +1,14 @@ [ ScanFunctionSymbol + ( TokenCons ParenL + ( HoleCons + ( TokenCons + ( Symbol "," ) + ( HoleCons ( TokenCons ParenR End ) ) + ) + ) + ) + ( Marker "example_pair" ) +, ScanFunctionSymbol ( TokenCons ( Command "apply" ) ( TokenCons InvisibleBraceL diff --git a/test/golden/proofdefinefunction/tokenizing.golden b/test/golden/proofdefinefunction/tokenizing.golden index 63692ab..d479529 100644 --- a/test/golden/proofdefinefunction/tokenizing.golden +++ b/test/golden/proofdefinefunction/tokenizing.golden @@ -1,4 +1,20 @@ [ + [ BeginEnv "signature" + , Label "example_pair" + , BeginEnv "math" + , ParenL + , Variable "x" + , Symbol "," + , Variable "y" + , ParenR + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, [ BeginEnv "definition" , Label "apply" , BeginEnv "math" diff --git a/test/golden/relation-notation/parsing.golden b/test/golden/relation-notation/parsing.golden index 6c489be..65a7b94 100644 --- a/test/golden/relation-notation/parsing.golden +++ b/test/golden/relation-notation/parsing.golden @@ -1,10 +1,58 @@ -[ BlockClaim Proposition +[ BlockSig ( Location { locFile = "test/examples/relation-notation.tex" , locLine = 1 , locColumn = 1 } ) Nothing + ( Marker "example_pair" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( TokenCons + ( Command "pair" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "pair" ) NonAssoc + ) + [ NamedVar "x" + , NamedVar "y" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/relation-notation.tex" + , locLine = 2 + , locColumn = 18 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockClaim Proposition + ( Location + { locFile = "test/examples/relation-notation.tex" + , locLine = 5 + , locColumn = 1 + } + ) Nothing ( Marker "mathrel_notation_test" ) ( Claim [] ( StmtConnected @@ -12,7 +60,7 @@ , mloc = Just ( Location { locFile = "test/examples/relation-notation.tex" - , locLine = 2 + , locLine = 6 , locColumn = 5 } ) @@ -25,7 +73,7 @@ ( RelationExpr ( Location { locFile = "test/examples/relation-notation.tex" - , locLine = 2 + , locLine = 6 , locColumn = 10 } ) @@ -47,7 +95,7 @@ ( RelationExpr ( Location { locFile = "test/examples/relation-notation.tex" - , locLine = 2 + , locLine = 6 , locColumn = 33 } ) diff --git a/test/golden/relation-notation/scanning.golden b/test/golden/relation-notation/scanning.golden index 0637a08..5a6351e 100644 --- a/test/golden/relation-notation/scanning.golden +++ b/test/golden/relation-notation/scanning.golden @@ -1 +1,11 @@ -[]
\ No newline at end of file +[ ScanFunctionSymbol + ( TokenCons ParenL + ( HoleCons + ( TokenCons + ( Symbol "," ) + ( HoleCons ( TokenCons ParenR End ) ) + ) + ) + ) + ( Marker "example_pair" ) +]
\ No newline at end of file diff --git a/test/golden/relation-notation/tokenizing.golden b/test/golden/relation-notation/tokenizing.golden index ae1bda5..84fc828 100644 --- a/test/golden/relation-notation/tokenizing.golden +++ b/test/golden/relation-notation/tokenizing.golden @@ -1,4 +1,20 @@ [ + [ BeginEnv "signature" + , Label "example_pair" + , BeginEnv "math" + , ParenL + , Variable "x" + , Symbol "," + , Variable "y" + , ParenR + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, [ BeginEnv "proposition" , Label "mathrel_notation_test" , Word "if" diff --git a/test/golden/replace/parsing.golden b/test/golden/replace/parsing.golden index 8bdea69..5ea7cac 100644 --- a/test/golden/replace/parsing.golden +++ b/test/golden/replace/parsing.golden @@ -1,10 +1,106 @@ -[ BlockAxiom +[ BlockSig ( Location { locFile = "test/examples/replace.tex" , locLine = 1 , locColumn = 1 } ) Nothing + ( Marker "example_cons" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( TokenCons + ( Command "cons" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "cons" ) NonAssoc + ) + [ NamedVar "y" + , NamedVar "X" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 2 + , locColumn = 24 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockSig + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 5 + , locColumn = 1 + } + ) Nothing + ( Marker "example_pair" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( TokenCons + ( Command "pair" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "pair" ) NonAssoc + ) + [ NamedVar "x" + , NamedVar "y" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 6 + , locColumn = 18 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockAxiom + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 9 + , locColumn = 1 + } + ) Nothing ( Marker "cons" ) ( Axiom [] ( StmtConnected @@ -19,7 +115,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 2 + , locLine = 10 , locColumn = 7 } ) @@ -32,7 +128,7 @@ ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 2 + , locLine = 10 , locColumn = 11 } ) @@ -71,7 +167,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 2 + , locLine = 10 , locColumn = 31 } ) @@ -95,7 +191,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 2 + , locLine = 10 , locColumn = 41 } ) @@ -117,7 +213,7 @@ , BlockDefn ( Location { locFile = "test/examples/replace.tex" - , locLine = 5 + , locLine = 13 , locColumn = 1 } ) Nothing @@ -139,14 +235,14 @@ ( ExprReplace ( Location { locFile = "test/examples/replace.tex" - , locLine = 6 + , locLine = 14 , locColumn = 18 } ) ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 6 + , locLine = 14 , locColumn = 21 } ) @@ -188,7 +284,7 @@ , BlockDefn ( Location { locFile = "test/examples/replace.tex" - , locLine = 9 + , locLine = 17 , locColumn = 1 } ) Nothing @@ -205,14 +301,14 @@ ( ExprFiniteSet ( Location { locFile = "test/examples/replace.tex" - , locLine = 10 + , locLine = 18 , locColumn = 14 } ) ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 10 + , locLine = 18 , locColumn = 16 } ) @@ -228,7 +324,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/replace.tex" - , locLine = 13 + , locLine = 21 , locColumn = 1 } ) Nothing @@ -240,7 +336,7 @@ ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 6 } ) @@ -262,7 +358,7 @@ [ ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 7 } ) @@ -275,7 +371,7 @@ , ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 17 } ) @@ -290,7 +386,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 27 } ) @@ -303,7 +399,7 @@ ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 31 } ) @@ -318,7 +414,7 @@ [ ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 31 } ) @@ -331,7 +427,7 @@ , ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 42 } ) @@ -350,7 +446,7 @@ , BlockDefn ( Location { locFile = "test/examples/replace.tex" - , locLine = 19 + , locLine = 27 , locColumn = 1 } ) Nothing @@ -371,7 +467,7 @@ ( ExprReplacePred ( Location { locFile = "test/examples/replace.tex" - , locLine = 20 + , locLine = 28 , locColumn = 16 } ) @@ -389,7 +485,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 20 + , locLine = 28 , locColumn = 44 } ) @@ -402,7 +498,7 @@ ( ExprFiniteSet ( Location { locFile = "test/examples/replace.tex" - , locLine = 20 + , locLine = 28 , locColumn = 46 } ) @@ -418,7 +514,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/replace.tex" - , locLine = 25 + , locLine = 33 , locColumn = 1 } ) Nothing @@ -430,7 +526,7 @@ ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 26 + , locLine = 34 , locColumn = 6 } ) @@ -451,7 +547,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 26 + , locLine = 34 , locColumn = 16 } ) @@ -464,14 +560,14 @@ ( ExprReplace ( Location { locFile = "test/examples/replace.tex" - , locLine = 26 + , locLine = 34 , locColumn = 18 } ) ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 26 + , locLine = 34 , locColumn = 21 } ) @@ -513,4 +609,30 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 36 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 37 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "times" :| [] ) + ) + ) + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 38 + , locColumn = 1 + } + ) ]
\ No newline at end of file diff --git a/test/golden/replace/scanning.golden b/test/golden/replace/scanning.golden index a131d69..6d9ffb0 100644 --- a/test/golden/replace/scanning.golden +++ b/test/golden/replace/scanning.golden @@ -1,4 +1,28 @@ [ ScanFunctionSymbol + ( TokenCons + ( Command "cons" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "example_cons" ) +, ScanFunctionSymbol + ( TokenCons ParenL + ( HoleCons + ( TokenCons + ( Symbol "," ) + ( HoleCons ( TokenCons ParenR End ) ) + ) + ) + ) + ( Marker "example_pair" ) +, ScanFunctionSymbol ( HoleCons ( TokenCons ( Command "times" ) ( HoleCons End ) diff --git a/test/golden/replace/tokenizing.golden b/test/golden/replace/tokenizing.golden index d32c8ab..06ab46a 100644 --- a/test/golden/replace/tokenizing.golden +++ b/test/golden/replace/tokenizing.golden @@ -1,4 +1,38 @@ [ + [ BeginEnv "signature" + , Label "example_cons" + , BeginEnv "math" + , Command "cons" + , InvisibleBraceL + , Variable "y" + , InvisibleBraceR + , InvisibleBraceL + , Variable "X" + , InvisibleBraceR + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, + [ BeginEnv "signature" + , Label "example_pair" + , BeginEnv "math" + , ParenL + , Variable "x" + , Symbol "," + , Variable "y" + , ParenR + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, [ BeginEnv "axiom" , Label "cons" , BeginEnv "math" @@ -138,4 +172,13 @@ , Symbol "." , EndEnv "proposition" ] +, + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "times" :| [] ) + , Symbol "." + , EndEnv "proof" + ] ]
\ No newline at end of file diff --git a/test/golden/russell/parsing.golden b/test/golden/russell/parsing.golden index 8e680cd..3ab466f 100644 --- a/test/golden/russell/parsing.golden +++ b/test/golden/russell/parsing.golden @@ -266,62 +266,37 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 14 - , locColumn = 5 + , locColumn = 6 } ) Nothing - ( StmtConnected - { conn = Equivalence - , mloc = Nothing - , stmt1 = StmtFormula - { formula = FormulaChain - ( ChainBase - ( ExprVar - ( NamedVar "R" ) :| [] - ) Positive - ( Relation - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 12 - } - ) - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) [] - ) - ( ExprVar - ( NamedVar "R" ) :| [] + ( StmtFormula + { formula = FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "R" ) :| [] + ) Positive + ( Relation + ( Location + { locFile = "test/examples/russell.tex" + , locLine = 14 + , locColumn = 7 + } ) + ( RelationSymbol + ( Command "in" ) + ( ParameterArity 0 ) + ( Marker "elem" ) + ) [] ) - } - , stmt2 = StmtFormula - { formula = FormulaChain - ( ChainBase - ( ExprVar - ( NamedVar "R" ) :| [] - ) Negative - ( Relation - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 29 - } - ) - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) [] - ) - ( ExprVar - ( NamedVar "R" ) :| [] - ) + ( ExprVar + ( NamedVar "V" ) :| [] ) - } + ) } - ) JustificationEmpty + ) + ( JustificationRef + ( Marker "universal_set" :| [] ) + ) ( Contradiction ( Location { locFile = "test/examples/russell.tex" diff --git a/test/golden/russell/tokenizing.golden b/test/golden/russell/tokenizing.golden index beba3ee..9a739f8 100644 --- a/test/golden/russell/tokenizing.golden +++ b/test/golden/russell/tokenizing.golden @@ -65,19 +65,14 @@ , VisibleBraceR , EndEnv "math" , Symbol "." - , Word "then" , BeginEnv "math" , Variable "R" , Command "in" - , Variable "R" - , EndEnv "math" - , Word "iff" - , BeginEnv "math" - , Variable "R" - , Command "not" - , Command "in" - , Variable "R" + , Variable "V" , EndEnv "math" + , Word "by" + , Ref + ( "universal_set" :| [] ) , Symbol "." , Word "contradiction" , Symbol "." diff --git a/test/golden/union/parsing.golden b/test/golden/union/parsing.golden index 4225bd8..df6361e 100644 --- a/test/golden/union/parsing.golden +++ b/test/golden/union/parsing.golden @@ -1,9 +1,50 @@ -[ BlockAxiom +[ BlockSig ( Location { locFile = "test/examples/union.tex" , locLine = 1 , locColumn = 1 } + ) Nothing + ( Marker "example_union" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( HoleCons + ( TokenCons + ( Command "union" ) ( HoleCons End ) + ) + ) + ( Marker "union" ) LeftAssoc + ) + [ NamedVar "A" + , NamedVar "B" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/union.tex" + , locLine = 2 + , locColumn = 22 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockAxiom + ( Location + { locFile = "test/examples/union.tex" + , locLine = 5 + , locColumn = 1 + } ) ( Just [ Word "extensionality" ] @@ -14,7 +55,7 @@ ( SymbolicQuantified { loc = Location { locFile = "test/examples/union.tex" - , locLine = 2 + , locLine = 6 , locColumn = 13 } , quant = Universally @@ -33,7 +74,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 2 + , locLine = 6 , locColumn = 35 } ) @@ -57,7 +98,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 2 + , locLine = 6 , locColumn = 48 } ) @@ -85,7 +126,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 3 + , locLine = 7 , locColumn = 13 } ) @@ -105,7 +146,7 @@ , BlockAxiom ( Location { locFile = "test/examples/union.tex" - , locLine = 6 + , locLine = 10 , locColumn = 1 } ) Nothing @@ -118,7 +159,7 @@ ( Noun ( Location { locFile = "test/examples/union.tex" - , locLine = 7 + , locLine = 11 , locColumn = 19 } ) @@ -146,7 +187,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 8 + , locLine = 12 , locColumn = 7 } ) @@ -159,7 +200,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 8 + , locLine = 12 , locColumn = 11 } ) @@ -191,7 +232,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 8 + , locLine = 12 , locColumn = 28 } ) @@ -215,7 +256,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 8 + , locLine = 12 , locColumn = 40 } ) @@ -237,7 +278,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/union.tex" - , locLine = 11 + , locLine = 15 , locColumn = 1 } ) Nothing @@ -249,7 +290,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 12 + , locLine = 16 , locColumn = 6 } ) @@ -270,7 +311,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 12 + , locLine = 16 , locColumn = 16 } ) @@ -283,7 +324,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 12 + , locLine = 16 , locColumn = 18 } ) @@ -308,7 +349,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/union.tex" - , locLine = 15 + , locLine = 19 , locColumn = 1 } ) Nothing @@ -320,7 +361,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 16 + , locLine = 20 , locColumn = 7 } ) @@ -335,7 +376,7 @@ [ ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 16 + , locLine = 20 , locColumn = 7 } ) @@ -359,7 +400,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 16 + , locLine = 20 , locColumn = 26 } ) @@ -372,7 +413,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 16 + , locLine = 20 , locColumn = 28 } ) @@ -389,7 +430,7 @@ , ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 16 + , locLine = 20 , locColumn = 37 } ) @@ -415,21 +456,21 @@ , BlockProof ( Location { locFile = "test/examples/union.tex" - , locLine = 18 + , locLine = 22 , locColumn = 1 } ) ( Have ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 5 } ) Nothing ( SymbolicQuantified { loc = Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 5 } , quant = Universally @@ -441,7 +482,7 @@ , mloc = Just ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 25 } ) @@ -454,7 +495,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 30 } ) @@ -467,7 +508,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 35 } ) @@ -482,7 +523,7 @@ [ ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 35 } ) @@ -514,7 +555,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 63 } ) @@ -527,7 +568,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 67 } ) @@ -544,7 +585,7 @@ , ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 76 } ) @@ -571,14 +612,14 @@ ( Have ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 5 } ) Nothing ( SymbolicQuantified { loc = Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 5 } , quant = Universally @@ -590,7 +631,7 @@ , mloc = Just ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 25 } ) @@ -603,7 +644,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 30 } ) @@ -616,7 +657,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 34 } ) @@ -633,7 +674,7 @@ , ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 43 } ) @@ -663,7 +704,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 63 } ) @@ -676,7 +717,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 68 } ) @@ -691,7 +732,7 @@ [ ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 68 } ) @@ -721,7 +762,7 @@ ) ( Location { locFile = "test/examples/union.tex" - , locLine = 21 + , locLine = 25 , locColumn = 1 } ) diff --git a/test/golden/union/scanning.golden b/test/golden/union/scanning.golden index 0637a08..410ced6 100644 --- a/test/golden/union/scanning.golden +++ b/test/golden/union/scanning.golden @@ -1 +1,8 @@ -[]
\ No newline at end of file +[ ScanFunctionSymbol + ( HoleCons + ( TokenCons + ( Command "union" ) ( HoleCons End ) + ) + ) + ( Marker "example_union" ) +]
\ No newline at end of file diff --git a/test/golden/union/tokenizing.golden b/test/golden/union/tokenizing.golden index 1672765..37ce74e 100644 --- a/test/golden/union/tokenizing.golden +++ b/test/golden/union/tokenizing.golden @@ -1,4 +1,18 @@ [ + [ BeginEnv "signature" + , Label "example_union" + , BeginEnv "math" + , Variable "A" + , Command "union" + , Variable "B" + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, [ BeginEnv "axiom" , BracketL , Word "extensionality" diff --git a/test/phase5/exact-case-failure.tex b/test/phase5/exact-case-failure.tex new file mode 100644 index 0000000..95530d5 --- /dev/null +++ b/test/phase5/exact-case-failure.tex @@ -0,0 +1,14 @@ +\begin{proposition}\label{case_failure_exact} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$A=\emptyset$.} + Follows. + \caseOf{$A=\{A\}$.} + Follows. + \caseOf{$A=\{\emptyset\}$.} + Follows. + \end{byCase} +\end{proof} diff --git a/test/phase5/exact-cases-contradiction.tex b/test/phase5/exact-cases-contradiction.tex new file mode 100644 index 0000000..cf08a8e --- /dev/null +++ b/test/phase5/exact-cases-contradiction.tex @@ -0,0 +1,45 @@ +\begin{proposition}\label{cases_exact} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$A=\emptyset$.} + Follows. + \caseOf{$A=\{A\}$.} + Follows. + \caseOf{$A=A$.} + Follows. + \end{byCase} +\end{proof} + +\begin{proposition}\label{by_contradiction_exact} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + Suppose not. + Follows. +\end{proof} + +\begin{proposition}\label{arbitrary_contradiction_exact} + Let $A$ be a set. + Suppose $A\neq A$. + Then $A=A$. +\end{proposition} +\begin{proof} + Contradiction. +\end{proof} + +\begin{proposition}\label{omitted_case_exact} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$A=A$.} + Omitted. + \caseOf{$A\neq A$.} + Follows. + \end{byCase} +\end{proof} diff --git a/test/phase5/exact-contradiction-goal.tex b/test/phase5/exact-contradiction-goal.tex deleted file mode 100644 index 007683f..0000000 --- a/test/phase5/exact-contradiction-goal.tex +++ /dev/null @@ -1,7 +0,0 @@ -\begin{proposition}\label{phase5_invalid_contradiction} - For all $A$ we have $A = A$. -\end{proposition} -\begin{proof} - Fix $A$. - Contradiction. -\end{proof} diff --git a/test/phase5/exact-datatype.tex b/test/phase5/exact-datatype.tex index 515638f..1f856e1 100644 --- a/test/phase5/exact-datatype.tex +++ b/test/phase5/exact-datatype.tex @@ -2,7 +2,7 @@ Define $\phasefivedata$ inductively as follows. \begin{enumerate} \item $\phasefivezero \in \phasefivedata$. - \item $\phasefiveatom{n} \in \phasefivedata$ for $n \in \unions{\emptyset}$. + \item $\phasefiveatom{n} \in \phasefivedata$ for $n \in \{\emptyset\}$. \item $\phasefivejoin{x}{y} \in \phasefivedata$ for $x \in \phasefivedata$ and $y \in \phasefivedata$. \end{enumerate} \end{datatype} diff --git a/test/phase5/exact-definition-alias-failure.tex b/test/phase5/exact-definition-alias-failure.tex new file mode 100644 index 0000000..e83fb3a --- /dev/null +++ b/test/phase5/exact-definition-alias-failure.tex @@ -0,0 +1,3 @@ +\begin{definition}\label{phase5_combined_alias} + The parity combined value of $X$, $\cons{X}{X}$, is $X$. +\end{definition} diff --git a/test/phase5/exact-definition-annotation-failure.tex b/test/phase5/exact-definition-annotation-failure.tex new file mode 100644 index 0000000..f772475 --- /dev/null +++ b/test/phase5/exact-definition-annotation-failure.tex @@ -0,0 +1,3 @@ +\begin{definition}\label{phase5_restricted_annotation} + A set equal to $A$ $X$ is parity restricted iff $X = X$. +\end{definition} diff --git a/test/phase5/exact-definition-boundary.tex b/test/phase5/exact-definition-boundary.tex new file mode 100644 index 0000000..d0c756c --- /dev/null +++ b/test/phase5/exact-definition-boundary.tex @@ -0,0 +1,15 @@ +\begin{definition}\label{phase5_annotated_adjective} + A set $X$ is parity canonical iff $X = X$. +\end{definition} + +\begin{definition}\label{phase5_annotated_verb} + A set $X$ parity contains $Y$ iff $Y \in X$. +\end{definition} + +\begin{definition}\label{phase5_symbolic_primary} + $\phasefivesymbolic{X} = X$. +\end{definition} + +\begin{abbreviation}\label{phase5_functional_wrapper} + The parity symbolic value of $X$ is $\phasefivesymbolic{X}$. +\end{abbreviation} diff --git a/test/phase5/exact-definition-guard-failure.tex b/test/phase5/exact-definition-guard-failure.tex new file mode 100644 index 0000000..0bab2cc --- /dev/null +++ b/test/phase5/exact-definition-guard-failure.tex @@ -0,0 +1,4 @@ +\begin{definition}\label{phase5_guarded_definition} + Suppose $\top$. + The parity guarded value of $X$ is $X$. +\end{definition} diff --git a/test/phase5/exact-direct-contradictory.tex b/test/phase5/exact-direct-contradictory.tex new file mode 100644 index 0000000..e29498e --- /dev/null +++ b/test/phase5/exact-direct-contradictory.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{direct_contradictory_exact} + Let $A$ be a set. + Suppose $A\neq A$. + Then $A=A$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} diff --git a/test/phase5/exact-induction-ambiguous.tex b/test/phase5/exact-induction-ambiguous.tex new file mode 100644 index 0000000..8029041 --- /dev/null +++ b/test/phase5/exact-induction-ambiguous.tex @@ -0,0 +1,7 @@ +\begin{proposition}\label{phase5_ambiguous_set_induction} + Let $A,B$ be sets. + Then $A=A$. +\end{proposition} +\begin{proof}[Proof by \in-induction] + Follows. +\end{proof} diff --git a/test/phase5/exact-induction-fixed.tex b/test/phase5/exact-induction-fixed.tex new file mode 100644 index 0000000..500cc55 --- /dev/null +++ b/test/phase5/exact-induction-fixed.tex @@ -0,0 +1,11 @@ +\begin{proposition}\label{phase5_fixed_set_induction} + For all sets $x$ we have $x=x$. +\end{proposition} +\begin{proof} + Fix $x$. + Show $x=x$. + \begin{subproof}[Proof by \in-induction on $x$] + Follows. + \end{subproof} + Follows by assumption. +\end{proof} diff --git a/test/phase5/exact-induction-formula-quantified.tex b/test/phase5/exact-induction-formula-quantified.tex new file mode 100644 index 0000000..9f9b322 --- /dev/null +++ b/test/phase5/exact-induction-formula-quantified.tex @@ -0,0 +1,10 @@ +\begin{proposition}\label{phase5_formula_quantified_set_induction} + $\forall x. x = x$. +\end{proposition} +\begin{proof}[Proof by \in-induction] + Show $x = x$. + \begin{subproof} + Follows. + \end{subproof} + Follows by assumption. +\end{proof} diff --git a/test/phase5/exact-induction-initial.tex b/test/phase5/exact-induction-initial.tex new file mode 100644 index 0000000..542ab40 --- /dev/null +++ b/test/phase5/exact-induction-initial.tex @@ -0,0 +1,7 @@ +\begin{proposition}\label{phase5_initial_set_induction} + Suppose $x\in A$. + Then $x=x$. +\end{proposition} +\begin{proof}[Proof by \in-induction on $x$] + Follows. +\end{proof} diff --git a/test/phase5/exact-induction-nested.tex b/test/phase5/exact-induction-nested.tex index 060a787..e9c5402 100644 --- a/test/phase5/exact-induction-nested.tex +++ b/test/phase5/exact-induction-nested.tex @@ -1,10 +1,11 @@ \begin{proposition}\label{phase5_nested_set_induction} - For all sets $x$ we have $x = x$. + Let $A$ be a set. + Then for all $x\in A$ such that $x\neq A$ we have $x = x$. \end{proposition} \begin{proof} - Fix $x$. - Show $x = x$. - \begin{subproof}[Proof by \in-induction on $x$] + Show for all $x\in A$ such that $x\neq A$ we have $x = x$. + \begin{subproof}[Proof by \in-induction] + Assume $x\in A$ and $x\neq A$. Follows by assumption. \end{subproof} Follows by assumption. diff --git a/test/phase5/exact-inductive-nested-failure.tex b/test/phase5/exact-inductive-nested-failure.tex new file mode 100644 index 0000000..0a4e9a4 --- /dev/null +++ b/test/phase5/exact-inductive-nested-failure.tex @@ -0,0 +1,21 @@ +\begin{axiom}\label{phase5_nested_failure_guard_1} + For all $A, x$ we have if $x\in\pow{\cumul{A}}$, then + $x\in\cumul{A}$. +\end{axiom} + +\begin{axiom}\label{phase5_nested_failure_guard_2} + For all $A, x$ we have if $x\in\pow{\pow{\cumul{A}}}$, then + $x\in\cumul{A}$. +\end{axiom} + +\begin{inductive}\label{phase5_nested_failure} + Define $\phasefivenestedfailure{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If $x\in\pow{\phasefivenestedfailure{A}}$, then + $x\in\phasefivenestedfailure{A}$. + \item If $x\in\pow{\pow{\phasefivenestedfailure{A}}}$, then + $x\in\phasefivenestedfailure{A}$. + \item If $y\in\pow{\phasefivenestedfailure{A}}$, then + $y\in\phasefivenestedfailure{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-nested.tex b/test/phase5/exact-inductive-nested.tex index a784652..cd7cf90 100644 --- a/test/phase5/exact-inductive-nested.tex +++ b/test/phase5/exact-inductive-nested.tex @@ -1,9 +1,20 @@ -% Nested recursion is outside the exact direct-inductive fragment. +\begin{proposition}\label{phase5_nested_guard} + For all $A, x$ we have if $x\in\pow{\cumul{A}}$, then + $A\in\cumul{A}$. +\end{proposition} +\begin{proof} + Fix $A, x$. + Assume $x\in\pow{\cumul{A}}$. +\end{proof} + +\begin{axiom}\label{phase5_nested_unsafe_support} + For all $A$ we have $A=A$. +\end{axiom} \begin{inductive}\label{phase5_nested} Define $\phasefivenested{A}\subseteq\cumul{A}$ inductively as follows. \begin{enumerate} \item If $x\in\pow{\phasefivenested{A}}$, then - $x\in\phasefivenested{A}$. + $A\in\phasefivenested{A}$. \end{enumerate} \end{inductive} diff --git a/test/phase5/exact-inductive-outside-membership.tex b/test/phase5/exact-inductive-outside-membership.tex new file mode 100644 index 0000000..0cefc39 --- /dev/null +++ b/test/phase5/exact-inductive-outside-membership.tex @@ -0,0 +1,7 @@ +\begin{inductive}\label{phase5_nested_outside_membership} + Define $\phasefiveoutside{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If $\phasefiveoutside{A}=\phasefiveoutside{A}$, then + $A\in\phasefiveoutside{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-recursive-domain.tex b/test/phase5/exact-inductive-recursive-domain.tex new file mode 100644 index 0000000..2259e9e --- /dev/null +++ b/test/phase5/exact-inductive-recursive-domain.tex @@ -0,0 +1,6 @@ +\begin{inductive}\label{phase5_recursive_domain} + Define $\phasefivedomain{A}\subseteq\phasefivedomain{A}$ inductively as follows. + \begin{enumerate} + \item $A\in\phasefivedomain{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-recursive-element.tex b/test/phase5/exact-inductive-recursive-element.tex new file mode 100644 index 0000000..c8ea915 --- /dev/null +++ b/test/phase5/exact-inductive-recursive-element.tex @@ -0,0 +1,7 @@ +\begin{inductive}\label{phase5_nested_recursive_element} + Define $\phasefiveelement{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If $\phasefiveelement{A}\in\pow{\phasefiveelement{A}}$, then + $A\in\phasefiveelement{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-recursive-result.tex b/test/phase5/exact-inductive-recursive-result.tex new file mode 100644 index 0000000..3309c64 --- /dev/null +++ b/test/phase5/exact-inductive-recursive-result.tex @@ -0,0 +1,6 @@ +\begin{inductive}\label{phase5_recursive_result} + Define $\phasefiveresult{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item $\phasefiveresult{A}\in\phasefiveresult{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-unsupported-context.tex b/test/phase5/exact-inductive-unsupported-context.tex new file mode 100644 index 0000000..9783630 --- /dev/null +++ b/test/phase5/exact-inductive-unsupported-context.tex @@ -0,0 +1,7 @@ +\begin{inductive}\label{phase5_nested_unsupported_context} + Define $\phasefiveunsupported{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If $x\in\{z\in\phasefiveunsupported{A}\mid z=z\}$, then + $x\in\phasefiveunsupported{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-wrapper.tex b/test/phase5/exact-inductive-wrapper.tex new file mode 100644 index 0000000..057528c --- /dev/null +++ b/test/phase5/exact-inductive-wrapper.tex @@ -0,0 +1,22 @@ +\begin{abbreviation}\label{phase5_nested_wrapper} + $\phasefivenestedwrapper{A}=\pow{A}$. +\end{abbreviation} + +\begin{proposition}\label{phase5_nested_wrapper_guard} + For all $A, x$ we have if + $x\in\phasefivenestedwrapper{\cumul{A}}$, then + $A\in\cumul{A}$. +\end{proposition} +\begin{proof} + Fix $A, x$. + Assume $x\in\phasefivenestedwrapper{\cumul{A}}$. +\end{proof} + +\begin{inductive}\label{phase5_nested_wrapper_inductive} + Define $\phasefivenestedwrapped{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If + $x\in\phasefivenestedwrapper{\phasefivenestedwrapped{A}}$, then + $A\in\phasefivenestedwrapped{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-inductive-wrong-arguments.tex b/test/phase5/exact-inductive-wrong-arguments.tex new file mode 100644 index 0000000..76f7508 --- /dev/null +++ b/test/phase5/exact-inductive-wrong-arguments.tex @@ -0,0 +1,7 @@ +\begin{inductive}\label{phase5_nested_wrong_arguments} + Define $\phasefivewrongargs{A}\subseteq\cumul{A}$ inductively as follows. + \begin{enumerate} + \item If $x\in\pow{\phasefivewrongargs{x}}$, then + $x\in\phasefivewrongargs{A}$. + \end{enumerate} +\end{inductive} diff --git a/test/phase5/exact-local-definition.tex b/test/phase5/exact-local-definition.tex index a1d2fcf..ddbd9d8 100644 --- a/test/phase5/exact-local-definition.tex +++ b/test/phase5/exact-local-definition.tex @@ -8,7 +8,7 @@ \begin{subproof} Fix $x$. Assume $x \in B$. - Follows by assumption. + Follows. \end{subproof} Follows by assumption. \end{proof} diff --git a/test/phase5/exact-proof-local-reasoning.tex b/test/phase5/exact-proof-local-reasoning.tex new file mode 100644 index 0000000..40f9343 --- /dev/null +++ b/test/phase5/exact-proof-local-reasoning.tex @@ -0,0 +1,82 @@ +\begin{proposition}\label{suffices_exact} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + It suffices to show that $A=A\land A=A$. + Follows. +\end{proof} + +\begin{proposition}\label{calculation_equality_exact} + Let $A$ be a set. + Suppose $A=\emptyset\land \emptyset=\{A\}$. + Then $A=\{A\}$. +\end{proposition} +\begin{proof} + \begin{align*} + A + &= \emptyset + \explanation{by \cref{suffices_exact}} + \\ + &= \{A\} + \explanation{by assumption} + \end{align*} + Follows by assumption. +\end{proof} + +\begin{proposition}\label{calculation_biconditional_exact} + Let $A$ be a set. + $(A=A)\iff ((A=A)\lor(A\neq A))$. +\end{proposition} +\begin{proof} + \begin{align*} + A=A + &\iff \top + \\ + &\iff (A=A)\lor(A\neq A) + \explanation{by assumption} + \end{align*} + Follows by assumption. +\end{proof} + +\begin{proposition}\label{calculation_quantified_exact} + Let $A$ be a set. + For all $x,y\in A$ such that $x=y$ we have $x=y$. +\end{proposition} +\begin{proof} + For all $x,y\in A$ such that $x=y$, we have + \begin{align*} + x + &= y + \end{align*} + Follows by assumption. +\end{proof} + +\begin{proposition}\label{since_structural_exact} + Let $A$ be a set. + Suppose $A=A$. + Then $A=A$. +\end{proposition} +\begin{proof} + Since $A=A$, we have $A=A$ by assumption. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{since_discharge_exact} + Let $A,B$ be sets. + Suppose $A=A$. + Then $A=A$. +\end{proposition} +\begin{proof} + Since $B=B$, we have $A=A$ by assumption. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{suffices_omitted_exact} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + It suffices to show that $A=A$. + Omitted. +\end{proof} diff --git a/test/phase5/exact-proof-parity-invalid-assume.tex b/test/phase5/exact-proof-parity-invalid-assume.tex new file mode 100644 index 0000000..3bb04bc --- /dev/null +++ b/test/phase5/exact-proof-parity-invalid-assume.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{invalid_disjunct_assume} + Let $A,B$ be sets. + $A=A$ or $B=B$. +\end{proposition} +\begin{proof} + Assume $A=A$. + Follows. +\end{proof} diff --git a/test/phase5/exact-proof-parity-invalid-fix-shape.tex b/test/phase5/exact-proof-parity-invalid-fix-shape.tex new file mode 100644 index 0000000..16a58a2 --- /dev/null +++ b/test/phase5/exact-proof-parity-invalid-fix-shape.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{invalid_fix_shape} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + Fix $x\in A$. + Follows. +\end{proof} diff --git a/test/phase5/exact-proof-parity-invalid-fix.tex b/test/phase5/exact-proof-parity-invalid-fix.tex new file mode 100644 index 0000000..0a2b24c --- /dev/null +++ b/test/phase5/exact-proof-parity-invalid-fix.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{invalid_bounded_fix} + Let $A$ be a set. + For all $x\in A$ we have $x\in A$. +\end{proposition} +\begin{proof} + Fix $x\notin A$. + Follows. +\end{proof} diff --git a/test/phase5/exact-proof-parity.tex b/test/phase5/exact-proof-parity.tex new file mode 100644 index 0000000..73d849f --- /dev/null +++ b/test/phase5/exact-proof-parity.tex @@ -0,0 +1,107 @@ +\begin{proposition}\label{bounded_fix_single} + Let $A$ be a set. + For all $x\in A$ we have $x\in A$. +\end{proposition} +\begin{proof} + Fix $x\in A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{bounded_fix_multiple} + Let $A$ be a set. + For all $x,y\in A$ we have $x\in A$ and $y\in A$. +\end{proposition} +\begin{proof} + Fix $x,y\in A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{bounded_fix_negative} + Let $A$ be a set. + For all $x\notin A$ we have $x\notin A$. +\end{proposition} +\begin{proof} + Fix $x\notin A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{fix_such_that} + Let $A$ be a set. + For all $x$ such that $x\in A$ we have $x\in A$. +\end{proposition} +\begin{proof} + Fix $x$ such that $x\in A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{assume_left_conjunct} + Let $A,B$ be sets. + If $A=A$ and $B=B$, then $A=A$. +\end{proposition} +\begin{proof} + Assume $A=A$. + Assume $B=B$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{assume_right_conjunct} + Let $A,B$ be sets. + If $A=A$ and $B=B$, then $B=B$. +\end{proposition} +\begin{proof} + Assume $B=B$. + Assume $A=A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{take_bounded} + Let $A$ be a set. + Suppose there exists $x\in A$ such that $x=x$. + Then $A=A$. +\end{proposition} +\begin{proof} + Take $x\in A$ such that $x=x$ by assumption. + We have $x\in A$ by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{take_named_noun} + Let $A$ be a set. + Suppose there exist sets $x,y$ such that $x=x$ and $y=y$. + Then $A=A$. +\end{proposition} +\begin{proof} + Take a set $x,y$ such that $x=x$ and $y=y$ by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{take_anonymous_noun} + Let $A$ be a set. + Suppose there exists a set. + Then $A=A$. +\end{proposition} +\begin{proof} + Take a set by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{existential_have_witness} + Let $A$ be a set. + Suppose there exists $x\in A$ such that $x=x$. + Then $A=A$. +\end{proposition} +\begin{proof} + We have there exists $x\in A$ such that $x=x$ by assumption. + We have $x\in A$ by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{take_omitted_continuation} + Let $A$ be a set. + Suppose there exists $x\in A$ such that $x=x$. + Then $A=A$. +\end{proposition} +\begin{proof} + Take $x\in A$ such that $x=x$ by assumption. + Omitted. +\end{proof} diff --git a/test/phase5/exact-quantified-proposition-terms.tex b/test/phase5/exact-quantified-proposition-terms.tex new file mode 100644 index 0000000..b713700 --- /dev/null +++ b/test/phase5/exact-quantified-proposition-terms.tex @@ -0,0 +1,22 @@ +\begin{abbreviation}\label{phase5_quantified_identity} + The phase five quantified identity of $A$ is $A$. +\end{abbreviation} + +\begin{abbreviation}\label{phase5_quantified_contains} + $A$ contains $B$ iff $B\in A$. +\end{abbreviation} + +\begin{proposition}\label{phase5_quantified_function_argument} + The phase five quantified identity of every set $A$ is equal to $A$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{phase5_quantified_verb_argument} + Let $A$ be a set. + Then $A$ contains every element of $A$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} diff --git a/test/phase5/exact-quantified-subject-nested.tex b/test/phase5/exact-quantified-subject-nested.tex deleted file mode 100644 index 69bed48..0000000 --- a/test/phase5/exact-quantified-subject-nested.tex +++ /dev/null @@ -1,9 +0,0 @@ -\import{set.tex} - -\begin{definition}\label{phase5_contains} - $A$ contains $B$ iff $B\in A$. -\end{definition} - -\begin{proposition}\label{phase5_nested_quantified_subject} - Then $A$ contains every set. -\end{proposition} diff --git a/test/phase5/exact-quantified-term-valued.tex b/test/phase5/exact-quantified-term-valued.tex new file mode 100644 index 0000000..8a841f5 --- /dev/null +++ b/test/phase5/exact-quantified-term-valued.tex @@ -0,0 +1,3 @@ +\begin{abbreviation}\label{phase5_invalid_quantified_value} + The phase five invalid quantified value of $A$ is every set. +\end{abbreviation} diff --git a/test/phase5/exact-relational-replacement-failure.tex b/test/phase5/exact-relational-replacement-failure.tex new file mode 100644 index 0000000..915ba91 --- /dev/null +++ b/test/phase5/exact-relational-replacement-failure.tex @@ -0,0 +1,7 @@ +\begin{definition}\label{phase5_relational_prefix} + $\phasefiverelationalprefix = \emptyset$. +\end{definition} + +\begin{definition}\label{phase5_relational_nonfunctional} + $\phasefivenonfunctional{A} = \{ y \mid \exists x\in A. y = y \}$. +\end{definition} diff --git a/test/phase5/exact-relational-replacement-local-failure.tex b/test/phase5/exact-relational-replacement-local-failure.tex new file mode 100644 index 0000000..6a051cd --- /dev/null +++ b/test/phase5/exact-relational-replacement-local-failure.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{phase5_relational_local_failure} + For every set $A$ we have $A = A$. +\end{proposition} +\begin{proof} + Fix $A$. + Let $B = \{ y \mid \exists x\in A. y = y \}$. + Follows. +\end{proof} diff --git a/test/phase5/exact-relational-replacement.tex b/test/phase5/exact-relational-replacement.tex new file mode 100644 index 0000000..43ef06f --- /dev/null +++ b/test/phase5/exact-relational-replacement.tex @@ -0,0 +1,16 @@ +\begin{axiom}\label{phase5_relational_support} + For every set $A$ we have $A = A$. +\end{axiom} + +\begin{definition}\label{phase5_relational_replacement_definition} + $\phasefiverelational{A} = \{ y \mid \exists x\in A. y = x \}$. +\end{definition} + +\begin{proposition}\label{phase5_relational_replacement_local} + For every set $A$ we have $A = A$. +\end{proposition} +\begin{proof} + Fix $A$. + Let $B = \{ y \mid \exists x\in A. y = x \}$. + Follows. +\end{proof} diff --git a/test/phase5/exact-replacement.tex b/test/phase5/exact-replacement.tex index 901fabe..d23ba42 100644 --- a/test/phase5/exact-replacement.tex +++ b/test/phase5/exact-replacement.tex @@ -8,5 +8,4 @@ \begin{proof} Fix $A, x$. Assume $x \in A$. - Follows by assumption. \end{proof} diff --git a/test/phase5/exact-separation.tex b/test/phase5/exact-separation.tex index e5b23a6..5b7e39d 100644 --- a/test/phase5/exact-separation.tex +++ b/test/phase5/exact-separation.tex @@ -3,10 +3,9 @@ \end{definition} \begin{proposition}\label{phase5_separation_theorem} - For all $A, x$ we have if $x \in \{ y \in A \mid y = y \}$, then $x \in A$. + For all $A, x$ we have if $x \in \phasefiveseparation{A}$, then $x \in A$. \end{proposition} \begin{proof} Fix $A, x$. - Assume $x \in \{ y \in A \mid y = y \}$. - Follows by assumption. + Assume $x \in \phasefiveseparation{A}$. \end{proof} diff --git a/test/phase5/exact-structure.tex b/test/phase5/exact-structure.tex index b1a0d86..fb34abe 100644 --- a/test/phase5/exact-structure.tex +++ b/test/phase5/exact-structure.tex @@ -25,3 +25,69 @@ \begin{proof} Follows by assumption. \end{proof} + +\begin{proposition}\label{pointed_self_member} + Let $X$ be a pointed set. + Then $X \in X$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_self_member_explicit} + Let $X$ be a pointed set. + Then $X \in \carrier[X]$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_self_not_member} + Let $X$ be a pointed set. + Then $X \notin X$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_self_not_member_explicit} + Let $X$ be a pointed set. + Then $X \notin \carrier[X]$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_self_element} + Let $X$ be a pointed set. + Then $X$ is an element of $X$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_self_element_explicit} + Let $X$ be a pointed set. + Then $X$ is an element of $\carrier[X]$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_header_member} + Let $X$ be a pointed set. + Let $x \in X$. + Then $x = x$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_header_member_explicit} + Let $X$ be a pointed set. + Let $x \in \carrier[X]$. + Then $x = x$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} diff --git a/test/phase7/calculation-link-order.tex b/test/phase7/calculation-link-order.tex new file mode 100644 index 0000000..48ff318 --- /dev/null +++ b/test/phase7/calculation-link-order.tex @@ -0,0 +1,13 @@ +\begin{proposition}\label{calculation_link_order} + Let $A,B,C$ be sets. + $A=C$. +\end{proposition} +\begin{proof} + \begin{align*} + A + &= B + \\ + &= C + \end{align*} + Follows by assumption. +\end{proof} |