Skip to content

Instantly share code, notes, and snippets.

@konn
Created November 8, 2018 21:40
Show Gist options
  • Save konn/80b14f62d51665d0b6317d5a7b18fa5f to your computer and use it in GitHub Desktop.
Save konn/80b14f62d51665d0b6317d5a7b18fa5f to your computer and use it in GitHub Desktop.
Monoids in RedPRL
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]
}.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment