summaryrefslogtreecommitdiff
path: root/test/golden/proofassume
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/proofassume')
-rw-r--r--test/golden/proofassume/encoding tasks.golden17
-rw-r--r--test/golden/proofassume/generating tasks.golden261
-rw-r--r--test/golden/proofassume/glossing.golden171
-rw-r--r--test/golden/proofassume/parsing.golden201
-rw-r--r--test/golden/proofassume/scanning.golden1
-rw-r--r--test/golden/proofassume/tokenizing.golden80
-rw-r--r--test/golden/proofassume/verification.golden1
7 files changed, 732 insertions, 0 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-06 09:38:23 +0000