--#include "Nat.alfa" --#include "Bool.alfa" package OpFin where open SET use Nat, Fin, Bool, True, rel, pred, whenBool, bool2nat open OpNat use zero, (+), unit, (*) open OpBool use true, false, and, or, not PreMon :: Type = sig {Elem :: Set; op0 :: Elem; op2 :: Elem -> Elem -> Elem;} tail (m::Nat)(f::pred (Fin (suc@_ m))) :: pred (Fin m) = \(n::Fin m) -> f (suc@_ n) -- Quantifiers. prodM (X::PreMon)(m::Nat)(f::Fin m -> X.Elem) :: X.Elem = case m of { (zer) -> X.op0; (suc m') -> X.op2 (f zer@_) (prodM X m' (\(x::Fin m') -> f (suc@_ x)));} filterM (X::PreMon)(m::Nat)(p::pred (Fin m))(f::Fin m -> X.Elem) :: X.Elem = case m of { (zer) -> X.op0; (suc m') -> X.op2 (whenBool X.Elem (f zer@_) X.op0 (p zer@_)) (filterM X m' (tail m' p) (\(x::Fin m') -> f (suc@_ x)));} sum :: (m::Nat) -> (n::Fin m -> Nat) -> Nat = prodM (struct { Elem = Nat; op0 = zero; op2 = (+);}) prod :: (m::Nat) -> (n::Fin m -> Nat) -> Nat = prodM (struct { Elem = Nat; op0 = unit; op2 = (*);}) exist :: (m::Nat) -> (f::Fin m -> Bool) -> Bool = prodM (struct { Elem = Bool; op0 = false; op2 = or;}) forall :: (m::Nat) -> (f::Fin m -> Bool) -> Bool = prodM (struct { Elem = Bool; op0 = true; op2 = and;}) -- The size of a subset given by a boolean predicate. count_sub (m::Nat)(p::Fin m -> Bool) :: Nat = case m of { (zer) -> zero; (suc m') -> (+) (bool2nat (p zer@_)) (count_sub m' (tail m' p));} -- The size of a quotient with boolean equality. count_qout (m::Nat)(r::rel (Fin m)) :: Nat = case m of { (zer) -> zero; (suc m') -> (+) (bool2nat (not (exist m' (\(x::Fin m') -> r zer@_ (suc@_ x))))) (count_qout m' (\(x1::Fin m') -> \(x2::Fin m') -> r (suc@_ x1) (suc@_ x2)));} {-# Alfa hiding on var "exist" as "\$" with symbolfont var "forall" as "\"" with symbolfont #-}