Monoids in RedPRL

monoid.prl

define IsSemigroup(#ty, #mul) =
  (record
    [assoc:
      (-> 
       [a b c: #ty]
       (= #ty 
        ($ #mul a ($ #mul b c))
        ($ #mul ($ #mul a b) c)
       )
      )
    ]).

theorem Semigroup(#l: lvl): (U (++ #l))  
  by {
  `(record
    [carrier: (U #l)]
    [mul: (-> carrier carrier carrier)]
    [is-semigroup: (IsSemigroup carrier mul)]
  )
}.

define IsMonoid(#ty, #mul, #unit) =
  (record
    [is-semigroup: (IsSemigroup #ty #mul)]
    [idn/l: 
      (->
        [a: #ty]
        (= #ty ($ #mul #unit a) a)
      )
    ]
    [idn/r: 
      (->
        [a: #ty]
        (= #ty ($ #mul a #unit) a)
      )
    ]
  ).

theorem Monoid(#l: lvl): (U (++ #l))  
  by {
  `(record
    [carrier: (U #l)]
    [mul: (-> carrier carrier carrier)]
    [unit: carrier]
    [is-monoid: (IsMonoid carrier mul unit)]
  )
}.

define IsGroup(#ty, #mul, #unit, #inv) =
  (record
    [is-monoid: (IsMonoid #ty #mul #unit)]
    [inv/l: 
      (-> [a: #ty] (= #ty ($ #mul ($ #inv a) a) #unit))
    ]
    [inv/r: 
      (-> [a: #ty] (= #ty ($ #mul a ($ #inv a)) #unit))
    ]
  ).

theorem Group(#l: lvl): (U (++ #l))  
  by {
  `(record
    [carrier: (U #l)]
    [mul: (-> carrier carrier carrier)]
    [unit: carrier]
    [inv: (-> carrier carrier)]
    [is-group: (IsGroup carrier mul unit inv)]
  )
}.

theorem Or :
  (-> bool bool bool)
by {
  lam a b => if a then `tt else `b
}.



theorem OrIsSemigroup :
  (IsSemigroup bool Or)
by {
  { assoc = 
      lam a b c => elim a; elim b; elim c; unfold Or; auto
  }
}.

theorem OrIsMonoid : (IsMonoid bool Or ff) by {
  { is-semigroup = `OrIsSemigroup
  , idn/l = lam a => auto
  , idn/r = 
      lam a => elim a; auto
  }
}.

define Monoid-0 = (Monoid #lvl{0}).

theorem AnyMonoid: Monoid-0 by { 
  { is-monoid = `OrIsMonoid
  , carrier = `bool
  , mul = `Or
  , unit = `ff
  } 
}.


data IntList: (U 0 kan) {
  nil,
  cons int self
} by {
  auto
}.

theorem AppendInt :
  (-> (. IntList type) (.IntList type) (.IntList type))
by {
  lam l => elim l;
  [ `(lam [r] r)
  , with ind _ x => 
      `(lam [r] (.IntList cons x ($ ind r)))
  ];
  auto;
}.

define Inil = (.IntList nil).
define Ilist = (.IntList type).
theorem Icons: (-> int Ilist Ilist) by { lam a xs => `(.IntList cons a xs) }.

theorem AppendInt' :
  (-> (. IntList type) (.IntList type) (.IntList type))
by {
  lam l r => 
  `(.IntList rec 
    [_] Ilist
    l
    r
    [x _ ind] ($ Icons x ind)
  )
}.


theorem IntApp-1-2-3 :
  (= Ilist 
    ($ Icons (int 0) ($ Icons (int 1) ($ Icons (int 2) Inil)))
    ($ AppendInt
      ($ Icons (int 0) ($Icons (int 1) Inil)) ($ Icons (int 2) Inil)))
by {
  auto
}.

theorem IntApp'-1-2-3 :
  (= Ilist 
    ($ Icons (int 0) ($ Icons (int 1) ($ Icons (int 2) Inil)))
    ($ AppendInt'
      ($ Icons (int 0) ($Icons (int 1) Inil)) ($ Icons (int 2) Inil)))
by {
  auto
}.

data List(#l: lvl) [a: (U #l coe)]: (U #l kan) {
  nil,
  cons a self
} by {
  auto
}.

define Listy(#l, #a) =
  (.List type #l #a).


define Nil(#l, #a) =
  (.List nil #l #a).

define Cons(#l, #a, #x, #xs) =
  (.List cons #l #a #x #xs).


theorem Append(#l: lvl) :
  (-> [a: (U #l coe)] (.List type #l a) (.List type #l a) (.List type #l a))
by {
  lam a ls rs =>
  [`(.List rec 
    [_] (.List type #l a)
    ls
    rs
    [x _ ind] (.List cons #l a x ind)
  );
  auto;?a]
}.