aboutsummaryrefslogtreecommitdiff
path: root/stdlib
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib')
-rw-r--r--stdlib/source/lux/math/constructive.lux196
-rw-r--r--stdlib/test/test/lux/math/constructive.lux58
-rw-r--r--stdlib/test/tests.lux1
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]
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 08:51:19 +0000