stdlib/source/test/lux/math/logic/continuous.lux


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

(.using
 [library
  [lux "*"
   ["_" test {"+" Test}]
   [abstract
    [monad {"+" do}]
    [\\specification
     ["$[0]" monoid]]]
   [math
    ["[0]" random]
    [number
     ["r" rev]]]]]
 [\\library
  ["[0]" /]])

(def: .public test
  Test
  (<| (_.covering /._)
      (do random.monad
        [left random.rev
         mid random.rev
         right random.rev]
        (`` (all _.and
                 (~~ (template [<monoid>]
                       [(_.for [<monoid>]
                               ($monoid.spec r.= <monoid> random.rev))]
                       
                       [/.disjunction]
                       [/.conjunction]
                       ))
                 
                 (_.cover [/.true /.false]
                          (let [true=max!
                                (r.= /.false (++ /.true))

                                false=min!
                                (r.= /.true (-- /.false))]
                            (and true=max!
                                 false=min!)))
                 (_.cover [/.or]
                          (let [identity!
                                (r.= left (/.or /.false left))

                                annihilation!
                                (r.= /.true (/.or /.true left))
                                
                                idempotence!
                                (r.= left (/.or left left))

                                associativity!
                                (r.= (all /.or left mid right)
                                     (.left /.or left mid right))]
                            (and identity!
                                 annihilation!
                                 idempotence!
                                 associativity!
                                 (let [l|r (/.or left right)]
                                   (and (r.>= left l|r)
                                        (r.>= right l|r))))))
                 (_.cover [/.and]
                          (let [identity!
                                (r.= left (/.and /.true left))

                                annihilation!
                                (r.= /.false (/.and /.false left))
                                
                                idempotence!
                                (r.= left (/.and left left))

                                associativity!
                                (r.= (all /.and left mid right)
                                     (.left /.and left mid right))]
                            (and identity!
                                 annihilation!
                                 idempotence!
                                 associativity!
                                 (let [l&r (/.and left right)]
                                   (and (r.<= left l&r)
                                        (r.<= right l&r))))))
                 (_.cover [/.not]
                          (let [inverses!
                                (and (r.= /.false (/.not /.true))
                                     (r.= /.true (/.not /.false)))

                                double_negation!
                                (r.= left (/.not (/.not left)))

                                de_morgan!
                                (and (r.= (/.not (/.or left right))
                                          (/.and (/.not left) (/.not right)))
                                     (r.= (/.not (/.and left right))
                                          (/.or (/.not left) (/.not right))))]
                            (and inverses!
                                 double_negation!
                                 de_morgan!)))
                 (_.cover [/.implies]
                          (let [modus_tollens!
                                (r.= (/.implies right left)
                                     (/.implies (/.not left) (/.not right)))]
                            (and modus_tollens!)))
                 (_.cover [/.=]
                          (let [trivial!
                                (and (r.= /.true (/.= /.true /.true))
                                     (r.= /.true (/.= /.false /.false))

                                     (r.= /.false (/.= /.true /.false)))

                                common!
                                (and (r.>= left
                                           (/.= left left))
                                     (r.>= right
                                           (/.= right right)))]
                            (and trivial!
                                 common!)))
                 )))))