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/proofassume/encoding tasks.golden | 17 ++ test/golden/proofassume/generating tasks.golden | 261 ++++++++++++++++++++++++ test/golden/proofassume/glossing.golden | 171 ++++++++++++++++ test/golden/proofassume/parsing.golden | 201 ++++++++++++++++++ test/golden/proofassume/scanning.golden | 1 + test/golden/proofassume/tokenizing.golden | 80 ++++++++ test/golden/proofassume/verification.golden | 1 + 7 files changed, 732 insertions(+) create mode 100644 test/golden/proofassume/encoding tasks.golden create mode 100644 test/golden/proofassume/generating tasks.golden create mode 100644 test/golden/proofassume/glossing.golden create mode 100644 test/golden/proofassume/parsing.golden create mode 100644 test/golden/proofassume/scanning.golden create mode 100644 test/golden/proofassume/tokenizing.golden create mode 100644 test/golden/proofassume/verification.golden (limited to 'test/golden/proofassume') diff --git a/test/golden/proofassume/encoding tasks.golden b/test/golden/proofassume/encoding tasks.golden new file mode 100644 index 0000000..43cc166 --- /dev/null +++ b/test/golden/proofassume/encoding tasks.golden @@ -0,0 +1,17 @@ +fof(assumetest,conjecture,elem(fx,fy)). +fof(assumetest1,axiom,elem(fx,fy)). +------------------ +fof(assumetest,conjecture,elem(fx,fy)). +fof(assumetest1,axiom,elem(fx,fy)). +fof(assumetest2,axiom,elem(fx,fy)). +------------------ +fof(assumetesttwo,conjecture,elem(fx,fy)). +fof(assumetest,axiom,![Xx,Xy]:(elem(Xx,Xy)=>elem(Xx,Xy))). +fof(assumetesttwo1,axiom,elem(fx,fy)). +fof(assumetesttwo2,axiom,elem(fa,fb)). +------------------ +fof(assumetesttwo,conjecture,elem(fx,fy)). +fof(assumetest,axiom,![Xx,Xy]:(elem(Xx,Xy)=>elem(Xx,Xy))). +fof(assumetesttwo1,axiom,elem(fx,fy)). +fof(assumetesttwo2,axiom,elem(fx,fy)). +fof(assumetesttwo3,axiom,elem(fa,fb)). \ No newline at end of file diff --git a/test/golden/proofassume/generating tasks.golden b/test/golden/proofassume/generating tasks.golden new file mode 100644 index 0000000..e66cf4a --- /dev/null +++ b/test/golden/proofassume/generating tasks.golden @@ -0,0 +1,261 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "assumetest1" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ] + , taskConjectureLabel = Marker "assumetest" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "assumetest1" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + , + ( Marker "assumetest2" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ] + , taskConjectureLabel = Marker "assumetest" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "assumetest" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "assumetesttwo1" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + , + ( Marker "assumetesttwo2" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ] + , taskConjectureLabel = Marker "assumetesttwo" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "assumetest" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "assumetesttwo1" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + , + ( Marker "assumetesttwo2" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + , + ( Marker "assumetesttwo3" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ] + , taskConjectureLabel = Marker "assumetesttwo" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + } +] \ No newline at end of file diff --git a/test/golden/proofassume/glossing.golden b/test/golden/proofassume/glossing.golden new file mode 100644 index 0000000..28b0e79 --- /dev/null +++ b/test/golden/proofassume/glossing.golden @@ -0,0 +1,171 @@ +[ BlockLemma + ( SourcePos + { sourceName = "test/examples/proofassume.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "assumetest" ) + ( Lemma [] + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/proofassume.tex" + , sourceLine = Pos 4 + , sourceColumn = Pos 1 + } + ) + ( Assume + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( Have + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) JustificationEmpty ( Qed JustificationEmpty ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/proofassume.tex" + , sourceLine = Pos 9 + , sourceColumn = Pos 1 + } + ) + ( Marker "assumetesttwo" ) + ( Lemma [] + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/proofassume.tex" + , sourceLine = Pos 12 + , sourceColumn = Pos 1 + } + ) + ( Assume + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + ) + ( Assume + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( Have + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) JustificationEmpty ( Qed JustificationEmpty ) + ) + ) + ) +] \ No newline at end of file diff --git a/test/golden/proofassume/parsing.golden b/test/golden/proofassume/parsing.golden new file mode 100644 index 0000000..57e542c --- /dev/null +++ b/test/golden/proofassume/parsing.golden @@ -0,0 +1,201 @@ +[ BlockLemma + ( SourcePos + { sourceName = "test/examples/proofassume.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "assumetest" ) + ( Lemma [] + ( StmtConnected Implication + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/proofassume.tex" + , sourceLine = Pos 4 + , sourceColumn = Pos 1 + } + ) + ( Assume + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ( Have Nothing + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) JustificationEmpty ( Qed JustificationEmpty ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/proofassume.tex" + , sourceLine = Pos 9 + , sourceColumn = Pos 1 + } + ) + ( Marker "assumetesttwo" ) + ( Lemma [] + ( StmtConnected Implication + ( StmtConnected Conjunction + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "b" ) :| [] + ) + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/proofassume.tex" + , sourceLine = Pos 12 + , sourceColumn = Pos 1 + } + ) + ( Assume + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "b" ) :| [] + ) + ) + ) + ) + ( Assume + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ( Have Nothing + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) JustificationEmpty ( Qed JustificationEmpty ) + ) + ) + ) +] \ No newline at end of file diff --git a/test/golden/proofassume/scanning.golden b/test/golden/proofassume/scanning.golden new file mode 100644 index 0000000..0637a08 --- /dev/null +++ b/test/golden/proofassume/scanning.golden @@ -0,0 +1 @@ +[] \ No newline at end of file diff --git a/test/golden/proofassume/tokenizing.golden b/test/golden/proofassume/tokenizing.golden new file mode 100644 index 0000000..cc97454 --- /dev/null +++ b/test/golden/proofassume/tokenizing.golden @@ -0,0 +1,80 @@ +[ BeginEnv "proposition" +, Label "assumetest" +, Word "if" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Variable "y" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Variable "y" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proof" +, Word "assume" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Variable "y" +, EndEnv "math" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Variable "y" +, EndEnv "math" +, Symbol "." +, EndEnv "proof" +, BeginEnv "proposition" +, Label "assumetesttwo" +, Word "if" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Variable "y" +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "b" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Variable "y" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proof" +, Word "assume" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "b" +, EndEnv "math" +, Symbol "." +, Word "assume" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Variable "y" +, EndEnv "math" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Variable "y" +, EndEnv "math" +, Symbol "." +, EndEnv "proof" +] \ No newline at end of file diff --git a/test/golden/proofassume/verification.golden b/test/golden/proofassume/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/proofassume/verification.golden @@ -0,0 +1 @@ +VerificationSuccess \ No newline at end of file -- cgit v1.2.3