- A small, in-development module for doing constructive mathematics with something close to dependent types.

2 files changed, 59 insertions, 0 deletions

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]