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

3 files changed, 255 insertions, 0 deletions

diff --git a/stdlib/source/lux/math/constructive.lux b/stdlib/source/lux/math/constructive.lux
new file mode 100644
index 000000000..3f12d1a88
--- /dev/null
+++ b/stdlib/source/lux/math/constructive.lux
@@ -0,0 +1,196 @@
+(.module:
+  [lux #+ ->]
+  (lux (control [monad #+ do]
+                ["p" parser "parser/" Monad<Parser>]
+                ["ex" exception #+ exception:])
+       (data [product]
+             ["e" error]
+             text/format
+             (coll [list "list/" Functor<List>]))
+       (type abstract)
+       [macro]
+       (macro [code]
+              ["s" syntax #+ syntax:]
+              (syntax (common ["scr" reader]
+                              ["scw" writer]))
+              [poly])))
+
+(abstract: #export (Witness t w)
+  {}
+
+  t
+
+  (.def: #export !
+    (.All [t]
+      (.Ex [w]
+        (-> t (Witness t w))))
+    (.|>> @abstraction))
+
+  (.def: #export ?
+    (.All [t w]
+      (-> (Witness t w) t))
+    (.|>> @representation))
+  )
+
+(syntax: #export (@ [name s.symbol])
+  (do @
+    [witnessT (macro.find-type name)]
+    (.case (.<| (poly.run witnessT)
+                poly.apply
+                (p.after (poly.this Witness))
+                (p.after poly.any)
+                poly.existential)
+      (#e.Success witness-id)
+      (wrap (.list (.` (#.Ex (~ (code.nat witness-id))))))
+      
+      (#e.Error error)
+      (macro.fail error))))
+
+(syntax: #export (proof: [export? scr.export]
+                   [name s.local-symbol]
+                   type
+                   proof)
+  (do @
+    [g!w (macro.gensym "w")]
+    (wrap (.list (.` (.def: (~+ (scw.export export?))
+                       (~ (code.local-symbol name))
+                       (..! (.: (~ type)
+                                (~ proof)))))))))
+
+(.def: type-vars
+  (s.Syntax (.List .Text))
+  (p.default (.list)
+             (s.tuple (p.some s.local-symbol))))
+
+(.type: Input'
+  {#input-name .Text
+   #input-type .Code})
+
+(.type: Input
+  (#Identified Input')
+  (#Anonymous Input'))
+
+(.do-template [<name> <tag> <type>]
+  [(.def: (<name> input)
+     (-> Input <type>)
+     (.case input
+       (#Identified input')
+       (.get@ <tag> input')
+       
+       (#Anonymous input')
+       (.get@ <tag> input')))]
+
+  [input-name #input-name .Text]
+  [input-type #input-type .Code]
+  )
+
+(.def: (identified? input)
+  (-> Input .Bool)
+  (.case input
+    (#Identified input')
+    true
+    
+    (#Anonymous input')
+    false))
+
+(.def: input
+  (s.Syntax Input)
+  (p.alt (s.record (p.seq s.local-symbol s.any))
+         (s.tuple (p.seq s.local-symbol s.any))))
+
+(.def: theorem-declaration
+  (s.Syntax [.Text (.List Input)])
+  (s.form (p.seq s.local-symbol (p.some input))))
+
+(.def: proposition-declaration
+  (s.Syntax [.Text (.List .Text)])
+  (s.form (p.seq s.local-symbol (p.many s.local-symbol))))
+
+(syntax: #export (proposition: [export? scr.export]
+                   [[name elements] proposition-declaration]
+                   [meaning (p.maybe s.any)])
+  (.case meaning
+    #.None
+    (wrap (.list (.` ((~! abstract:) (~+ (scw.export export?))
+                      ((~ (code.local-symbol name))
+                       (~+ (list/map code.local-symbol elements)))
+
+                      {}
+
+                      .Unit))))
+
+    (#.Some meaning)
+    (wrap (.list (.` (.type: (~+ (scw.export export?))
+                       ((~ (code.local-symbol name))
+                        (~+ (list/map code.local-symbol elements)))
+                       (~ meaning)))))))
+
+(.def: (theorem-type type-vars inputs meaning)
+  (-> (.List .Text) (.List Input) .Code .Code)
+  (.let [g!universals (list/map code.local-symbol
+                                type-vars)
+         g!identities (.|> inputs
+                           (list.filter identified?)
+                           (list/map (.|>> input-name code.local-symbol)))
+         g!requisites (list/map (.function [input]
+                                  (.case input
+                                    (#Identified input')
+                                    (.` (..Witness (~ (.get@ #input-type input'))
+                                                   (~ (code.local-symbol (input-name input)))))
+                                    
+                                    (#Anonymous input')
+                                    (.get@ #input-type input')))
+                                inputs)]
+    (.` (.All [(~+ g!universals)]
+          (.Ex [(~+ g!identities)]
+            (-> (~+ g!requisites) (~ meaning)))))))
+
+(syntax: #export (axiom [description (p.default "" s.text)])
+  (wrap (.list (.` (.:!! [])))))
+
+(syntax: #export (theorem [type-vars type-vars]
+                          [[name inputs] theorem-declaration]
+                          outputT
+                          meaning)
+  (.let [inputs-names (list/map (.|>> input-name code.local-symbol)
+                                inputs)]
+    (wrap (.list (.` (.: (~ (theorem-type type-vars inputs outputT))
+                         (.function (~ (code.local-symbol name))
+                           [(~+ inputs-names)]
+                           (~ meaning))))))))
+
+(.def: (input-code input)
+  (-> Input .Code)
+  (.case input
+    (#Identified [name type])
+    (.` {(~ (code.local-symbol name)) (~ type)})
+    
+    (#Anonymous [name type])
+    (.` [(~ (code.local-symbol name)) (~ type)])))
+
+(syntax: #export (theorem: [export? scr.export]
+                   [type-vars type-vars]
+                   [[name inputs] theorem-declaration]
+                   outputT
+                   meaning)
+  (wrap (.list (.` (..proof: (~+ (scw.export export?))
+                     (~ (code.local-symbol name))
+                     (~ (theorem-type type-vars inputs outputT))
+                     (..theorem [(~+ (list/map code.local-symbol type-vars))]
+                                ((~ (code.local-symbol name)) (~+ (list/map input-code inputs)))
+                                (~ outputT)
+                                (~ meaning)))))))
+
+(.type: #export (not p)
+  (-> p .Bottom))
+
+(.type: #export (Test p)
+  (#True p)
+  (#False (not p)))
+
+(exception: #export Absurdity)
+
+(.def: #export absurdity
+  (.All [p] (-> p .Bottom))
+  (.function [proof]
+    (.error! (Absurdity ""))))
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]