\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Pointed
\import Data.Array
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Set
\import Set.Category
\import Set.Fin

\record FinSuppFunc \extends SetHom {
  \override Cod : AddPointed
  | fSupp : ∃ (s : Array Dom) ∀ i ((\Pi (j : Fin s.len) -> s j /= i) -> func i = )
}

\instance FinSuppFuncDec (M : DecSet) (R : AddPointed) {D : DecSet R} : DecSet (FinSuppFunc M R)
  | decideEq f g => \case fSupp {f}, fSupp {g} \with {
    | inP (s : Array, c), inP (s' : Array, c') =>
      \case FinSet.search (\lam j => f (s j) /= g (s j)) (\lam j => decide), FinSet.search (\lam j => f (s' j) /= g (s' j)) (\lam j => decide) \with {
        | yes (inP (j,d)), _ => no \lam p => d $ pmap {FinSuppFunc M R} (__ (s j)) p
        | _, yes (inP (j,d)) => no \lam p => d $ pmap {FinSuppFunc M R} (__ (s' j)) p
        | no q, no q' => yes $ exts \lam i => \case FinSet.search (\lam j => i = s j) (\lam j => decide), FinSet.search (\lam j => i = s' j) (\lam j => decide) \with {
          | yes (inP (j,p)), _ => rewrite p $ tightness \lam e => q  $ inP (j, Set#.apartNotEqual e)
          | _, yes (inP (j,p)) => rewrite p $ tightness \lam e => q' $ inP (j, Set#.apartNotEqual e)
          | no r, no r' => c i (\lam j p => r $ inP (j, inv p)) *> inv (c' i \lam j p => r' $ inP (j, inv p))
        }
      }
  }

\instance FinSuppFuncAddPointed {A : BaseSet} {B : AddPointed} : AddPointed (FinSuppFunc A B)
  | zro => \new FinSuppFunc {
    | func _ => 
    | fSupp => inP (nil, \lam _ _ => idp)
  }

\instance FinSuppFuncAddMonoid {A : BaseSet} {B : AddMonoid} : AddMonoid (FinSuppFunc A B)
  | AddPointed => FinSuppFuncAddPointed
  | + f g => \new FinSuppFunc {
    | func a => f a + g a
    | fSupp => \case fSupp {f}, fSupp {g} \with {
      | inP (s,c), inP (s',c') => inP (s ++ s', \lam a d => pmap2 (+) (c a \lam j => rewrite ++.++_index-left in d (++.index-left j)) (c' a \lam j => rewrite ++.++_index-right in d (++.index-right j)) *> zro-left)
    }
  }
  | zro-left => exts (\lam a => zro-left)
  | zro-right => exts (\lam a => zro-right)
  | +-assoc => exts (\lam a => +-assoc)

\instance FinSuppFuncAbMonoid {A : BaseSet} {B : AbMonoid} : AbMonoid (FinSuppFunc A B)
  | AddMonoid => FinSuppFuncAddMonoid
  | +-comm => exts (\lam a => +-comm)

\instance FinSuppFuncAddGroup {A : BaseSet} {B : AddGroup} : AddGroup (FinSuppFunc A B)
  | AddMonoid => FinSuppFuncAddMonoid
  | negative f => \new FinSuppFunc {
    | func a => negative (f a)
    | fSupp => TruncP.map (fSupp {f}) \lam c => (c., \lam a d => pmap negative (c. a d) *> B.negative_zro)
  }
  | negative-left => exts (\lam a => negative-left)
  | negative-right => exts (\lam a => negative-right)

\instance FinSuppFuncAbGroup {A : BaseSet} {B : AbGroup} : AbGroup (FinSuppFunc A B)
  | AddGroup => FinSuppFuncAddGroup
  | +-comm => FinSuppFuncAbMonoid.+-comm