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]
        (`` ($_ _.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.= ($_ /.or left mid right)
                                    (_$ /.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.= ($_ /.and left mid right)
                                    (_$ /.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!)))
                )))))