aboutsummaryrefslogtreecommitdiff
path: root/stdlib/test
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/test')
-rw-r--r--stdlib/test/test/lux/math/constructive.lux58
-rw-r--r--stdlib/test/tests.lux1
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]