adding Euler's identity

test/built-in/eulers_identity.n3s

@@ -0,0 +1,106 @@
+# ----------------
+# Euler's identity
+# ----------------
+#
+# The most beautiful theorem in mathematics
+#
+#   i*pi
+# e      + 1 = 0
+#
+# See https://en.wikipedia.org/wiki/Euler%27s_identity
+
+@prefix math: <http://www.w3.org/2000/10/swap/math#>.
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix complex: <http://eyereasoner.github.io/eye/complex#>.
+@prefix : <urn:example:>.
+
+(_:A _:B _:C _:D _:E _:F) log:onNegativeSurface {
+    () log:onNegativeQuestionSurface {
+        ((_:A _:B) (_:C _:D)) complex:sum (_:E _:F).
+    }.
+    (_:A _:C) math:sum _:E.
+    (_:B _:D) math:sum _:F.
+}.
+
+(_:A _:B _:C _:D _:E _:F _:R _:T _:Z1 _:Z2 _:Z3 _:Z4 _:Z5 _:Z6 _:Z7 _:Z8 _:Z9 _:Z10) log:onNegativeSurface {
+    () log:onNegativeQuestionSurface {
+        ((_:A _:B) (_:C _:D)) complex:exponentiation (_:E _:F).
+    }.
+    (_:A _:B) complex:polar (_:R _:T).
+    (_:R _:C) math:exponentiation _:Z1.
+    _:D math:negation _:Z2.
+    (_:Z2 _:T) math:product _:Z3.
+    (2.718281828459045 _:Z3) math:exponentiation _:Z4.
+    (2.718281828459045 _:Z5) math:exponentiation _:R.
+    (_:D _:Z5) math:product _:Z6.
+    (_:C _:T) math:product _:Z7.
+    (_:Z6 _:Z7) math:sum _:Z8.
+    _:Z8 math:cos _:Z9.
+    (_:Z1 _:Z4 _:Z9) math:product _:E.
+    _:Z8 math:sin _:Z10.
+    (_:Z1 _:Z4 _:Z10) math:product _:F.
+}.
+
+(_:X _:Y _:R _:T _:Tp _:Z1 _:Z2 _:Z3 _:Z4 _:Z5) log:onNegativeSurface {
+    () log:onNegativeQuestionSurface {
+        (_:X _:Y) complex:polar (_:R _:Tp).
+    }.
+    (_:X 2) math:exponentiation _:Z1.
+    (_:Y 2) math:exponentiation _:Z2.
+    (_:Z1 _:Z2) math:sum _:Z3.
+    (_:Z3 0.5) math:exponentiation _:R.
+    _:X math:absoluteValue _:Z4.
+    (_:Z4 _:R) math:quotient _:Z5.
+    _:Z5 math:acos _:T.
+    (_:X _:Y _:T) complex:dial _:Tp.
+}.
+
+(_:X _:Y _:T _:Tp) log:onNegativeSurface {
+    () log:onNegativeQuestionSurface {
+        (_:X _:Y _:T) complex:dial _:Tp.
+    }.
+    _:X math:notLessThan 0.
+    _:Y math:notLessThan 0.
+    (0 _:T) math:sum _:Tp.
+}.
+
+(_:X _:Y _:T _:Tp) log:onNegativeSurface {
+    () log:onNegativeQuestionSurface {
+        (_:X _:Y _:T) complex:dial _:Tp.
+    }.
+    _:X math:lessThan 0.
+    _:Y math:notLessThan 0.
+    (3.141592653589793 _:T) math:difference _:Tp.
+}.
+
+(_:X _:Y _:T _:Tp) log:onNegativeSurface {
+    () log:onNegativeQuestionSurface {
+        (_:X _:Y _:T) complex:dial _:Tp.
+    }.
+    _:X math:lessThan 0.
+    _:Y math:lessThan 0.
+    (3.141592653589793 _:T) math:sum _:Tp.
+}.
+
+(_:X _:Y _:T _:Tp) log:onNegativeSurface {
+    () log:onNegativeQuestionSurface {
+        (_:X _:Y _:T) complex:dial _:Tp.
+    }.
+    _:X math:notLessThan 0.
+    _:Y math:lessThan 0.
+    (3.141592653589793 2) math:product _:Z1.
+    (_:Z1 _:T) math:difference _:Tp.
+}.
+
+# query
+(_:A _:B _:C _:D) log:onNegativeSurface {
+    ((2.718281828459045 0) (0 3.141592653589793)) complex:exponentiation (_:A _:B).
+    ((_:A _:B) (1.0 0.0)) complex:sum (_:C _:D).
+    _:C math:notLessThan -2.0e-16.
+    _:C math:lessThan 2.0e-16.
+    _:D math:notLessThan -2.0e-16.
+    _:D math:lessThan 2.0e-16.
+    () log:onNegativeAnswerSurface {
+        :test :is true.
+    }.
+}.