-- | Named law functions for lattice / Heyting / Boolean carriers.
--
-- These are the value-level oracles: run them on concrete models so claims
-- about \"Boolean\", \"Heyting\", or \"just a lattice\" can go red.
module Circuit.Logics.Laws
  ( -- * Lattice
    law_join_assoc,
    law_join_comm,
    law_join_idem,
    law_meet_assoc,
    law_meet_comm,
    law_meet_idem,
    law_absorption_join,
    law_absorption_meet,

    -- * Heyting
    law_heyting_refl,
    law_heyting_mp_left,
    law_heyting_mp_right,
    law_heyting_distr,

    -- * Boolean
    law_excluded_middle,
    law_noncontradiction,
    law_double_negation,

    -- * Suites
    latticeSuite,
    heytingSuite,
    booleanSuite,
  )
where

import Circuit.Logics.Boolean (Complemented (..))
import Circuit.Logics.Heyting (Heyting (..))
import Circuit.Logics.Lattice
  ( JoinSemiLattice (..),
    LowerBounded (..),
    MeetSemiLattice (..),
    UpperBounded (..),
    (/\),
    (\/),
  )

law_join_assoc :: (JoinSemiLattice a) => a -> a -> a -> Bool
law_join_assoc :: forall a. JoinSemiLattice a => a -> a -> a -> Bool
law_join_assoc a
a a
b a
c = a
a a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ (a
b a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a
c) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a
a a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a
b) a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a
c

law_join_comm :: (JoinSemiLattice a) => a -> a -> Bool
law_join_comm :: forall a. JoinSemiLattice a => a -> a -> Bool
law_join_comm a
a a
b = a
a a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a
a

law_join_idem :: (JoinSemiLattice a) => a -> Bool
law_join_idem :: forall a. JoinSemiLattice a => a -> Bool
law_join_idem a
a = a
a a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a

law_meet_assoc :: (MeetSemiLattice a) => a -> a -> a -> Bool
law_meet_assoc :: forall a. MeetSemiLattice a => a -> a -> a -> Bool
law_meet_assoc a
a a
b a
c = a
a a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ (a
b a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
c) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a
a a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
b) a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
c

law_meet_comm :: (MeetSemiLattice a) => a -> a -> Bool
law_meet_comm :: forall a. MeetSemiLattice a => a -> a -> Bool
law_meet_comm a
a a
b = a
a a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
a

law_meet_idem :: (MeetSemiLattice a) => a -> Bool
law_meet_idem :: forall a. MeetSemiLattice a => a -> Bool
law_meet_idem a
a = a
a a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a

law_absorption_join :: (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> Bool
law_absorption_join :: forall a. (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> Bool
law_absorption_join a
a a
b = a
a a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ (a
a a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
b) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a

law_absorption_meet :: (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> Bool
law_absorption_meet :: forall a. (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> Bool
law_absorption_meet a
a a
b = a
a a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ (a
a a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a
b) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a

law_heyting_refl :: (Heyting a) => a -> Bool
law_heyting_refl :: forall a. Heyting a => a -> Bool
law_heyting_refl a
a = (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
a) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. UpperBounded a => a
top

law_heyting_mp_left :: (Heyting a) => a -> a -> Bool
law_heyting_mp_left :: forall a. Heyting a => a -> a -> Bool
law_heyting_mp_left a
a a
b = (a
a a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
b)) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a
a a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
b)

law_heyting_mp_right :: (Heyting a) => a -> a -> Bool
law_heyting_mp_right :: forall a. Heyting a => a -> a -> Bool
law_heyting_mp_right a
a a
b = (a
b a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
b)) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b

law_heyting_distr :: (Heyting a) => a -> a -> a -> Bool
law_heyting_distr :: forall a. Heyting a => a -> a -> a -> Bool
law_heyting_distr a
a a
b a
c = (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> (a
b a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a
c)) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== ((a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
b) a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ (a
a a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
c))

law_excluded_middle :: (Complemented a) => a -> Bool
law_excluded_middle :: forall a. Complemented a => a -> Bool
law_excluded_middle a
a = (a
a a -> a -> a
forall a. JoinSemiLattice a => a -> a -> a
\/ a -> a
forall a. Complemented a => a -> a
complement a
a) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. UpperBounded a => a
top

law_noncontradiction :: (Complemented a) => a -> Bool
law_noncontradiction :: forall a. Complemented a => a -> Bool
law_noncontradiction a
a = (a
a a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a -> a
forall a. Complemented a => a -> a
complement a
a) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. LowerBounded a => a
bottom

law_double_negation :: (Complemented a) => a -> Bool
law_double_negation :: forall a. Complemented a => a -> Bool
law_double_negation a
a = a -> a
forall a. Complemented a => a -> a
complement (a -> a
forall a. Complemented a => a -> a
complement a
a) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a

-- | All lattice laws on a triple of samples.
latticeSuite :: (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> a -> Bool
latticeSuite :: forall a.
(JoinSemiLattice a, MeetSemiLattice a) =>
a -> a -> a -> Bool
latticeSuite a
a a
b a
c =
  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
    [ a -> a -> a -> Bool
forall a. JoinSemiLattice a => a -> a -> a -> Bool
law_join_assoc a
a a
b a
c,
      a -> a -> Bool
forall a. JoinSemiLattice a => a -> a -> Bool
law_join_comm a
a a
b,
      a -> Bool
forall a. JoinSemiLattice a => a -> Bool
law_join_idem a
a,
      a -> a -> a -> Bool
forall a. MeetSemiLattice a => a -> a -> a -> Bool
law_meet_assoc a
a a
b a
c,
      a -> a -> Bool
forall a. MeetSemiLattice a => a -> a -> Bool
law_meet_comm a
a a
b,
      a -> Bool
forall a. MeetSemiLattice a => a -> Bool
law_meet_idem a
a,
      a -> a -> Bool
forall a. (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> Bool
law_absorption_join a
a a
b,
      a -> a -> Bool
forall a. (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> Bool
law_absorption_meet a
a a
b
    ]

heytingSuite :: (Heyting a) => a -> a -> a -> Bool
heytingSuite :: forall a. Heyting a => a -> a -> a -> Bool
heytingSuite a
a a
b a
c =
  a -> a -> a -> Bool
forall a.
(JoinSemiLattice a, MeetSemiLattice a) =>
a -> a -> a -> Bool
latticeSuite a
a a
b a
c
    Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ a -> Bool
forall a. Heyting a => a -> Bool
law_heyting_refl a
a,
        a -> a -> Bool
forall a. Heyting a => a -> a -> Bool
law_heyting_mp_left a
a a
b,
        a -> a -> Bool
forall a. Heyting a => a -> a -> Bool
law_heyting_mp_right a
a a
b,
        a -> a -> a -> Bool
forall a. Heyting a => a -> a -> a -> Bool
law_heyting_distr a
a a
b a
c
      ]

booleanSuite :: (Heyting a, Complemented a) => a -> a -> a -> Bool
booleanSuite :: forall a. (Heyting a, Complemented a) => a -> a -> a -> Bool
booleanSuite a
a a
b a
c =
  a -> a -> a -> Bool
forall a. Heyting a => a -> a -> a -> Bool
heytingSuite a
a a
b a
c
    Bool -> Bool -> Bool
&& a -> Bool
forall a. Complemented a => a -> Bool
law_excluded_middle a
a
    Bool -> Bool -> Bool
&& a -> Bool
forall a. Complemented a => a -> Bool
law_noncontradiction a
a
    Bool -> Bool -> Bool
&& a -> Bool
forall a. Complemented a => a -> Bool
law_double_negation a
a