# Bourbaki LaTTe

(ns latte-bourbaki
(:refer-clojure :exclude [and or not set complement])
(:require [latte.core :refer [defthm defaxiom definition example
lambda try-proof proof assume have pose qed
type-of type-check?]]
[latte-prelude.quant :refer [ex exists ex-elim] :as q]
[latte-prelude.classic :as classic]
[latte-prelude.prop :refer [and or not absurd] :as prop]
[latte-prelude.equal :refer [equal] :as e]
[latte-sets.core :refer [set elem set-equal set-equal-prop
forall-in]
:as sets]
[latte-sets.algebra :refer [complement]]
[latte-sets.rel :refer [rel]]
[latte-sets.pfun :refer [pfun]]))

We might look at a theory of full groups, i.e. the set support of the group will coincide with the set of all inhabitants of G.

(definition magma "A bourbakian Magma over the type T"
[[T :type]]
(==> T T T))
3[:defined,:term,magma]
(clojure.repl/source example)
(example [[T :type][m (magma T)][x T][y T]]
T
(qed (m x y)))
2[:checked,:example]
(definition associative ""
[[T :type][m (magma T)]]
(forall [x y z T]
(equal (m x (m y z))
(m (m x y) z))))
3[:defined,:term,associative]
(definition monoid "A Monoid is an associative magma with an Identity"
[[T :type][m (magma T)][e T]]
(and (associative T m)
(forall [x T] (and (equal x (m x e))
(equal x (m e x))))))
3[:defined,:term,monoid]
(definition group "A group is a Monoid with inverses"
[[T :type][m (magma T)][e T][i (==> T T)]]
(and (monoid T m e)
(forall [x T] (and (equal e (m (i x) x))
(equal e (m x (i x)))))))
3[:defined,:term,group]
(definition subgroup "A set closed under multiplication and inverses"
[[G :type][m (magma G)][e G][i (==> G G)][H (set G)]]
(and (group G m e i)
(and (elem e H)
(forall-in [x G H]
(forall-in [y G H] (elem (m (i y) x) H))))))
3[:defined,:term,subgroup]