VerifiedOption.idr

module VerifiedOption

import Classes.Verified

-- data Maybe a = Just a | Nothing

data Option a = Some a | None

-- Associativity
-- (a <+> b) <+> c = a <+> (b <+> c)

instance Semigroup a => Semigroup (Option a) where
  (Some a) <+> (Some b) = Some (a <+> b)
  None <+> a = a
  a <+> b = a

-- Identity laws
-- neutral <+> a = a
-- a <+> neutral = a

instance Semigroup a => Monoid (Option a) where
  neutral = None

-- Verify

instance VerifiedSemigroup a => VerifiedSemigroup (Option a) where
  semigroupOpIsAssociative (Some a) (Some b) (Some c) = ?someSomeSome
  semigroupOpIsAssociative (Some _) (Some _) None = Refl
  semigroupOpIsAssociative (Some _) None _ = Refl
  semigroupOpIsAssociative None _ _ = Refl

instance VerifiedSemigroup a => VerifiedMonoid (Option a) where
  monoidNeutralIsNeutralL (Some _) = Refl
  monoidNeutralIsNeutralL None = Refl
  monoidNeutralIsNeutralR (Some _) = Refl
  monoidNeutralIsNeutralR None = Refl

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

someSomeSome = proof
  intros
  rewrite (semigroupOpIsAssociative a b c)
  trivial

Hi,
I saw your very good explaining YouTube and tried motivated to redo your steps. Unfortunately I got:

Optional.idr:24:10:VerifiedSemigroup is not a type class
Optional.idr:30:10:VerifiedMonoid is not a type class

How could I fix that?

@Jentsch you now have to add:

import Classes.Verified

And change all occurrences of refl with Refl

Is rewrite still a thing in interactive proof mode?

rewrite (semigroupOpIsAssociative a1 b c)
(input):1:42: error: unexpected
    EOF, expected: "$", "&&", "*",
    "*>", "+", "++", "-", "->", ".",
    "/", "/=", "::", "<", "<#>",
    "<$>", "<*", "<*>", "<+>",
    "<->", "<.>", "<<", "<=", "<==",
    "<|>", "<||>", "=", "==", "==>",
    ">", ">=", ">>", ">>=", "\\\\",
    "`", "in", "using", "|", "||",
    "~=~",
    ambiguous use of a left-associative operator,
    ambiguous use of a non-associative operator,
    ambiguous use of a right-associative operator,
    function argument
rewrite (semigroupOpIsAssociative a1 b c)<EOF>
                                         ^