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/union/encoding tasks.golden | 21 + test/golden/union/generating tasks.golden | 1335 +++++++++++++++++++++++++++++ test/golden/union/glossing.golden | 456 ++++++++++ test/golden/union/parsing.golden | 406 +++++++++ test/golden/union/scanning.golden | 1 + test/golden/union/tokenizing.golden | 168 ++++ test/golden/union/verification.golden | 1 + 7 files changed, 2388 insertions(+) create mode 100644 test/golden/union/encoding tasks.golden create mode 100644 test/golden/union/generating tasks.golden create mode 100644 test/golden/union/glossing.golden create mode 100644 test/golden/union/parsing.golden create mode 100644 test/golden/union/scanning.golden create mode 100644 test/golden/union/tokenizing.golden create mode 100644 test/golden/union/verification.golden (limited to 'test/golden/union') diff --git a/test/golden/union/encoding tasks.golden b/test/golden/union/encoding tasks.golden new file mode 100644 index 0000000..34d92fd --- /dev/null +++ b/test/golden/union/encoding tasks.golden @@ -0,0 +1,21 @@ +fof(union_comm,conjecture,union(fA,fB)=union(fB,fA)). +fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))). +fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)). +------------------ +fof(union_assoc,conjecture,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC))))). +fof(union_comm,axiom,![XA,XB]:union(XA,XB)=union(XB,XA)). +fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))). +fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)). +------------------ +fof(union_assoc,conjecture,![Xa]:(elem(Xa,union(fA,union(fB,fC)))=>elem(Xa,union(union(fA,fB),fC)))). +fof(union_comm,axiom,![XA,XB]:union(XA,XB)=union(XB,XA)). +fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))). +fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)). +fof(union_assoc1,axiom,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC))))). +------------------ +fof(union_assoc,conjecture,union(union(fA,fB),fC)=union(fA,union(fB,fC))). +fof(union_comm,axiom,![XA,XB]:union(XA,XB)=union(XB,XA)). +fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))). +fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)). +fof(union_assoc1,axiom,![Xa]:(elem(Xa,union(fA,union(fB,fC)))=>elem(Xa,union(union(fA,fB),fC)))). +fof(union_assoc2,axiom,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC))))). \ No newline at end of file diff --git a/test/golden/union/generating tasks.golden b/test/golden/union/generating tasks.golden new file mode 100644 index 0000000..f7f72bb --- /dev/null +++ b/test/golden/union/generating tasks.golden @@ -0,0 +1,1335 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "union_defn" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ext" + , Quantified Universally + ( Scope + ( Connected Implication + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "union_comm" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "B" ) + , TermVar + ( NamedVar "A" ) + ] + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "union_comm" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "union_defn" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ext" + , Quantified Universally + ( Scope + ( Connected Implication + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "union_assoc" + , taskConjecture = Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ) + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "union_comm" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "union_defn" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ext" + , Quantified Universally + ( Scope + ( Connected Implication + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "union_assoc1" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "union_assoc" + , taskConjecture = Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ) + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "union_comm" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "union_defn" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ext" + , Quantified Universally + ( Scope + ( Connected Implication + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "union_assoc1" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "union_assoc2" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "union_assoc" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + , TermVar + ( NamedVar "C" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "B" ) + , TermVar + ( NamedVar "C" ) + ] + ] + ] + } +] \ No newline at end of file diff --git a/test/golden/union/glossing.golden b/test/golden/union/glossing.golden new file mode 100644 index 0000000..1925c15 --- /dev/null +++ b/test/golden/union/glossing.golden @@ -0,0 +1,456 @@ +[ BlockAxiom + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "ext" ) + ( Axiom + [ Asm + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + ) + ) + ) + ) + ] + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 6 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_defn" ) + ( Axiom + [ Asm ( PropositionalConstant IsTop ) + , Asm ( PropositionalConstant IsTop ) + ] + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "A" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "B" ) + ] + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 11 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_comm" ) + ( Lemma [] + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "B" ) + , TermVar + ( NamedVar "A" ) + ] + ] + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 15 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_assoc" ) + ( Lemma [] + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + , TermVar + ( NamedVar "C" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "B" ) + , TermVar + ( NamedVar "C" ) + ] + ] + ] + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 18 + , sourceColumn = Pos 1 + } + ) + ( Have + ( Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ) + ) + ) JustificationEmpty + ( Have + ( Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ) + ) + ) JustificationEmpty ( Qed JustificationEmpty ) + ) + ) +] \ No newline at end of file diff --git a/test/golden/union/parsing.golden b/test/golden/union/parsing.golden new file mode 100644 index 0000000..391f039 --- /dev/null +++ b/test/golden/union/parsing.golden @@ -0,0 +1,406 @@ +[ BlockAxiom + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "ext" ) + ( Axiom + [ AsmSuppose + ( SymbolicQuantified Universally + ( NamedVar "a" :| [] ) Unbounded Nothing + ( StmtConnected Equivalence + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "A" ) :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "B" ) :| [] + ) + ) + ) + ) + ) + ) + ] + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "A" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "B" ) :| [] + ) + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 6 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_defn" ) + ( Axiom + [ AsmLetNoun + ( NamedVar "A" :| + [ NamedVar "B" ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "set" ) + ] + , pl = + [ Just + ( Word "sets" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtConnected Equivalence + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "B" ) + ] :| [] + ) + ) + ) + ) + ( StmtConnected Disjunction + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "A" ) :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "B" ) :| [] + ) + ) + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 11 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_comm" ) + ( Lemma [] + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "B" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "B" ) + , ExprVar + ( NamedVar "A" ) + ] :| [] + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 15 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_assoc" ) + ( Lemma [] + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "B" ) + ] + , ExprVar + ( NamedVar "C" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "B" ) + , ExprVar + ( NamedVar "C" ) + ] + ] :| [] + ) + ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 18 + , sourceColumn = Pos 1 + } + ) + ( Have Nothing + ( SymbolicQuantified Universally + ( NamedVar "a" :| [] ) Unbounded Nothing + ( StmtConnected Implication + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "B" ) + ] + , ExprVar + ( NamedVar "C" ) + ] :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "B" ) + , ExprVar + ( NamedVar "C" ) + ] + ] :| [] + ) + ) + ) + ) + ) + ) JustificationEmpty + ( Have Nothing + ( SymbolicQuantified Universally + ( NamedVar "a" :| [] ) Unbounded Nothing + ( StmtConnected Implication + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "B" ) + , ExprVar + ( NamedVar "C" ) + ] + ] :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "B" ) + ] + , ExprVar + ( NamedVar "C" ) + ] :| [] + ) + ) + ) + ) + ) + ) JustificationEmpty ( Qed JustificationEmpty ) + ) + ) +] \ No newline at end of file diff --git a/test/golden/union/scanning.golden b/test/golden/union/scanning.golden new file mode 100644 index 0000000..0637a08 --- /dev/null +++ b/test/golden/union/scanning.golden @@ -0,0 +1 @@ +[] \ No newline at end of file diff --git a/test/golden/union/tokenizing.golden b/test/golden/union/tokenizing.golden new file mode 100644 index 0000000..e336098 --- /dev/null +++ b/test/golden/union/tokenizing.golden @@ -0,0 +1,168 @@ +[ BeginEnv "axiom" +, BracketL +, Word "extensionality" +, BracketR +, Label "ext" +, Word "suppose" +, Word "for" +, Word "all" +, BeginEnv "math" +, Variable "a" +, EndEnv "math" +, Word "we" +, Word "have" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, EndEnv "math" +, Word "iff" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "B" +, EndEnv "math" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Variable "A" +, Symbol "=" +, Variable "B" +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "axiom" +, Label "union_defn" +, Word "let" +, BeginEnv "math" +, Variable "A" +, Symbol "," +, Variable "B" +, EndEnv "math" +, Word "be" +, Word "sets" +, Symbol "." +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, Command "union" +, Variable "B" +, EndEnv "math" +, Word "iff" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, EndEnv "math" +, Word "or" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "B" +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "proposition" +, Label "union_comm" +, BeginEnv "math" +, Variable "A" +, Command "union" +, Variable "B" +, Symbol "=" +, Variable "B" +, Command "union" +, Variable "A" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proposition" +, Label "union_assoc" +, BeginEnv "math" +, ParenL +, Variable "A" +, Command "union" +, Variable "B" +, ParenR +, Command "union" +, Variable "C" +, Symbol "=" +, Variable "A" +, Command "union" +, ParenL +, Variable "B" +, Command "union" +, Variable "C" +, ParenR +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proof" +, Word "for" +, Word "all" +, BeginEnv "math" +, Variable "a" +, EndEnv "math" +, Word "we" +, Word "have" +, Word "if" +, BeginEnv "math" +, Variable "a" +, Command "in" +, ParenL +, Variable "A" +, Command "union" +, Variable "B" +, ParenR +, Command "union" +, Variable "C" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, Command "union" +, ParenL +, Variable "B" +, Command "union" +, Variable "C" +, ParenR +, EndEnv "math" +, Symbol "." +, Word "for" +, Word "all" +, BeginEnv "math" +, Variable "a" +, EndEnv "math" +, Word "we" +, Word "have" +, Word "if" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, Command "union" +, ParenL +, Variable "B" +, Command "union" +, Variable "C" +, ParenR +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "a" +, Command "in" +, ParenL +, Variable "A" +, Command "union" +, Variable "B" +, ParenR +, Command "union" +, Variable "C" +, EndEnv "math" +, Symbol "." +, EndEnv "proof" +] \ No newline at end of file diff --git a/test/golden/union/verification.golden b/test/golden/union/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/union/verification.golden @@ -0,0 +1 @@ +VerificationSuccess \ No newline at end of file -- cgit v1.2.3