From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Sat, 10 Feb 2024 02:22:14 +0100 Subject: Initial commit --- test/golden/no-reflexive-set/encoding tasks.golden | 2 + .../no-reflexive-set/generating tasks.golden | 64 ++++++++++++++++++++++ test/golden/no-reflexive-set/glossing.golden | 43 +++++++++++++++ test/golden/no-reflexive-set/parsing.golden | 54 ++++++++++++++++++ test/golden/no-reflexive-set/scanning.golden | 1 + test/golden/no-reflexive-set/tokenizing.golden | 29 ++++++++++ test/golden/no-reflexive-set/verification.golden | 1 + 7 files changed, 194 insertions(+) create mode 100644 test/golden/no-reflexive-set/encoding tasks.golden create mode 100644 test/golden/no-reflexive-set/generating tasks.golden create mode 100644 test/golden/no-reflexive-set/glossing.golden create mode 100644 test/golden/no-reflexive-set/parsing.golden create mode 100644 test/golden/no-reflexive-set/scanning.golden create mode 100644 test/golden/no-reflexive-set/tokenizing.golden create mode 100644 test/golden/no-reflexive-set/verification.golden (limited to 'test/golden/no-reflexive-set') diff --git a/test/golden/no-reflexive-set/encoding tasks.golden b/test/golden/no-reflexive-set/encoding tasks.golden new file mode 100644 index 0000000..dc79b95 --- /dev/null +++ b/test/golden/no-reflexive-set/encoding tasks.golden @@ -0,0 +1,2 @@ +fof(in_irrefl,conjecture,~elem(fA,fA)). +fof(in_irrefl1,axiom,![XIndAntecedent]:(elem(XIndAntecedent,fA)=>~elem(XIndAntecedent,XIndAntecedent))). \ No newline at end of file diff --git a/test/golden/no-reflexive-set/generating tasks.golden b/test/golden/no-reflexive-set/generating tasks.golden new file mode 100644 index 0000000..3ed340b --- /dev/null +++ b/test/golden/no-reflexive-set/generating tasks.golden @@ -0,0 +1,64 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "in_irrefl1" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "IndAntecedent" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + ] + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "IndAntecedent" ) + ) + , TermVar + ( B + ( NamedVar "IndAntecedent" ) + ) + ] + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "in_irrefl" + , taskConjecture = Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "A" ) + ] + ) + } +] \ No newline at end of file diff --git a/test/golden/no-reflexive-set/glossing.golden b/test/golden/no-reflexive-set/glossing.golden new file mode 100644 index 0000000..a58b5b7 --- /dev/null +++ b/test/golden/no-reflexive-set/glossing.golden @@ -0,0 +1,43 @@ +[ BlockLemma + ( SourcePos + { sourceName = "test/examples/no-reflexive-set.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "in_irrefl" ) + ( Lemma [] + ( Quantified Universally + ( Scope + ( Connected Implication ( PropositionalConstant IsTop ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ) + ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/no-reflexive-set.tex" + , sourceLine = Pos 4 + , sourceColumn = Pos 1 + } + ) + ( BySetInduction Nothing ( Qed JustificationEmpty ) ) +] \ No newline at end of file diff --git a/test/golden/no-reflexive-set/parsing.golden b/test/golden/no-reflexive-set/parsing.golden new file mode 100644 index 0000000..3de5dcc --- /dev/null +++ b/test/golden/no-reflexive-set/parsing.golden @@ -0,0 +1,54 @@ +[ BlockLemma + ( SourcePos + { sourceName = "test/examples/no-reflexive-set.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "in_irrefl" ) + ( Lemma [] + ( StmtQuantPhrase + ( QuantPhrase Universally NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "set" ) + ] + , pl = + [ Just + ( Word "sets" ) + ] + } + ) [] + ) + ( + [ NamedVar "A" ] + ) ( [] ) ( Nothing ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "A" ) :| [] + ) Negative + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "A" ) :| [] + ) + ) + ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/no-reflexive-set.tex" + , sourceLine = Pos 4 + , sourceColumn = Pos 1 + } + ) + ( BySetInduction Nothing ( Qed JustificationEmpty ) ) +] \ No newline at end of file diff --git a/test/golden/no-reflexive-set/scanning.golden b/test/golden/no-reflexive-set/scanning.golden new file mode 100644 index 0000000..0637a08 --- /dev/null +++ b/test/golden/no-reflexive-set/scanning.golden @@ -0,0 +1 @@ +[] \ No newline at end of file diff --git a/test/golden/no-reflexive-set/tokenizing.golden b/test/golden/no-reflexive-set/tokenizing.golden new file mode 100644 index 0000000..16835be --- /dev/null +++ b/test/golden/no-reflexive-set/tokenizing.golden @@ -0,0 +1,29 @@ +[ BeginEnv "proposition" +, Label "in_irrefl" +, Word "for" +, Word "all" +, Word "sets" +, BeginEnv "math" +, Variable "A" +, EndEnv "math" +, Word "we" +, Word "have" +, BeginEnv "math" +, Variable "A" +, Command "not" +, Command "in" +, Variable "A" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proof" +, BracketL +, Word "proof" +, Word "by" +, Command "in" +, Word "-induction" +, BracketR +, Word "straightforward" +, Symbol "." +, EndEnv "proof" +] \ No newline at end of file diff --git a/test/golden/no-reflexive-set/verification.golden b/test/golden/no-reflexive-set/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/no-reflexive-set/verification.golden @@ -0,0 +1 @@ +VerificationSuccess \ No newline at end of file -- cgit v1.2.3