From 59d674d660b4e52ec54ef046024b850b4eeb7a0f Mon Sep 17 00:00:00 2001
From: Eduardo Julian
Date: Thu, 28 Dec 2017 23:19:37 -0400
Subject: - A small, in-development module for doing constructive mathematics
 with something close to dependent types.

---
 stdlib/test/test/lux/math/constructive.lux | 58 ++++++++++++++++++++++++++++++
 stdlib/test/tests.lux                      |  1 +
 2 files changed, 59 insertions(+)
 create mode 100644 stdlib/test/test/lux/math/constructive.lux

(limited to 'stdlib/test')

diff --git a/stdlib/test/test/lux/math/constructive.lux b/stdlib/test/test/lux/math/constructive.lux
new file mode 100644
index 000000000..715a9a60c
--- /dev/null
+++ b/stdlib/test/test/lux/math/constructive.lux
@@ -0,0 +1,58 @@
+(.module:
+  [lux #+ ->]
+  (lux (data text/format)
+       (math ["_" constructive #*])))
+
+(theorem: #export (n/+ [param .Nat] [subject .Nat])
+  .Nat
+  (.n/+ param subject))
+
+(proposition: #export (apply2 f input0 input1 output))
+
+(proposition: #export (commutativity f left right output)
+  (-> (apply2 f left right output)
+      (apply2 f right left output)))
+
+(proof: #export n/+|commutativity
+  (commutativity (~ (@ n/+)))
+  (theorem [@left @right @output]
+           (_ [normal (apply2 (~ (@ n/+)) @left @right @output)])
+           (apply2 (~ (@ n/+)) @right @left @output)
+
+           (axiom "n/+|commutativity")))
+
+(proposition: #export (equality reference sample))
+
+(theorem: #export [t] (is {reference t} {sample t})
+  (Test (equality reference sample))
+  (.if (.is reference sample)
+    (#_.True (.let [the-axiom (axiom "is")]
+               the-axiom))
+    (#_.False absurdity)))
+
+(proposition: #export (relation2 rel reference sample))
+
+(proposition: #export (reflexivity rel value)
+  (relation2 rel value value))
+
+(proposition: #export (symmetry rel left right)
+  (-> (relation2 rel left right)
+      (relation2 rel right left)))
+
+(proposition: #export (transitivity rel left mid right)
+  (-> [(relation2 rel left mid)
+       (relation2 rel mid right)]
+      (relation2 rel left right)))
+
+(theorem: #export [t0 t1 t2] ($2 {f (-> t0 t1 t2)}
+                                 {input0 t0}
+                                 {input1 t1})
+  [t2 (apply2 f input0 input1 t2)]
+  (.let [output ((? f) (? input0) (? input1))]
+    [output (axiom)]))
+
+(theorem: (can-commute-n/+ {param .Nat} {subject .Nat})
+  .Nat
+  (.let [[output apply2] ((? $2) n/+ param subject)
+         output|commutes! ((? n/+|commutativity) apply2)]
+    output))
diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux
index b5dcf571a..e234b6b48 100644
--- a/stdlib/test/tests.lux
+++ b/stdlib/test/tests.lux
@@ -57,6 +57,7 @@
              ["_." math]
              (math ["_." random]
                    ["_." modular]
+                   ["_." constructive]
                    (logic ["_." continuous]
                           ["_." fuzzy]))
              (macro ["_." code]
-- 
cgit v1.2.3