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 --- .../proofdefinefunction/encoding tasks.golden | 9 + .../proofdefinefunction/generating tasks.golden | 332 +++++++++++++++++++++ test/golden/proofdefinefunction/glossing.golden | 163 ++++++++++ test/golden/proofdefinefunction/parsing.golden | 184 ++++++++++++ test/golden/proofdefinefunction/scanning.golden | 30 ++ test/golden/proofdefinefunction/tokenizing.golden | 94 ++++++ .../golden/proofdefinefunction/verification.golden | 1 + 7 files changed, 813 insertions(+) create mode 100644 test/golden/proofdefinefunction/encoding tasks.golden create mode 100644 test/golden/proofdefinefunction/generating tasks.golden create mode 100644 test/golden/proofdefinefunction/glossing.golden create mode 100644 test/golden/proofdefinefunction/parsing.golden create mode 100644 test/golden/proofdefinefunction/scanning.golden create mode 100644 test/golden/proofdefinefunction/tokenizing.golden create mode 100644 test/golden/proofdefinefunction/verification.golden (limited to 'test/golden/proofdefinefunction') diff --git a/test/golden/proofdefinefunction/encoding tasks.golden b/test/golden/proofdefinefunction/encoding tasks.golden new file mode 100644 index 0000000..36c916f --- /dev/null +++ b/test/golden/proofdefinefunction/encoding tasks.golden @@ -0,0 +1,9 @@ +fof(definefunctiontest,conjecture,elem(fx,fy)=>elem(fx,fy)). +fof(relation,axiom,![Xf]:(relation(Xf)<=>Xf=Xf)). +fof(rightunique,axiom,![Xf]:(rightunique(Xf)<=>Xf=Xf)). +fof(dom,axiom,![Xf]:dom(Xf)=Xf). +fof(apply,axiom,![Xf,Xx]:apply(Xf,Xx)=Xx). +fof(definefunctiontest1,axiom,relation(ff)). +fof(definefunctiontest2,axiom,rightunique(ff)). +fof(definefunctiontest3,axiom,![Xz]:(elem(Xz,fx)=>apply(ff,Xz)=Xz)). +fof(definefunctiontest4,axiom,dom(ff)=fx). \ No newline at end of file diff --git a/test/golden/proofdefinefunction/generating tasks.golden b/test/golden/proofdefinefunction/generating tasks.golden new file mode 100644 index 0000000..3ab9857 --- /dev/null +++ b/test/golden/proofdefinefunction/generating tasks.golden @@ -0,0 +1,332 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "relation" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "relation" ) + ] + , pl = + [ Just + ( Word "relations" ) + ] + } + ) + ) + ) + [ TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "f" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "f" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + , + ( Marker "rightunique" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "right-unique" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "f" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "f" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + , + ( Marker "dom" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "dom" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "f" ) + ) + ] + , TermVar + ( B + ( NamedVar "f" ) + ) + ] + ) + ) + ) + , + ( Marker "apply" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "apply" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "f" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + , + ( Marker "definefunctiontest1" + , TermSymbol + ( SymbolPredicate + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "relation" ) + ] + , pl = + [ Just + ( Word "relations" ) + ] + } + ) + ) + ) + [ TermVar + ( NamedVar "f" ) + ] + ) + , + ( Marker "definefunctiontest2" + , TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "right-unique" ) + ] + ) + ) + [ TermVar + ( NamedVar "f" ) + ] + ) + , + ( Marker "definefunctiontest3" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "z" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "x" ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "apply" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "f" ) + ) + ) + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + , TermVar + ( B + ( NamedVar "z" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "definefunctiontest4" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "dom" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "f" ) + ] + , TermVar + ( NamedVar "x" ) + ] + ) + ] + , taskConjectureLabel = Marker "definefunctiontest" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + } +] \ No newline at end of file diff --git a/test/golden/proofdefinefunction/glossing.golden b/test/golden/proofdefinefunction/glossing.golden new file mode 100644 index 0000000..931e5da --- /dev/null +++ b/test/golden/proofdefinefunction/glossing.golden @@ -0,0 +1,163 @@ +[ BlockDefn + ( SourcePos + { sourceName = "test/examples/proofdefinefunction.tex" + , sourceLine = Pos 3 + , sourceColumn = Pos 1 + } + ) + ( Marker "apply" ) + ( DefnOp + [ Just + ( Command "apply" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "f" + , NamedVar "x" + ] + ( TermVar + ( NamedVar "x" ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/proofdefinefunction.tex" + , sourceLine = Pos 8 + , sourceColumn = Pos 1 + } + ) + ( Marker "dom" ) + ( DefnOp + [ Just + ( Command "dom" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "f" ] + ( TermVar + ( NamedVar "f" ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/proofdefinefunction.tex" + , sourceLine = Pos 13 + , sourceColumn = Pos 1 + } + ) + ( Marker "rightunique" ) + ( DefnPredicate [] + ( PredicateAdj + [ Just + ( Word "right-unique" ) + ] + ) + ( NamedVar "f" :| [] ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "f" ) + , TermVar + ( NamedVar "f" ) + ] + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/proofdefinefunction.tex" + , sourceLine = Pos 18 + , sourceColumn = Pos 1 + } + ) + ( Marker "relation" ) + ( DefnPredicate [] + ( PredicateNoun + ( SgPl + { sg = + [ Just + ( Word "relation" ) + ] + , pl = + [ Just + ( Word "relations" ) + ] + } + ) + ) + ( NamedVar "f" :| [] ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "f" ) + , TermVar + ( NamedVar "f" ) + ] + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/proofdefinefunction.tex" + , sourceLine = Pos 22 + , sourceColumn = Pos 1 + } + ) + ( Marker "definefunctiontest" ) + ( 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/proofdefinefunction.tex" + , sourceLine = Pos 25 + , sourceColumn = Pos 1 + } + ) + ( DefineFunction + ( NamedVar "f" ) + ( NamedVar "z" ) + ( TermVar + ( NamedVar "z" ) + ) + ( TermVar + ( NamedVar "x" ) + ) ( Qed JustificationEmpty ) + ) +] \ No newline at end of file diff --git a/test/golden/proofdefinefunction/parsing.golden b/test/golden/proofdefinefunction/parsing.golden new file mode 100644 index 0000000..eba14ec --- /dev/null +++ b/test/golden/proofdefinefunction/parsing.golden @@ -0,0 +1,184 @@ +[ BlockDefn + ( SourcePos + { sourceName = "test/examples/proofdefinefunction.tex" + , sourceLine = Pos 3 + , sourceColumn = Pos 1 + } + ) + ( Marker "apply" ) + ( DefnOp + ( SymbolPattern + [ Just + ( Command "apply" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "f" + , NamedVar "x" + ] + ) + ( ExprVar + ( NamedVar "x" ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/proofdefinefunction.tex" + , sourceLine = Pos 8 + , sourceColumn = Pos 1 + } + ) + ( Marker "dom" ) + ( DefnOp + ( SymbolPattern + [ Just + ( Command "dom" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "f" ] + ) + ( ExprVar + ( NamedVar "f" ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/proofdefinefunction.tex" + , sourceLine = Pos 13 + , sourceColumn = Pos 1 + } + ) + ( Marker "rightunique" ) + ( Defn [] + ( DefnAdj Nothing + ( NamedVar "f" ) + ( Adj + [ Just + ( Word "right-unique" ) + ] [] + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "f" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "f" ) :| [] + ) + ) + ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/proofdefinefunction.tex" + , sourceLine = Pos 18 + , sourceColumn = Pos 1 + } + ) + ( Marker "relation" ) + ( Defn [] + ( DefnNoun + ( NamedVar "f" ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "relation" ) + ] + , pl = + [ Just + ( Word "relations" ) + ] + } + ) [] + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "f" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "f" ) :| [] + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/proofdefinefunction.tex" + , sourceLine = Pos 22 + , sourceColumn = Pos 1 + } + ) + ( Marker "definefunctiontest" ) + ( 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/proofdefinefunction.tex" + , sourceLine = Pos 25 + , sourceColumn = Pos 1 + } + ) + ( DefineFunction + ( NamedVar "f" ) + ( NamedVar "z" ) + ( ExprVar + ( NamedVar "z" ) + ) + ( NamedVar "z" ) + ( ExprVar + ( NamedVar "x" ) + ) ( Qed JustificationEmpty ) + ) +] \ No newline at end of file diff --git a/test/golden/proofdefinefunction/scanning.golden b/test/golden/proofdefinefunction/scanning.golden new file mode 100644 index 0000000..e5d7748 --- /dev/null +++ b/test/golden/proofdefinefunction/scanning.golden @@ -0,0 +1,30 @@ +[ ScanFunctionSymbol + [ Just + ( Command "apply" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "apply" ) +, ScanFunctionSymbol + [ Just + ( Command "dom" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "dom" ) +, ScanAdj + [ Just + ( Word "right-unique" ) + ] + ( Marker "rightunique" ) +, ScanNoun + [ Just + ( Word "relation" ) + ] + ( Marker "relation" ) +] \ No newline at end of file diff --git a/test/golden/proofdefinefunction/tokenizing.golden b/test/golden/proofdefinefunction/tokenizing.golden new file mode 100644 index 0000000..542a89c --- /dev/null +++ b/test/golden/proofdefinefunction/tokenizing.golden @@ -0,0 +1,94 @@ +[ BeginEnv "definition" +, Label "apply" +, BeginEnv "math" +, Command "apply" +, InvisibleBraceL +, Variable "f" +, InvisibleBraceR +, InvisibleBraceL +, Variable "x" +, InvisibleBraceR +, Symbol "=" +, Variable "x" +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "definition" +, Label "dom" +, BeginEnv "math" +, Command "dom" +, InvisibleBraceL +, Variable "f" +, InvisibleBraceR +, Symbol "=" +, Variable "f" +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "definition" +, Label "rightunique" +, BeginEnv "math" +, Variable "f" +, EndEnv "math" +, Word "is" +, Word "right-unique" +, Word "iff" +, BeginEnv "math" +, Variable "f" +, Symbol "=" +, Variable "f" +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "definition" +, Label "relation" +, BeginEnv "math" +, Variable "f" +, EndEnv "math" +, Word "is" +, Word "a" +, Word "relation" +, Word "iff" +, BeginEnv "math" +, Variable "f" +, Symbol "=" +, Variable "f" +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "proposition" +, Label "definefunctiontest" +, 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 "let" +, BeginEnv "math" +, Variable "f" +, ParenL +, Variable "z" +, ParenR +, Symbol "=" +, Variable "z" +, EndEnv "math" +, Word "for" +, BeginEnv "math" +, Variable "z" +, Command "in" +, Variable "x" +, EndEnv "math" +, Symbol "." +, EndEnv "proof" +] \ No newline at end of file diff --git a/test/golden/proofdefinefunction/verification.golden b/test/golden/proofdefinefunction/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/proofdefinefunction/verification.golden @@ -0,0 +1 @@ +VerificationSuccess \ No newline at end of file -- cgit v1.2.3