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 (.except)
   ["_" test (.only Test)]
   [abstract
    [monad (.only 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]
                       ))
                 
                 (_.coverage [/.true /.false]
                   (let [true=max!
                         (r.= /.false (++ /.true))

                         false=min!
                         (r.= /.true (-- /.false))]
                     (and true=max!
                          false=min!)))
                 (_.coverage [/.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))))))
                 (_.coverage [/.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))))))
                 (_.coverage [/.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!)))
                 (_.coverage [/.implies]
                   (let [modus_tollens!
                         (r.= (/.implies right left)
                              (/.implies (/.not left) (/.not right)))]
                     (and modus_tollens!)))
                 (_.coverage [/.=]
                   (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!)))
                 )))))