(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)

(** {2 Theory of Equality} *)

(** {3 example: Monoids} *)

type t

function o t t : t
(** composition operator *)

constant e : t
(** identity *)

axiom assoc : forall x y z. o (o x y) z = o x (o y z)
axiom id_left : forall x. o e x = x
axiom id_right : forall x. o x e = x

goal test1 : o e e = e

goal test2 : forall a b. o a b = o b a -> 
    forall x . o (o x a) b = o (o x b) a


(** {3 example: Groups} *)


function i t : t
(** inverse *)

axiom inv_left : forall x. o (i x) x = e

goal inv_e : i e = e

goal inv_right : forall y. o y (i y) = e

goal inv_inv : forall x. i (i x) = x

goal inv_prod : forall x y. i (o x y) = o (i y) (i x)