gistfile1.hs

-- This is really Idris code, but it will highlight reasonably as Haskell

module vectorTripleStuff

data Triple = VectorTriple Nat Nat Nat

instance Semigroup Triple where
  (VectorTriple a b c) <+> (VectorTriple d e f) = VectorTriple (a + d) (b + e) (c + f)

instance VerifiedSemigroup Triple where
  semigroupOpIsAssociative (VectorTriple a b c) (VectorTriple d e f) (VectorTriple g h i) = ?tripleTripleTriple

instance Monoid Triple where
  neutral = VectorTriple 0 0 0

instance VerifiedMonoid Triple where
  monoidNeutralIsNeutralL (VectorTriple a b c) = ?monoidLeft
  monoidNeutralIsNeutralR (VectorTriple a b c) = ?monoidRight

---------- Proofs ----------

monoidLeft = proof
  intros
  rewrite plusZeroRightNeutral a
  rewrite plusZeroRightNeutral b
  rewrite plusZeroRightNeutral c
  trivial


monoidRight = proof
  intros
  rewrite plusZeroLeftNeutral a
  rewrite plusZeroLeftNeutral b
  rewrite plusZeroLeftNeutral c
  trivial


tripleTripleTriple = proof
  intros
  rewrite plusAssociative a d g
  rewrite plusAssociative b e h
  rewrite plusAssociative c f i
  trivial

(This doesn't have much of a purpose, but we were talking about similar proofs in my math class at YSU and I thought it'd be a good excuse to try out theorem proving in Idris).